let n be Nat; 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); ( 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
; 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 S1[ 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 S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
A5:
(
n = 0 implies
n = 0 )
;
set m1 =
m + 1;
assume A6:
S1[
m]
;
S1[m + 1]
assume A7:
m + 1
<= len F
;
( 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;
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;
( Mx2Tran M = Product (F | (m + 1)) implies M is Orthogonal )
assume A14:
Mx2Tran M = Product (F | (m + 1))
;
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;
verum
end;
A17:
F | (len F) = F
by FINSEQ_1:58;
A18:
S1[ 0 ]
proof
assume
0 <= len F
;
( 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)
;
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;
( 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;
verum
end;
for m being Nat holds S1[m]
from NAT_1:sch 2(A18, A4);
hence
AutMt f is Orthogonal
by A1, A17, A3; verum