:: The Rotation Group :: by Karol P\kak :: :: Received May 30, 2011 :: Copyright (c) 2011-2012 Association of Mizar Users begin theorem Th1: :: MATRTOP3:1 for n being Nat for K being Field for M being Matrix of n,K for P being Permutation of (Seg n) holds ( Det ((((M * P) @) * P) @) = Det M & ( for i, j being Nat st [i,j] in Indices M holds ((((M * P) @) * P) @) * (i,j) = M * ((P . i),(P . j)) ) ) proofend; theorem Th2: :: MATRTOP3:2 for n being Nat for K being Field for M being V244(b2) Matrix of n,K holds M @ = M proofend; theorem Th3: :: MATRTOP3:3 for r being real number for f being real-valued FinSequence for i being Nat st i in dom f holds Sum (sqr (f +* (i,r))) = ((Sum (sqr f)) - ((f . i) ^2)) + (r ^2) proofend; definition let X be set ; let F be Function-yielding Function; attrF is X -support-yielding means :Def1: :: MATRTOP3:def 1 for f being Function for x being set st f in dom F & (F . f) . x <> f . x holds x in X; end; :: deftheorem Def1 defines -support-yielding MATRTOP3:def_1_:_ for X being set for F being Function-yielding Function holds ( F is X -support-yielding iff for f being Function for x being set st f in dom F & (F . f) . x <> f . x holds x in X ); registration let X be set ; cluster Relation-like Function-like Function-yielding V235() X -support-yielding for set ; existence ex b1 being Function-yielding Function st b1 is X -support-yielding proofend; end; registration let X be set ; let Y be Subset of X; cluster Relation-like Function-like Function-yielding Y -support-yielding -> Function-yielding X -support-yielding for set ; coherence for b1 being Function-yielding Function st b1 is Y -support-yielding holds b1 is X -support-yielding proofend; end; registration let X, Y be set ; cluster Relation-like Function-like Function-yielding X -support-yielding Y -support-yielding -> Function-yielding X /\ Y -support-yielding for set ; coherence for b1 being Function-yielding Function st b1 is X -support-yielding & b1 is Y -support-yielding holds b1 is X /\ Y -support-yielding proofend; let f be Function-yielding X -support-yielding Function; let g be Function-yielding Y -support-yielding Function; clusterg (#) f -> X \/ Y -support-yielding ; coherence f * g is X \/ Y -support-yielding proofend; end; registration let n be Nat; cluster non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total homogeneous for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]; existence ex b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 is homogeneous proofend; end; registration let n, m be Nat; cluster Function-like quasi_total -> FinSequence-yielding for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL m):]; coherence for b1 being Function of (TOP-REAL n),(TOP-REAL m) holds b1 is FinSequence-yielding proofend; end; registration let n, m be Nat; let A be Matrix of n,m,F_Real; cluster Mx2Tran A -> additive ; coherence Mx2Tran A is additive proofend; end; registration let n be Nat; let A be Matrix of n,F_Real; cluster Mx2Tran A -> homogeneous ; coherence Mx2Tran A is homogeneous proofend; end; registration let n be Nat; let f, g be homogeneous Function of (TOP-REAL n),(TOP-REAL n); clusterg (#) f -> homogeneous for Function of (TOP-REAL n),(TOP-REAL n); coherence for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 = f * g holds b1 is homogeneous proofend; end; begin Lm1: for i, n being Nat st i in Seg n holds ex M being Matrix of n,F_Real st ( Det M = - (1. F_Real) & M * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices M holds ( ( k = m & k <> i implies M * (k,k) = 1. F_Real ) & ( k <> m implies M * (k,m) = 0. F_Real ) ) ) ) proofend; definition let n, i be Nat; assume B1: i in Seg n ; func AxialSymmetry (i,n) -> invertible Matrix of n,F_Real means :Def2: :: MATRTOP3:def 2 ( it * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices it holds ( ( k = m & k <> i implies it * (k,k) = 1. F_Real ) & ( k <> m implies it * (k,m) = 0. F_Real ) ) ) ); existence ex b1 being invertible Matrix of n,F_Real st ( b1 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b1 holds ( ( k = m & k <> i implies b1 * (k,k) = 1. F_Real ) & ( k <> m implies b1 * (k,m) = 0. F_Real ) ) ) ) proofend; uniqueness for b1, b2 being invertible Matrix of n,F_Real st b1 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b1 holds ( ( k = m & k <> i implies b1 * (k,k) = 1. F_Real ) & ( k <> m implies b1 * (k,m) = 0. F_Real ) ) ) & b2 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b2 holds ( ( k = m & k <> i implies b2 * (k,k) = 1. F_Real ) & ( k <> m implies b2 * (k,m) = 0. F_Real ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def2 defines AxialSymmetry MATRTOP3:def_2_:_ for n, i being Nat st i in Seg n holds for b3 being invertible Matrix of n,F_Real holds ( b3 = AxialSymmetry (i,n) iff ( b3 * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b3 holds ( ( k = m & k <> i implies b3 * (k,k) = 1. F_Real ) & ( k <> m implies b3 * (k,m) = 0. F_Real ) ) ) ) ); theorem Th4: :: MATRTOP3:4 for i, n being Nat st i in Seg n holds Det (AxialSymmetry (i,n)) = - (1. F_Real) proofend; theorem Th5: :: MATRTOP3:5 for i, n, j being Nat for p being Point of (TOP-REAL n) st i in Seg n & j in Seg n & i <> j holds (@ p) "*" (Col ((AxialSymmetry (i,n)),j)) = p . j proofend; theorem Th6: :: MATRTOP3:6 for i, n being Nat for p being Point of (TOP-REAL n) st i in Seg n holds (@ p) "*" (Col ((AxialSymmetry (i,n)),i)) = - (p . i) proofend; theorem Th7: :: MATRTOP3:7 for i, n being Nat st i in Seg n holds ( AxialSymmetry (i,n) is V244( F_Real ) & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) ) proofend; theorem Th8: :: MATRTOP3:8 for i, n, j being Nat for p being Point of (TOP-REAL n) st i in Seg n & i <> j holds ((Mx2Tran (AxialSymmetry (i,n))) . p) . j = p . j proofend; theorem Th9: :: MATRTOP3:9 for i, n being Nat for p being Point of (TOP-REAL n) st i in Seg n holds ((Mx2Tran (AxialSymmetry (i,n))) . p) . i = - (p . i) proofend; theorem Th10: :: MATRTOP3:10 for i, n being Nat for p being Point of (TOP-REAL n) st i in Seg n holds (Mx2Tran (AxialSymmetry (i,n))) . p = p +* (i,(- (p . i))) proofend; theorem Th11: :: MATRTOP3:11 for i, n being Nat st i in Seg n holds Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding proofend; theorem Th12: :: MATRTOP3:12 for r being real number for n being Nat for a, b being Element of F_Real st a = cos r & b = sin r holds Det (block_diagonal (<*((a,b) ][ ((- b),a)),(1. (F_Real,n))*>,(0. F_Real))) = 1. F_Real proofend; Lm2: for i, j, n being Nat st 1 <= i & i < j & j <= n holds ex P being Permutation of (Seg n) st ( P . 1 = i & P . 2 = j & ( for k being Nat st k in Seg n & k > 2 holds ( ( k <= i + 1 implies P . k = k - 2 ) & ( i + 1 < k & k <= j implies P . k = k - 1 ) & ( k > j implies P . k = k ) ) ) ) proofend; Lm3: for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds ex A being Matrix of n,F_Real st ( Det A = 1. F_Real & A * (i,i) = cos r & A * (j,j) = cos r & A * (i,j) = sin r & A * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices A holds ( ( k = m & k <> i & k <> j implies A * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies A * (k,m) = 0. F_Real ) ) ) ) proofend; begin definition let n be Nat; let r be real number ; let i, j be Nat; assume B1: ( 1 <= i & i < j & j <= n ) ; func Rotation (i,j,n,r) -> invertible Matrix of n,F_Real means :Def3: :: MATRTOP3:def 3 ( it * (i,i) = cos r & it * (j,j) = cos r & it * (i,j) = sin r & it * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices it holds ( ( k = m & k <> i & k <> j implies it * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies it * (k,m) = 0. F_Real ) ) ) ); existence ex b1 being invertible Matrix of n,F_Real st ( b1 * (i,i) = cos r & b1 * (j,j) = cos r & b1 * (i,j) = sin r & b1 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b1 holds ( ( k = m & k <> i & k <> j implies b1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b1 * (k,m) = 0. F_Real ) ) ) ) proofend; uniqueness for b1, b2 being invertible Matrix of n,F_Real st b1 * (i,i) = cos r & b1 * (j,j) = cos r & b1 * (i,j) = sin r & b1 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b1 holds ( ( k = m & k <> i & k <> j implies b1 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b1 * (k,m) = 0. F_Real ) ) ) & b2 * (i,i) = cos r & b2 * (j,j) = cos r & b2 * (i,j) = sin r & b2 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b2 holds ( ( k = m & k <> i & k <> j implies b2 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b2 * (k,m) = 0. F_Real ) ) ) holds b1 = b2 proofend; end; :: deftheorem Def3 defines Rotation MATRTOP3:def_3_:_ for n being Nat for r being real number for i, j being Nat st 1 <= i & i < j & j <= n holds for b5 being invertible Matrix of n,F_Real holds ( b5 = Rotation (i,j,n,r) iff ( b5 * (i,i) = cos r & b5 * (j,j) = cos r & b5 * (i,j) = sin r & b5 * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b5 holds ( ( k = m & k <> i & k <> j implies b5 * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b5 * (k,m) = 0. F_Real ) ) ) ) ); theorem Th13: :: MATRTOP3:13 for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds Det (Rotation (i,j,n,r)) = 1. F_Real proofend; theorem Th14: :: MATRTOP3:14 for r being real number for i, j, n, k being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k in Seg n & k <> i & k <> j holds (@ p) "*" (Col ((Rotation (i,j,n,r)),k)) = p . k proofend; theorem Th15: :: MATRTOP3:15 for r being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds (@ p) "*" (Col ((Rotation (i,j,n,r)),i)) = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) proofend; theorem Th16: :: MATRTOP3:16 for r being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds (@ p) "*" (Col ((Rotation (i,j,n,r)),j)) = ((p . i) * (sin r)) + ((p . j) * (cos r)) proofend; theorem Th17: :: MATRTOP3:17 for r1, r2 being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds (Rotation (i,j,n,r1)) * (Rotation (i,j,n,r2)) = Rotation (i,j,n,(r1 + r2)) proofend; Lm4: for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds (Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r)) proofend; theorem Th18: :: MATRTOP3:18 for i, j, n being Nat st 1 <= i & i < j & j <= n holds Rotation (i,j,n,0) = 1. (F_Real,n) proofend; Lm5: for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) proofend; theorem Th19: :: MATRTOP3:19 for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds ( Rotation (i,j,n,r) is Orthogonal & (Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r)) ) proofend; theorem Th20: :: MATRTOP3:20 for r being real number for i, j, n, k being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & k <> i & k <> j holds ((Mx2Tran (Rotation (i,j,n,r))) . p) . k = p . k proofend; theorem Th21: :: MATRTOP3:21 for r being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = ((p . i) * (cos r)) + ((p . j) * (- (sin r))) proofend; theorem Th22: :: MATRTOP3:22 for r being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = ((p . i) * (sin r)) + ((p . j) * (cos r)) proofend; theorem Th23: :: MATRTOP3:23 for r being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds (Mx2Tran (Rotation (i,j,n,r))) . p = ((((p | (i -' 1)) ^ <*(((p . i) * (cos r)) + ((p . j) * (- (sin r))))*>) ^ ((p /^ i) | ((j -' i) -' 1))) ^ <*(((p . i) * (sin r)) + ((p . j) * (cos r)))*>) ^ (p /^ j) proofend; theorem Th24: :: MATRTOP3:24 for s being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds ex r being real number st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s proofend; Lm6: for r being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n holds ((((Mx2Tran (Rotation (i,j,n,r))) . p) . i) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . i)) + ((((Mx2Tran (Rotation (i,j,n,r))) . p) . j) * (((Mx2Tran (Rotation (i,j,n,r))) . p) . j)) = ((p . i) * (p . i)) + ((p . j) * (p . j)) proofend; theorem Th25: :: MATRTOP3:25 for s being real number for i, j, n being Nat for p being Point of (TOP-REAL n) st 1 <= i & i < j & j <= n & s ^2 <= ((p . i) ^2) + ((p . j) ^2) holds ex r being real number st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s proofend; theorem Th26: :: MATRTOP3:26 for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds Mx2Tran (Rotation (i,j,n,r)) is {i,j} -support-yielding proofend; begin definition let n be Nat; let f be Function of (TOP-REAL n),(TOP-REAL n); attrf is rotation means :Def4: :: MATRTOP3:def 4 for p being Point of (TOP-REAL n) holds |.p.| = |.(f . p).|; end; :: deftheorem Def4 defines rotation MATRTOP3:def_4_:_ for n being Nat for f being Function of (TOP-REAL n),(TOP-REAL n) holds ( f is rotation iff for p being Point of (TOP-REAL n) holds |.p.| = |.(f . p).| ); theorem Th27: :: MATRTOP3:27 for i, n being Nat st i in Seg n holds Mx2Tran (AxialSymmetry (i,n)) is rotation proofend; definition let n be Nat; let f be Function of (TOP-REAL n),(TOP-REAL n); attrf is base_rotation means :Def5: :: MATRTOP3:def 5 ex F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) st ( f = Product F & ( for k being Nat st k in dom F holds ex i, j being Nat ex r being real number st ( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ); end; :: deftheorem Def5 defines base_rotation MATRTOP3:def_5_:_ for n being Nat for f being Function of (TOP-REAL n),(TOP-REAL n) holds ( f is base_rotation iff ex F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) st ( f = Product F & ( for k being Nat st k in dom F holds ex i, j being Nat ex r being real number st ( 1 <= i & i < j & j <= n & F . k = Mx2Tran (Rotation (i,j,n,r)) ) ) ) ); registration let n be Nat; cluster id (TOP-REAL n) -> base_rotation ; coherence id (TOP-REAL n) is base_rotation proofend; end; registration let n be Nat; cluster non empty Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued Function-like total quasi_total FinSequence-yielding Function-yielding V235() base_rotation for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]; existence ex b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 is base_rotation proofend; end; registration let n be Nat; let f, g be base_rotation Function of (TOP-REAL n),(TOP-REAL n); clusterg (#) f -> base_rotation for Function of (TOP-REAL n),(TOP-REAL n); coherence for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 = f * g holds b1 is base_rotation proofend; end; Lm7: for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds Mx2Tran (Rotation (i,j,n,r)) is rotation proofend; theorem Th28: :: MATRTOP3:28 for r being real number for i, j, n being Nat st 1 <= i & i < j & j <= n holds Mx2Tran (Rotation (i,j,n,r)) is base_rotation proofend; Lm8: for n being Nat for f, g being Function of (TOP-REAL n),(TOP-REAL n) st f is rotation & g is rotation holds f * g is rotation proofend; registration let n be Nat; cluster Function-like quasi_total base_rotation -> additive homogeneous being_homeomorphism rotation for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]; coherence for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 is base_rotation holds ( b1 is homogeneous & b1 is additive & b1 is rotation & b1 is being_homeomorphism ) proofend; end; registration let n be Nat; let f be base_rotation Function of (TOP-REAL n),(TOP-REAL n); clusterf /" -> base_rotation ; coherence f " is base_rotation proofend; end; registration let n be Nat; let f, g be rotation Function of (TOP-REAL n),(TOP-REAL n); clusterg (#) f -> rotation for Function of (TOP-REAL n),(TOP-REAL n); coherence for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 = f * g holds b1 is rotation by Lm8; end; definition let n be Nat; let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); func AutMt f -> Matrix of n,F_Real means :Def6: :: MATRTOP3:def 6 f = Mx2Tran it; existence ex b1 being Matrix of n,F_Real st f = Mx2Tran b1 proofend; uniqueness for b1, b2 being Matrix of n,F_Real st f = Mx2Tran b1 & f = Mx2Tran b2 holds b1 = b2 by MATRTOP1:34; end; :: deftheorem Def6 defines AutMt MATRTOP3:def_6_:_ for n being Nat for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) for b3 being Matrix of n,F_Real holds ( b3 = AutMt f iff f = Mx2Tran b3 ); theorem Th29: :: MATRTOP3:29 for n being Nat for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds AutMt (f1 * f2) = (AutMt f2) * (AutMt f1) proofend; theorem Th30: :: MATRTOP3:30 for X being set for k, n being Nat for p being Point of (TOP-REAL n) st k in X & k in Seg n holds ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st ( f is X -support-yielding & f is base_rotation & ( card (X /\ (Seg n)) > 1 implies (f . p) . k >= 0 ) & ( for i being Nat st i in X /\ (Seg n) & i <> k holds (f . p) . i = 0 ) ) proofend; theorem Th31: :: MATRTOP3:31 for n being Nat for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) for A being Subset of (TOP-REAL n) st f | A = id A holds f | (Lin A) = id (Lin A) proofend; theorem Th32: :: MATRTOP3:32 for n being Nat for p being Point of (TOP-REAL n) for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) for A being Subset of (TOP-REAL n) st f is rotation & f | A = id A holds for i being Nat st i in Seg n & Base_FinSeq (n,i) in Lin A holds (f . p) . i = p . i proofend; theorem Th33: :: MATRTOP3:33 for X being set for n being Nat for p being Point of (TOP-REAL n) for f being rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & ( for i being Nat st i in X /\ (Seg n) holds p . i = 0 ) holds f . p = p proofend; theorem Th34: :: MATRTOP3:34 for i, n being Nat for p being Point of (TOP-REAL n) st i in Seg n & n >= 2 holds ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st ( f is base_rotation & f . p = p +* (i,(- (p . i))) ) proofend; Lm9: for X being set for n, i being Nat for f being additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n) st f is X -support-yielding & not i in X holds f . (Base_FinSeq (n,i)) = Base_FinSeq (n,i) proofend; theorem Th35: :: MATRTOP3:35 for i, n being Nat for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is {i} -support-yielding & f is rotation & not AutMt f = AxialSymmetry (i,n) holds AutMt f = 1. (F_Real,n) proofend; theorem Th36: :: MATRTOP3:36 for n being Nat for f1 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation holds ex f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st ( f2 is base_rotation & f2 * f1 is {n} -support-yielding ) proofend; Lm10: for n being Nat for M being Matrix of n,F_Real st Mx2Tran M is base_rotation holds Det M = 1. F_Real proofend; begin theorem Th37: :: MATRTOP3:37 for n being Nat for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is rotation holds ( Det (AutMt f) = 1. F_Real iff f is base_rotation ) proofend; theorem Th38: :: MATRTOP3:38 for n being Nat for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) holds ( not f is rotation or Det (AutMt f) = 1. F_Real or Det (AutMt f) = - (1. F_Real) ) proofend; theorem Th39: :: MATRTOP3:39 for i, n being Nat for f1, f2 being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f1 is rotation & Det (AutMt f1) = - (1. F_Real) & i in Seg n & AutMt f2 = AxialSymmetry (i,n) holds f1 * f2 is base_rotation proofend; Lm11: for n being Nat for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is base_rotation holds AutMt f is Orthogonal proofend; registration let n be Nat; let f be additive homogeneous rotation Function of (TOP-REAL n),(TOP-REAL n); cluster AutMt f -> Orthogonal ; coherence AutMt f is Orthogonal proofend; end; registration let n be Nat; cluster Function-like quasi_total additive homogeneous rotation -> being_homeomorphism for Element of bool [: the carrier of (TOP-REAL n), the carrier of (TOP-REAL n):]; coherence for b1 being Function of (TOP-REAL n),(TOP-REAL n) st b1 is homogeneous & b1 is additive & b1 is rotation holds b1 is being_homeomorphism proofend; end; begin theorem :: MATRTOP3:40 for n being Nat for p, q being Point of (TOP-REAL n) st n = 1 & |.p.| = |.q.| holds ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st ( f is rotation & f . p = q & ( AutMt f = AxialSymmetry (n,n) or AutMt f = 1. (F_Real,n) ) ) proofend; theorem :: MATRTOP3:41 for n being Nat for p, q being Point of (TOP-REAL n) st n <> 1 & |.p.| = |.q.| holds ex f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st ( f is base_rotation & f . p = q ) proofend;