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));
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;
A3: now :: thesis: for x being Point of (TOP-REAL n) holds (x + p) - (q + p) = x - q
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;
A4: dom (transl (p,(TOP-REAL n))) = [#] (TOP-REAL n) by FUNCT_2:def 1;
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))) .: (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))
proof
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;
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)) )
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;
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)
proof
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))
proof
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;
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)) )
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;
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))
proof
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;
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)) )
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