let n be Nat; :: thesis: for p being Point of (TOP-REAL n)
for r being Real
for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is onto holds
( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
let p be Point of (TOP-REAL n); :: thesis: for r being Real
for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is onto holds
( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
let r be Real; :: thesis: for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is onto holds
( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
set TR = TOP-REAL n;
let f be additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is onto implies ( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) ) )
assume f is onto ; :: thesis: ( f .: (Ball (p,r)) = Ball ((f . p),r) & f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
A2: - (f . p) = (- 1) * (f . p) by RLVECT_1:16
.= f . ((- 1) * p) by TOPREAL9:def 4
.= f . (- p) by RLVECT_1:16 ;
A3: rng f = the carrier of (TOP-REAL n) by FUNCT_2:def 3;
thus f .: (Ball (p,r)) = Ball ((f . p),r) :: thesis: ( f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) & f .: (Sphere (p,r)) = Sphere ((f . p),r) )
proof
thus f .: (Ball (p,r)) c= Ball ((f . p),r) :: according to XBOOLE_0:def 10 :: thesis: Ball ((f . p),r) c= f .: (Ball (p,r))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Ball (p,r)) or y in Ball ((f . p),r) )
assume y in f .: (Ball (p,r)) ; :: thesis: y in Ball ((f . p),r)
then consider x being object such that
A4: x in dom f and
A5: x in Ball (p,r) and
A6: f . x = y by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL n) by A4;
(f . q) - (f . p) = f . (q - p) by A2, VECTSP_1:def 20;
then A7: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;
|.(q - p).| < r by A5, TOPREAL9:7;
hence y in Ball ((f . p),r) by A7, A6; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball ((f . p),r) or y in f .: (Ball (p,r)) )
assume A8: y in Ball ((f . p),r) ; :: thesis: y in f .: (Ball (p,r))
then consider x being object such that
A9: x in dom f and
A10: f . x = y by A3, FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A9;
(f . x) - (f . p) = f . (x - p) by A2, VECTSP_1:def 20;
then A11: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;
|.((f . x) - (f . p)).| < r by A8, A10, TOPREAL9:7;
then x in Ball (p,r) by A11;
hence y in f .: (Ball (p,r)) by A9, A10, FUNCT_1:def 6; :: thesis: verum
end;
thus f .: (cl_Ball (p,r)) = cl_Ball ((f . p),r) :: thesis: f .: (Sphere (p,r)) = Sphere ((f . p),r)
proof
thus f .: (cl_Ball (p,r)) c= cl_Ball ((f . p),r) :: according to XBOOLE_0:def 10 :: thesis: cl_Ball ((f . p),r) c= f .: (cl_Ball (p,r))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (cl_Ball (p,r)) or y in cl_Ball ((f . p),r) )
assume y in f .: (cl_Ball (p,r)) ; :: thesis: y in cl_Ball ((f . p),r)
then consider x being object such that
A12: x in dom f and
A13: x in cl_Ball (p,r) and
A14: f . x = y by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL n) by A12;
(f . q) - (f . p) = f . (q - p) by A2, VECTSP_1:def 20;
then A15: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;
|.(q - p).| <= r by A13, TOPREAL9:8;
hence y in cl_Ball ((f . p),r) by A15, A14; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in cl_Ball ((f . p),r) or y in f .: (cl_Ball (p,r)) )
assume A16: y in cl_Ball ((f . p),r) ; :: thesis: y in f .: (cl_Ball (p,r))
then consider x being object such that
A17: x in dom f and
A18: f . x = y by A3, FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A17;
(f . x) - (f . p) = f . (x - p) by A2, VECTSP_1:def 20;
then A19: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;
|.((f . x) - (f . p)).| <= r by A16, A18, TOPREAL9:8;
then x in cl_Ball (p,r) by A19;
hence y in f .: (cl_Ball (p,r)) by A17, A18, FUNCT_1:def 6; :: thesis: verum
end;
thus f .: (Sphere (p,r)) c= Sphere ((f . p),r) :: according to XBOOLE_0:def 10 :: thesis: Sphere ((f . p),r) c= f .: (Sphere (p,r))
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in f .: (Sphere (p,r)) or y in Sphere ((f . p),r) )
assume y in f .: (Sphere (p,r)) ; :: thesis: y in Sphere ((f . p),r)
then consider x being object such that
A20: x in dom f and
A21: x in Sphere (p,r) and
A22: f . x = y by FUNCT_1:def 6;
reconsider q = x as Point of (TOP-REAL n) by A20;
(f . q) - (f . p) = f . (q - p) by A2, VECTSP_1:def 20;
then A23: |.((f . q) - (f . p)).| = |.(q - p).| by MATRTOP3:def 4;
|.(q - p).| = r by A21, TOPREAL9:9;
hence y in Sphere ((f . p),r) by A23, A22; :: thesis: verum
end;
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Sphere ((f . p),r) or y in f .: (Sphere (p,r)) )
assume A24: y in Sphere ((f . p),r) ; :: thesis: y in f .: (Sphere (p,r))
then consider x being object such that
A25: x in dom f and
A26: f . x = y by A3, FUNCT_1:def 3;
reconsider x = x as Point of (TOP-REAL n) by A25;
(f . x) - (f . p) = f . (x - p) by A2, VECTSP_1:def 20;
then A27: |.((f . x) - (f . p)).| = |.(x - p).| by MATRTOP3:def 4;
|.((f . x) - (f . p)).| = r by A24, A26, TOPREAL9:9;
then x in Sphere (p,r) by A27;
hence y in f .: (Sphere (p,r)) by A25, A26, FUNCT_1:def 6; :: thesis: verum