let n be Nat; 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); 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; ( (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));
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)
( (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)
XBOOLE_0:def 10 Ball ((q + p),r) c= (transl (p,(TOP-REAL n))) .: (Ball (q,r))proof
let y be
object ;
TARSKI:def 3 ( 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))
;
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;
verum
end;
let y be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
thus
(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)) c= cl_Ball (
(q + p),
r)
XBOOLE_0:def 10 cl_Ball ((q + p),r) c= (transl (p,(TOP-REAL n))) .: (cl_Ball (q,r))proof
let y be
object ;
TARSKI:def 3 ( 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))
;
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;
verum
end;
let y be
object ;
TARSKI:def 3 ( 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)
;
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;
verum
end;
thus
(transl (p,(TOP-REAL n))) .: (Sphere (q,r)) c= Sphere ((q + p),r)
XBOOLE_0:def 10 Sphere ((q + p),r) c= (transl (p,(TOP-REAL n))) .: (Sphere (q,r))proof
let y be
object ;
TARSKI:def 3 ( 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))
;
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;
verum
end;
let y be object ; TARSKI:def 3 ( 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)
; 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; verum