let K be Field; for R1, R2 being FinSequence_of_Square-Matrix of K holds Det (R1 ^ R2) = (Det R1) ^ (Det R2)
let R1, R2 be FinSequence_of_Square-Matrix of K; Det (R1 ^ R2) = (Det R1) ^ (Det R2)
set R12 = R1 ^ R2;
A1:
len (R1 ^ R2) = (len R1) + (len R2)
by FINSEQ_1:22;
A2:
len ((Det R1) ^ (Det R2)) = (len R1) + (len R2)
by CARD_1:def 7;
len R2 = len (Det R2)
by CARD_1:def 7;
then A3:
dom (Det R2) = dom R2
by FINSEQ_3:29;
A4:
len R1 = len (Det R1)
by CARD_1:def 7;
then A5:
dom (Det R1) = dom R1
by FINSEQ_3:29;
A6:
len (Det (R1 ^ R2)) = len (R1 ^ R2)
by CARD_1:def 7;
then A7:
dom ((Det R1) ^ (Det R2)) = dom (Det (R1 ^ R2))
by A1, A2, FINSEQ_3:29;
now for k being Nat st 1 <= k & k <= (len R1) + (len R2) holds
(Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . klet k be
Nat;
( 1 <= k & k <= (len R1) + (len R2) implies (Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k )assume that A8:
1
<= k
and A9:
k <= (len R1) + (len R2)
;
(Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . kA10:
k in dom ((Det R1) ^ (Det R2))
by A2, A8, A9, FINSEQ_3:25;
now ((Det R1) ^ (Det R2)) . k = (Det (R1 ^ R2)) . kper cases
( k in dom (Det R1) or ex n being Nat st
( n in dom (Det R2) & k = (len (Det R1)) + n ) )
by A10, FINSEQ_1:25;
suppose
ex
n being
Nat st
(
n in dom (Det R2) &
k = (len (Det R1)) + n )
;
((Det R1) ^ (Det R2)) . k = (Det (R1 ^ R2)) . kthen consider n being
Nat such that A13:
n in dom (Det R2)
and A14:
k = (len R1) + n
by A4;
A15:
len (R2 . n) = len ((R1 ^ R2) . k)
by A3, A13, A14, FINSEQ_1:def 7;
thus ((Det R1) ^ (Det R2)) . k =
(Det R2) . n
by A4, A13, A14, FINSEQ_1:def 7
.=
Det (R2 . n)
by A13, Def7
.=
Det ((R1 ^ R2) . k)
by A3, A13, A14, A15, FINSEQ_1:def 7
.=
(Det (R1 ^ R2)) . k
by A7, A10, Def7
;
verum end; hence
(Det (R1 ^ R2)) . k = ((Det R1) ^ (Det R2)) . k
;
verum end;
hence
Det (R1 ^ R2) = (Det R1) ^ (Det R2)
by A6, A1, A2; verum