:: The Rotation Group
:: by Karol P\kak
::
:: Received May 30, 2011
:: Copyright (c) 2011-2021 Association of Mizar Users


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

theorem Th2: :: MATRTOP3:2
for n being Nat
for K being Field
for M being V254(b2) Matrix of n,K holds M @ = M
proof end;

theorem Th3: :: MATRTOP3:3
for r being Real
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)
proof end;

definition
let X be set ;
let F be Function-yielding Function;
attr F 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 V196() X -support-yielding for set ;
existence
ex b1 being Function-yielding Function st b1 is X -support-yielding
proof end;
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
proof end;
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
proof end;
let f be Function-yielding X -support-yielding Function;
let g be Function-yielding Y -support-yielding Function;
cluster g (#) f -> X \/ Y -support-yielding ;
coherence
f * g is X \/ Y -support-yielding
proof end;
end;

registration
let n be Nat;
cluster Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued non empty 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
proof end;
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
proof end;
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 by MATRTOP1:22;
end;

registration
let n be Nat;
let A be Matrix of n,F_Real;
cluster Mx2Tran A -> homogeneous ;
coherence
Mx2Tran A is homogeneous by MATRTOP1:23;
end;

registration
let n be Nat;
let f, g be homogeneous Function of (TOP-REAL n),(TOP-REAL n);
cluster g (#) 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
proof end;
end;

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

definition
let n, i be Nat;
assume A1: 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 ) ) ) )
proof end;
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
proof end;
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)
proof end;

theorem Th5: :: MATRTOP3:5
for i, j, n 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
proof end;

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

theorem Th7: :: MATRTOP3:7
for i, n being Nat st i in Seg n holds
( AxialSymmetry (i,n) is V254( F_Real ) & (AxialSymmetry (i,n)) ~ = AxialSymmetry (i,n) )
proof end;

theorem Th8: :: MATRTOP3:8
for i, j, n 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
proof end;

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

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

theorem Th11: :: MATRTOP3:11
for i, n being Nat st i in Seg n holds
Mx2Tran (AxialSymmetry (i,n)) is {i} -support-yielding
proof end;

theorem Th12: :: MATRTOP3:12
for r being Real
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
proof end;

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

Lm3: for r being Real
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 ) ) ) )
proof end;

definition
let n be Nat;
let r be Real;
let i, j be Nat;
assume A1: ( 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 ) ) ) )
proof end;
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
proof end;
end;

:: deftheorem Def3 defines Rotation MATRTOP3:def 3 :
for n being Nat
for r being Real
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
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Det (Rotation (i,j,n,r)) = 1. F_Real
proof end;

theorem Th14: :: MATRTOP3:14
for r being Real
for i, j, k, n 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
proof end;

theorem Th15: :: MATRTOP3:15
for r being Real
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)))
proof end;

theorem Th16: :: MATRTOP3:16
for r being Real
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))
proof end;

theorem Th17: :: MATRTOP3:17
for r1, r2 being Real
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))
proof end;

Lm4: for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r)) @ = Rotation (i,j,n,(- r))
proof end;

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

Lm5: for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
(Rotation (i,j,n,r)) ~ = Rotation (i,j,n,(- r))
proof end;

theorem Th19: :: MATRTOP3:19
for r being Real
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)) )
proof end;

theorem Th20: :: MATRTOP3:20
for r being Real
for i, j, k, n 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
proof end;

theorem Th21: :: MATRTOP3:21
for r being Real
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)))
proof end;

theorem Th22: :: MATRTOP3:22
for r being Real
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))
proof end;

theorem Th23: :: MATRTOP3:23
for r being Real
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)
proof end;

theorem Th24: :: MATRTOP3:24
for s being Real
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 st ((Mx2Tran (Rotation (i,j,n,r))) . p) . i = s
proof end;

Lm6: for r being Real
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))
proof end;

theorem Th25: :: MATRTOP3:25
for s being Real
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 st ((Mx2Tran (Rotation (i,j,n,r))) . p) . j = s
proof end;

theorem Th26: :: MATRTOP3:26
for r being Real
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
proof end;

definition
let n be Nat;
let f be Function of (TOP-REAL n),(TOP-REAL n);
attr f 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
proof end;

definition
let n be Nat;
let f be Function of (TOP-REAL n),(TOP-REAL n);
attr f 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 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 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
proof end;
end;

registration
let n be Nat;
cluster Relation-like the carrier of (TOP-REAL n) -defined the carrier of (TOP-REAL n) -valued non empty Function-like total quasi_total Function-yielding V196() FinSequence-yielding 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
proof end;
end;

registration
let n be Nat;
let f, g be base_rotation Function of (TOP-REAL n),(TOP-REAL n);
cluster g (#) 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
proof end;
end;

Lm7: for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Mx2Tran (Rotation (i,j,n,r)) is rotation
proof end;

theorem Th28: :: MATRTOP3:28
for r being Real
for i, j, n being Nat st 1 <= i & i < j & j <= n holds
Mx2Tran (Rotation (i,j,n,r)) is base_rotation
proof end;

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

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

registration
let n be Nat;
let f be base_rotation Function of (TOP-REAL n),(TOP-REAL n);
cluster f /" -> base_rotation ;
coherence
f " is base_rotation
proof end;
end;

registration
let n be Nat;
let f, g be rotation Function of (TOP-REAL n),(TOP-REAL n);
cluster g (#) 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
proof end;
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)
proof end;

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

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

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

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

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

Lm9: for X being set
for i, n 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)
proof end;

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

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

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

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

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

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

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

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

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

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