let n be Nat; :: thesis: for p, q being Point of (TOP-REAL n)

for r being Real holds

( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

let p, q be Point of (TOP-REAL n); :: thesis: for r being Real holds

( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

let r be Real; :: thesis: ( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

set TR = TOP-REAL n;

set T = transl (p,(TOP-REAL n));

thus (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) :: thesis: ( (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

assume A26: y in Sphere ((q + p),r) ; :: thesis: y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r))

then reconsider y = y as Point of (TOP-REAL n) ;

A27: (y - p) - q = y - (p + q) by RLVECT_1:27;

|.(y - (q + p)).| = r by A26, TOPREAL9:9;

then A28: y - p in Sphere (q,r) by A27;

(transl (p,(TOP-REAL n))) . (y - p) = y by A2;

hence y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) by A28, A4, FUNCT_1:def 6; :: thesis: verum

for r being Real holds

( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

let p, q be Point of (TOP-REAL n); :: thesis: for r being Real holds

( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

let r be Real; :: thesis: ( (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

set TR = TOP-REAL n;

set T = transl (p,(TOP-REAL n));

A2: now :: thesis: for q being Point of (TOP-REAL n) holds (transl (p,(TOP-REAL n))) . (q - p) = q

let q be Point of (TOP-REAL n); :: thesis: (transl (p,(TOP-REAL n))) . (q - p) = q

(q - p) + p = q - (p - p) by RLVECT_1:29

.= q - (0. (TOP-REAL n)) by RLVECT_1:def 10

.= q by RLVECT_1:13 ;

hence (transl (p,(TOP-REAL n))) . (q - p) = q by RLTOPSP1:def 10; :: thesis: verum

end;(q - p) + p = q - (p - p) by RLVECT_1:29

.= q - (0. (TOP-REAL n)) by RLVECT_1:def 10

.= q by RLVECT_1:13 ;

hence (transl (p,(TOP-REAL n))) . (q - p) = q by RLTOPSP1:def 10; :: thesis: verum

A3: now :: thesis: for x being Point of (TOP-REAL n) holds (x + p) - (q + p) = x - q

A4:
dom (transl (p,(TOP-REAL n))) = [#] (TOP-REAL n)
by FUNCT_2:def 1;let x be Point of (TOP-REAL n); :: thesis: (x + p) - (q + p) = x - q

thus (x + p) - (q + p) = ((x + p) - p) - q by RLVECT_1:27

.= (x + (p - p)) - q by RLVECT_1:28

.= (x + (0. (TOP-REAL n))) - q by RLVECT_1:def 10

.= x - q by RLVECT_1:def 4 ; :: thesis: verum

end;thus (x + p) - (q + p) = ((x + p) - p) - q by RLVECT_1:27

.= (x + (p - p)) - q by RLVECT_1:28

.= (x + (0. (TOP-REAL n))) - q by RLVECT_1:def 10

.= x - q by RLVECT_1:def 4 ; :: thesis: verum

thus (transl (p,(TOP-REAL n))) .: (Ball (q,r)) = Ball ((q + p),r) :: thesis: ( (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r) & (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r) )

proof

thus
(transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) = cl_Ball ((q + p),r)
:: thesis: (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) = Sphere ((q + p),r)
thus
(transl (p,(TOP-REAL n))) .: (Ball (q,r)) c= Ball ((q + p),r)
:: according to XBOOLE_0:def 10 :: thesis: Ball ((q + p),r) c= (transl (p,(TOP-REAL n))) .: (Ball (q,r))

assume A10: y in Ball ((q + p),r) ; :: thesis: y in (transl (p,(TOP-REAL n))) .: (Ball (q,r))

then reconsider y = y as Point of (TOP-REAL n) ;

A11: (y - p) - q = y - (p + q) by RLVECT_1:27;

|.(y - (q + p)).| < r by A10, TOPREAL9:7;

then A12: y - p in Ball (q,r) by A11;

(transl (p,(TOP-REAL n))) . (y - p) = y by A2;

hence y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) by A12, A4, FUNCT_1:def 6; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball ((q + p),r) or y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) or y in Ball ((q + p),r) )

assume y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) ; :: thesis: y in Ball ((q + p),r)

then consider x being object such that

A5: x in dom (transl (p,(TOP-REAL n))) and

A6: x in Ball (q,r) and

A7: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;

reconsider x = x as Point of (TOP-REAL n) by A5;

A8: y = x + p by A7, RLTOPSP1:def 10;

A9: (x + p) - (q + p) = x - q by A3;

|.(x - q).| < r by A6, TOPREAL9:7;

hence y in Ball ((q + p),r) by A9, A8; :: thesis: verum

end;assume y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) ; :: thesis: y in Ball ((q + p),r)

then consider x being object such that

A5: x in dom (transl (p,(TOP-REAL n))) and

A6: x in Ball (q,r) and

A7: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;

reconsider x = x as Point of (TOP-REAL n) by A5;

A8: y = x + p by A7, RLTOPSP1:def 10;

A9: (x + p) - (q + p) = x - q by A3;

|.(x - q).| < r by A6, TOPREAL9:7;

hence y in Ball ((q + p),r) by A9, A8; :: thesis: verum

assume A10: y in Ball ((q + p),r) ; :: thesis: y in (transl (p,(TOP-REAL n))) .: (Ball (q,r))

then reconsider y = y as Point of (TOP-REAL n) ;

A11: (y - p) - q = y - (p + q) by RLVECT_1:27;

|.(y - (q + p)).| < r by A10, TOPREAL9:7;

then A12: y - p in Ball (q,r) by A11;

(transl (p,(TOP-REAL n))) . (y - p) = y by A2;

hence y in (transl (p,(TOP-REAL n))) .: (Ball (q,r)) by A12, A4, FUNCT_1:def 6; :: thesis: verum

proof

thus
(transl (p,(TOP-REAL n))) .: (Sphere (q,r)) c= Sphere ((q + p),r)
:: according to XBOOLE_0:def 10 :: thesis: Sphere ((q + p),r) c= (transl (p,(TOP-REAL n))) .: (Sphere (q,r))
thus
(transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) c= cl_Ball ((q + p),r)
:: according to XBOOLE_0:def 10 :: thesis: cl_Ball ((q + p),r) c= (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r))

assume A18: y in cl_Ball ((q + p),r) ; :: thesis: y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r))

then reconsider y = y as Point of (TOP-REAL n) ;

A19: (y - p) - q = y - (p + q) by RLVECT_1:27;

|.(y - (q + p)).| <= r by A18, TOPREAL9:8;

then A20: y - p in cl_Ball (q,r) by A19;

(transl (p,(TOP-REAL n))) . (y - p) = y by A2;

hence y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) by A20, A4, FUNCT_1:def 6; :: thesis: verum

end;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in cl_Ball ((q + p),r) or y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) or y in cl_Ball ((q + p),r) )

assume y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) ; :: thesis: y in cl_Ball ((q + p),r)

then consider x being object such that

A13: x in dom (transl (p,(TOP-REAL n))) and

A14: x in cl_Ball (q,r) and

A15: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;

reconsider x = x as Point of (TOP-REAL n) by A13;

A16: y = x + p by A15, RLTOPSP1:def 10;

A17: (x + p) - (q + p) = x - q by A3;

|.(x - q).| <= r by A14, TOPREAL9:8;

hence y in cl_Ball ((q + p),r) by A17, A16; :: thesis: verum

end;assume y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) ; :: thesis: y in cl_Ball ((q + p),r)

then consider x being object such that

A13: x in dom (transl (p,(TOP-REAL n))) and

A14: x in cl_Ball (q,r) and

A15: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;

reconsider x = x as Point of (TOP-REAL n) by A13;

A16: y = x + p by A15, RLTOPSP1:def 10;

A17: (x + p) - (q + p) = x - q by A3;

|.(x - q).| <= r by A14, TOPREAL9:8;

hence y in cl_Ball ((q + p),r) by A17, A16; :: thesis: verum

assume A18: y in cl_Ball ((q + p),r) ; :: thesis: y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r))

then reconsider y = y as Point of (TOP-REAL n) ;

A19: (y - p) - q = y - (p + q) by RLVECT_1:27;

|.(y - (q + p)).| <= r by A18, TOPREAL9:8;

then A20: y - p in cl_Ball (q,r) by A19;

(transl (p,(TOP-REAL n))) . (y - p) = y by A2;

hence y in (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r)) by A20, A4, FUNCT_1:def 6; :: thesis: verum

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Sphere ((q + p),r) or y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) )
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) or y in Sphere ((q + p),r) )

assume y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) ; :: thesis: y in Sphere ((q + p),r)

then consider x being object such that

A21: x in dom (transl (p,(TOP-REAL n))) and

A22: x in Sphere (q,r) and

A23: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;

reconsider x = x as Point of (TOP-REAL n) by A21;

A24: y = x + p by A23, RLTOPSP1:def 10;

A25: (x + p) - (q + p) = x - q by A3;

|.(x - q).| = r by A22, TOPREAL9:9;

hence y in Sphere ((q + p),r) by A25, A24; :: thesis: verum

end;assume y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) ; :: thesis: y in Sphere ((q + p),r)

then consider x being object such that

A21: x in dom (transl (p,(TOP-REAL n))) and

A22: x in Sphere (q,r) and

A23: (transl (p,(TOP-REAL n))) . x = y by FUNCT_1:def 6;

reconsider x = x as Point of (TOP-REAL n) by A21;

A24: y = x + p by A23, RLTOPSP1:def 10;

A25: (x + p) - (q + p) = x - q by A3;

|.(x - q).| = r by A22, TOPREAL9:9;

hence y in Sphere ((q + p),r) by A25, A24; :: thesis: verum

assume A26: y in Sphere ((q + p),r) ; :: thesis: y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r))

then reconsider y = y as Point of (TOP-REAL n) ;

A27: (y - p) - q = y - (p + q) by RLVECT_1:27;

|.(y - (q + p)).| = r by A26, TOPREAL9:9;

then A28: y - p in Sphere (q,r) by A27;

(transl (p,(TOP-REAL n))) . (y - p) = y by A2;

hence y in (transl (p,(TOP-REAL n))) .: (Sphere (q,r)) by A28, A4, FUNCT_1:def 6; :: thesis: verum