let X be RealNormSpace; :: thesis: for x being Point of X
for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
let x be Point of X; :: thesis: for r being Real holds Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
let r be Real; :: thesis: Ball ((0. X),r) = (- 1) * (Ball ((0. X),r))
thus Ball ((0. X),r) c= (- 1) * (Ball ((0. X),r)) :: according to XBOOLE_0:def 10 :: thesis: (- 1) * (Ball ((0. X),r)) c= Ball ((0. X),r)
proof
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in Ball ((0. X),r) or z in (- 1) * (Ball ((0. X),r)) )
assume A1: z in Ball ((0. X),r) ; :: thesis: z in (- 1) * (Ball ((0. X),r))
then reconsider z1 = z as Point of X ;
ex zz1 being Point of X st
( z1 = zz1 & ||.((0. X) - zz1).|| < r ) by A1;
then ||.(- z1).|| < r by RLVECT_1:14;
then ||.(- (- z1)).|| < r by NORMSP_1:2;
then ||.((0. X) - (- z1)).|| < r by RLVECT_1:14;
then A2: - z1 in Ball ((0. X),r) ;
(- 1) * (- z1) = 1 * z1 by RLVECT_1:26
.= z1 by RLVECT_1:def 8 ;
hence z in (- 1) * (Ball ((0. X),r)) by A2; :: thesis: verum
end;
let z be object ; :: according to TARSKI:def 3 :: thesis: ( not z in (- 1) * (Ball ((0. X),r)) or z in Ball ((0. X),r) )
assume A3: z in (- 1) * (Ball ((0. X),r)) ; :: thesis: z in Ball ((0. X),r)
then reconsider z1 = z as Point of X ;
consider y1 being Point of X such that
A4: z1 = (- 1) * y1 and
A5: y1 in Ball ((0. X),r) by A3;
ex zz1 being Point of X st
( y1 = zz1 & ||.((0. X) - zz1).|| < r ) by A5;
then ||.(- y1).|| < r by RLVECT_1:14;
then ||.(- (- y1)).|| < r by NORMSP_1:2;
then A6: ||.((0. X) - (- y1)).|| < r by RLVECT_1:14;
- y1 = z1 by A4, RLVECT_1:16;
hence z in Ball ((0. X),r) by A6; :: thesis: verum