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) )

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

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 .: (cl_Ball (p,r)) = cl_Ball ((f . p),r)
:: thesis: f .: (Sphere (p,r)) = Sphere ((f . p),r)
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))

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;proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Ball ((f . p),r) or y in f .: (Ball (p,r)) )
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;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

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

proof

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))
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))

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;proof

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)) )
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;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

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

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in Sphere ((f . p),r) or y in f .: (Sphere (p,r)) )
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;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

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