let n be Nat; for M being Matrix of n,F_Real st Mx2Tran M is base_rotation holds
Det M = 1. F_Real
let M be Matrix of n,F_Real; ( Mx2Tran M is base_rotation implies Det M = 1. F_Real )
set TR = TOP-REAL n;
set G = GFuncs the carrier of (TOP-REAL n);
assume
Mx2Tran M is base_rotation
; Det M = 1. F_Real
then consider F being FinSequence of (GFuncs the carrier of (TOP-REAL n)) such that
A1:
Mx2Tran M = 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)) )
;
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
Det M = 1. F_Real ) ) );
A3:
for m being Nat st S1[m] holds
S1[m + 1]
proof
let m be
Nat;
( S1[m] implies S1[m + 1] )
A4:
(
n = 0 implies
n = 0 )
;
set m1 =
m + 1;
assume A5:
S1[
m]
;
S1[m + 1]
assume A6:
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
Det M = 1. F_Real ) )
then reconsider P =
Product (F | m) as
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n) by A5, NAT_1:13;
set R =
AutMt P;
A7:
(
width (AutMt P) = n &
len (AutMt P) = n )
by MATRIX_0:24;
1
<= m + 1
by NAT_1:11;
then A8:
m + 1
in dom F
by A6, FINSEQ_3:25;
then consider i,
j being
Nat,
r being
Real such that A9:
( 1
<= i &
i < j &
j <= n )
and A10:
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 A8, A10, FINSEQ_5:10;
then A11:
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 A9, Th28;
hence
Product (F | (m + 1)) is
base_rotation Function of
(TOP-REAL n),
(TOP-REAL n)
by A11;
for M being Matrix of n,F_Real st Mx2Tran M = Product (F | (m + 1)) holds
Det M = 1. F_Real
A12:
(
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 Det M = 1. F_Real )
assume A13:
Mx2Tran M = Product (F | (m + 1))
;
Det M = 1. F_Real
Mx2Tran M =
(Mx2Tran (Rotation (i,j,n,r))) * (Mx2Tran (AutMt P))
by A11, A13, Def6
.=
Mx2Tran ((AutMt P) * (Rotation (i,j,n,r)))
by A4, A12, A7, MATRTOP1:32
;
then A14:
M = (AutMt P) * (Rotation (i,j,n,r))
by MATRTOP1:34;
P = Mx2Tran (AutMt P)
by Def6;
then A15:
Det (AutMt P) = 1. F_Real
by A5, A6, NAT_1:13;
(
len (AutMt P) = n &
Det (Rotation (i,j,n,r)) = 1. F_Real )
by A9, Th13, MATRIX_0:25;
hence Det M =
(1. F_Real) * (1. F_Real)
by A14, A15, MATRIXR2:45
.=
(1. F_Real) * 1
.=
1. F_Real
;
verum
end;
A16:
F | (len F) = F
by FINSEQ_1:58;
A17:
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
Det M = 1. F_Real ) )
A18:
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 A19:
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
Det M = 1. F_Real
(
n = 0 or
n >= 1 )
by NAT_1:14;
then A20:
( (
Det (1. (F_Real,n)) = 1_ F_Real &
n >= 1 ) or (
Det (1. (F_Real,n)) = 1. F_Real &
n = 0 ) )
by MATRIXR2:41, MATRIX_7:16;
let M be
Matrix of
n,
F_Real;
( Mx2Tran M = Product (F | 0) implies Det M = 1. F_Real )
thus
(
Mx2Tran M = Product (F | 0) implies
Det M = 1. F_Real )
by A18, A19, A20, MATRTOP1:34;
verum
end;
for m being Nat holds S1[m]
from NAT_1:sch 2(A17, A3);
hence
Det M = 1. F_Real
by A1, A16; verum