let X be RealNormSpace; for r, a being Real st 0 < a holds
Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
let r, a be Real; ( 0 < a implies Ball ((0. X),(a * r)) = a * (Ball ((0. X),r)) )
assume A1:
0 < a
; Ball ((0. X),(a * r)) = a * (Ball ((0. X),r))
thus
Ball ((0. X),(a * r)) c= a * (Ball ((0. X),r))
XBOOLE_0:def 10 a * (Ball ((0. X),r)) c= Ball ((0. X),(a * r))proof
let z be
object ;
TARSKI:def 3 ( not z in Ball ((0. X),(a * r)) or z in a * (Ball ((0. X),r)) )
assume A2:
z in Ball (
(0. X),
(a * r))
;
z in a * (Ball ((0. X),r))
then reconsider z1 =
z as
Point of
X ;
ex
zz1 being
Point of
X st
(
z1 = zz1 &
||.((0. X) - zz1).|| < a * r )
by A2;
then
||.(- z1).|| < a * r
by RLVECT_1:14;
then
||.z1.|| < a * r
by NORMSP_1:2;
then
(a ") * ||.z1.|| < (a ") * (a * r)
by A1, XREAL_1:68;
then
(a ") * ||.z1.|| < (a * (a ")) * r
;
then A3:
(a ") * ||.z1.|| < 1
* r
by A1, XCMPLX_0:def 7;
set y1 =
(a ") * z1;
||.((a ") * z1).|| =
|.(a ").| * ||.z1.||
by NORMSP_1:def 1
.=
(a ") * ||.z1.||
by A1, ABSVALUE:def 1
;
then
||.(- ((a ") * z1)).|| < r
by A3, NORMSP_1:2;
then
||.((0. X) - ((a ") * z1)).|| < r
by RLVECT_1:14;
then A4:
(a ") * z1 in Ball (
(0. X),
r)
;
a * ((a ") * z1) =
(a * (a ")) * z1
by RLVECT_1:def 7
.=
1
* z1
by A1, XCMPLX_0:def 7
.=
z1
by RLVECT_1:def 8
;
hence
z in a * (Ball ((0. X),r))
by A4;
verum
end;
let z be object ; TARSKI:def 3 ( not z in a * (Ball ((0. X),r)) or z in Ball ((0. X),(a * r)) )
assume A5:
z in a * (Ball ((0. X),r))
; z in Ball ((0. X),(a * r))
then reconsider z1 = z as Point of X ;
consider y1 being Point of X such that
A6:
z1 = a * y1
and
A7:
y1 in Ball ((0. X),r)
by A5;
ex yy1 being Point of X st
( y1 = yy1 & ||.((0. X) - yy1).|| < r )
by A7;
then
||.(- y1).|| < r
by RLVECT_1:14;
then A8:
||.y1.|| < r
by NORMSP_1:2;
||.z1.|| =
|.a.| * ||.y1.||
by A6, NORMSP_1:def 1
.=
a * ||.y1.||
by A1, ABSVALUE:def 1
;
then
||.z1.|| < a * r
by A1, A8, XREAL_1:68;
then
||.(- z1).|| < a * r
by NORMSP_1:2;
then
||.((0. X) - z1).|| < a * r
by RLVECT_1:14;
hence
z in Ball ((0. X),(a * r))
; verum