:: 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(b₂) 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 b₁ being Function-yielding Function st b₁ 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 b₁ being Function-yielding Function st b₁ is Y -support-yielding holds
b₁ 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 b₁ being Function-yielding Function st b₁ is X -support-yielding & b₁ is Y -support-yielding holds
b₁ 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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ 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 b₁ being Function of (TOP-REAL n),(TOP-REAL m) holds b₁ 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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ = f * g holds
b₁ 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 b₁ being invertible Matrix of n,F_Real st
( b₁ * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b₁ holds
( ( k = m & k <> i implies b₁ * (k,k) = 1. F_Real ) & ( k <> m implies b₁ * (k,m) = 0. F_Real ) ) ) )

proof end;

uniqueness
for b₁, b₂ being invertible Matrix of n,F_Real st b₁ * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b₁ holds
( ( k = m & k <> i implies b₁ * (k,k) = 1. F_Real ) & ( k <> m implies b₁ * (k,m) = 0. F_Real ) ) ) & b₂ * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b₂ holds
( ( k = m & k <> i implies b₂ * (k,k) = 1. F_Real ) & ( k <> m implies b₂ * (k,m) = 0. F_Real ) ) ) holds
b₁ = b₂

proof end;

end;

:: deftheorem Def2 defines AxialSymmetry MATRTOP3:def 2 :
for n, i being Nat st i in Seg n holds
for b₃ being invertible Matrix of n,F_Real holds
( b₃ = AxialSymmetry (i,n) iff ( b₃ * (i,i) = - (1. F_Real) & ( for k, m being Nat st [k,m] in Indices b₃ holds
( ( k = m & k <> i implies b₃ * (k,k) = 1. F_Real ) & ( k <> m implies b₃ * (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 b₁ being invertible Matrix of n,F_Real st
( b₁ * (i,i) = cos r & b₁ * (j,j) = cos r & b₁ * (i,j) = sin r & b₁ * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b₁ holds
( ( k = m & k <> i & k <> j implies b₁ * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b₁ * (k,m) = 0. F_Real ) ) ) )

proof end;

uniqueness
for b₁, b₂ being invertible Matrix of n,F_Real st b₁ * (i,i) = cos r & b₁ * (j,j) = cos r & b₁ * (i,j) = sin r & b₁ * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b₁ holds
( ( k = m & k <> i & k <> j implies b₁ * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b₁ * (k,m) = 0. F_Real ) ) ) & b₂ * (i,i) = cos r & b₂ * (j,j) = cos r & b₂ * (i,j) = sin r & b₂ * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b₂ holds
( ( k = m & k <> i & k <> j implies b₂ * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b₂ * (k,m) = 0. F_Real ) ) ) holds
b₁ = b₂

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 b₅ being invertible Matrix of n,F_Real holds
( b₅ = Rotation (i,j,n,r) iff ( b₅ * (i,i) = cos r & b₅ * (j,j) = cos r & b₅ * (i,j) = sin r & b₅ * (j,i) = - (sin r) & ( for k, m being Nat st [k,m] in Indices b₅ holds
( ( k = m & k <> i & k <> j implies b₅ * (k,k) = 1. F_Real ) & ( k <> m & {k,m} <> {i,j} implies b₅ * (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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ 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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ = f * g holds
b₁ 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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ is base_rotation holds
( b₁ is homogeneous & b₁ is additive & b₁ is rotation & b₁ 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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ = f * g holds
b₁ 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 b₁ being Matrix of n,F_Real st f = Mx2Tran b₁

proof end;

uniqueness
for b₁, b₂ being Matrix of n,F_Real st f = Mx2Tran b₁ & f = Mx2Tran b₂ holds
b₁ = b₂ 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 b₃ being Matrix of n,F_Real holds
( b₃ = AutMt f iff f = Mx2Tran b₃ );

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 b₁ being Function of (TOP-REAL n),(TOP-REAL n) st b₁ is homogeneous & b₁ is additive & b₁ is rotation holds
b₁ 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;