let n be Nat; :: thesis: for f being additive homogeneous Function of (TOP-REAL n),(TOP-REAL n) st f is base_rotation holds

AutMt f is Orthogonal

let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is base_rotation implies AutMt f is Orthogonal )

set TR = TOP-REAL n;

set G = GFuncs the carrier of (TOP-REAL n);

assume f is base_rotation ; :: thesis: AutMt f is Orthogonal

then consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that

A1: f = Product F and

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

A3: f = Mx2Tran (AutMt f) by Def6;

defpred S_{1}[ Nat] means ( $1 <= len F implies ( Product (F | $1) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | $1) holds

M is Orthogonal ) ) );

A4: for m being Nat st S_{1}[m] holds

S_{1}[m + 1]

A18: S_{1}[ 0 ]
_{1}[m]
from NAT_1:sch 2(A18, A4);

hence AutMt f is Orthogonal by A1, A17, A3; :: thesis: verum

AutMt f is Orthogonal

let f be additive homogeneous Function of (TOP-REAL n),(TOP-REAL n); :: thesis: ( f is base_rotation implies AutMt f is Orthogonal )

set TR = TOP-REAL n;

set G = GFuncs the carrier of (TOP-REAL n);

assume f is base_rotation ; :: thesis: AutMt f is Orthogonal

then consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that

A1: f = Product F and

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

A3: f = Mx2Tran (AutMt f) by Def6;

defpred S

M is Orthogonal ) ) );

A4: for m being Nat st S

S

proof

A17:
F | (len F) = F
by FINSEQ_1:58;
let m be Nat; :: thesis: ( S_{1}[m] implies S_{1}[m + 1] )

A5: ( n = 0 implies n = 0 ) ;

set m1 = m + 1;

assume A6: S_{1}[m]
; :: thesis: S_{1}[m + 1]

assume A7: m + 1 <= len F ; :: thesis: ( Product (F | (m + 1)) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds

M is Orthogonal ) )

then reconsider P = Product (F | m) as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A6, NAT_1:13;

set R = AutMt P;

A8: ( width (AutMt P) = n & len (AutMt P) = n ) by MATRIX_0:24;

1 <= m + 1 by NAT_1:11;

then A9: m + 1 in dom F by A7, FINSEQ_3:25;

then consider i, j being Nat, r being Real such that

A10: ( 1 <= i & i < j & j <= n ) and

A11: F . (m + 1) = Mx2Tran (Rotation (i,j,n,r)) by A2;

set O = Rotation (i,j,n,r);

reconsider MO = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of (TOP-REAL n)) by MONOID_0:73;

F | (m + 1) = (F | m) ^ <*MO*> by A9, A11, FINSEQ_5:10;

then A12: Product (F | (m + 1)) = (Product (F | m)) * MO by GROUP_4:6

.= (Mx2Tran (Rotation (i,j,n,r))) * P by MONOID_0:70 ;

Mx2Tran (Rotation (i,j,n,r)) is base_rotation by A10, Th28;

hence Product (F | (m + 1)) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A12; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds

M is Orthogonal

A13: ( width (Rotation (i,j,n,r)) = n & len (Rotation (i,j,n,r)) = n ) by MATRIX_0:24;

let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | (m + 1)) implies M is Orthogonal )

assume A14: Mx2Tran M = Product (F | (m + 1)) ; :: thesis: M is Orthogonal

Mx2Tran M = (Mx2Tran (Rotation (i,j,n,r))) * (Mx2Tran (AutMt P)) by A12, A14, Def6

.= Mx2Tran ((AutMt P) * (Rotation (i,j,n,r))) by A5, A13, A8, MATRTOP1:32 ;

then A15: M = (AutMt P) * (Rotation (i,j,n,r)) by MATRTOP1:34;

P = Mx2Tran (AutMt P) by Def6;

then A16: ( AutMt P is Orthogonal & n > i ) by A10, A6, A7, NAT_1:13, XXREAL_0:2;

( len (AutMt P) = n & Rotation (i,j,n,r) is Orthogonal & n > 0 ) by A10, Th19, MATRIX_0:25;

hence M is Orthogonal by A15, A16, MATRIX_6:46; :: thesis: verum

end;A5: ( n = 0 implies n = 0 ) ;

set m1 = m + 1;

assume A6: S

assume A7: m + 1 <= len F ; :: thesis: ( Product (F | (m + 1)) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds

M is Orthogonal ) )

then reconsider P = Product (F | m) as base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A6, NAT_1:13;

set R = AutMt P;

A8: ( width (AutMt P) = n & len (AutMt P) = n ) by MATRIX_0:24;

1 <= m + 1 by NAT_1:11;

then A9: m + 1 in dom F by A7, FINSEQ_3:25;

then consider i, j being Nat, r being Real such that

A10: ( 1 <= i & i < j & j <= n ) and

A11: F . (m + 1) = Mx2Tran (Rotation (i,j,n,r)) by A2;

set O = Rotation (i,j,n,r);

reconsider MO = Mx2Tran (Rotation (i,j,n,r)) as Element of (GFuncs the carrier of (TOP-REAL n)) by MONOID_0:73;

F | (m + 1) = (F | m) ^ <*MO*> by A9, A11, FINSEQ_5:10;

then A12: Product (F | (m + 1)) = (Product (F | m)) * MO by GROUP_4:6

.= (Mx2Tran (Rotation (i,j,n,r))) * P by MONOID_0:70 ;

Mx2Tran (Rotation (i,j,n,r)) is base_rotation by A10, Th28;

hence Product (F | (m + 1)) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) by A12; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds

M is Orthogonal

A13: ( width (Rotation (i,j,n,r)) = n & len (Rotation (i,j,n,r)) = n ) by MATRIX_0:24;

let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | (m + 1)) implies M is Orthogonal )

assume A14: Mx2Tran M = Product (F | (m + 1)) ; :: thesis: M is Orthogonal

Mx2Tran M = (Mx2Tran (Rotation (i,j,n,r))) * (Mx2Tran (AutMt P)) by A12, A14, Def6

.= Mx2Tran ((AutMt P) * (Rotation (i,j,n,r))) by A5, A13, A8, MATRTOP1:32 ;

then A15: M = (AutMt P) * (Rotation (i,j,n,r)) by MATRTOP1:34;

P = Mx2Tran (AutMt P) by Def6;

then A16: ( AutMt P is Orthogonal & n > i ) by A10, A6, A7, NAT_1:13, XXREAL_0:2;

( len (AutMt P) = n & Rotation (i,j,n,r) is Orthogonal & n > 0 ) by A10, Th19, MATRIX_0:25;

hence M is Orthogonal by A15, A16, MATRIX_6:46; :: thesis: verum

A18: S

proof

for m being Nat holds S
assume
0 <= len F
; :: thesis: ( Product (F | 0) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) & ( for M being Matrix of n,F_Real st Mx2Tran M = Product (F | 0) holds

M is Orthogonal ) )

A19: Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n) by MATRTOP1:33;

F | 0 = <*> the carrier of (GFuncs the carrier of (TOP-REAL n)) ;

then A20: Product (F | 0) = 1_ (GFuncs the carrier of (TOP-REAL n)) by GROUP_4:8

.= the_unity_wrt the multF of (GFuncs the carrier of (TOP-REAL n)) by GROUP_1:22

.= id (TOP-REAL n) by MONOID_0:75 ;

hence Product (F | 0) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) ; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | 0) holds

M is Orthogonal

A21: 1. (F_Real,n) is Orthogonal by MATRIX_6:58;

let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | 0) implies M is Orthogonal )

thus ( Mx2Tran M = Product (F | 0) implies M is Orthogonal ) by A19, A20, A21, MATRTOP1:34; :: thesis: verum

end;M is Orthogonal ) )

A19: Mx2Tran (1. (F_Real,n)) = id (TOP-REAL n) by MATRTOP1:33;

F | 0 = <*> the carrier of (GFuncs the carrier of (TOP-REAL n)) ;

then A20: Product (F | 0) = 1_ (GFuncs the carrier of (TOP-REAL n)) by GROUP_4:8

.= the_unity_wrt the multF of (GFuncs the carrier of (TOP-REAL n)) by GROUP_1:22

.= id (TOP-REAL n) by MONOID_0:75 ;

hence Product (F | 0) is base_rotation Function of (TOP-REAL n),(TOP-REAL n) ; :: thesis: for M being Matrix of n,F_Real st Mx2Tran M = Product (F | 0) holds

M is Orthogonal

A21: 1. (F_Real,n) is Orthogonal by MATRIX_6:58;

let M be Matrix of n,F_Real; :: thesis: ( Mx2Tran M = Product (F | 0) implies M is Orthogonal )

thus ( Mx2Tran M = Product (F | 0) implies M is Orthogonal ) by A19, A20, A21, MATRTOP1:34; :: thesis: verum

hence AutMt f is Orthogonal by A1, A17, A3; :: thesis: verum