let K be Field; for R being FinSequence_of_Square-Matrix of K holds Det (block_diagonal (R,(0. K))) = Product (Det R)
let R be FinSequence_of_Square-Matrix of K; Det (block_diagonal (R,(0. K))) = Product (Det R)
defpred S1[ Nat] means for R being FinSequence_of_Square-Matrix of K st len R = $1 holds
Det (block_diagonal (R,(0. K))) = Product (Det R);
A1:
for n being Nat st S1[n] holds
S1[n + 1]
proof
let n be
Nat;
( S1[n] implies S1[n + 1] )
assume A2:
S1[
n]
;
S1[n + 1]
set n1 =
n + 1;
let R be
FinSequence_of_Square-Matrix of
K;
( len R = n + 1 implies Det (block_diagonal (R,(0. K))) = Product (Det R) )
assume A3:
len R = n + 1
;
Det (block_diagonal (R,(0. K))) = Product (Det R)
set Rn =
R | n;
A4:
len (R | n) = n
by A3, FINSEQ_1:59, NAT_1:11;
set R1 =
R . (n + 1);
set bR =
block_diagonal (
(R | n),
(0. K));
A5:
R = (R | n) ^ <*(R . (n + 1))*>
by A3, FINSEQ_3:55;
then A6:
block_diagonal (
R,
(0. K))
= block_diagonal (
<*(block_diagonal ((R | n),(0. K))),(R . (n + 1))*>,
(0. K))
by Th35;
Sum (Len <*(block_diagonal ((R | n),(0. K))),(R . (n + 1))*>) =
(len (block_diagonal ((R | n),(0. K)))) + (len (R . (n + 1)))
by Th16
.=
(Sum (Len (R | n))) + (len (R . (n + 1)))
by Def5
.=
Sum ((Len (R | n)) ^ <*(len (R . (n + 1)))*>)
by RVSUM_1:74
.=
Sum ((Len (R | n)) ^ (Len <*(R . (n + 1))*>))
by Th15
.=
Sum (Len R)
by A5, Th14
;
hence Det (block_diagonal (R,(0. K))) =
(Det (block_diagonal ((R | n),(0. K)))) * (Det (R . (n + 1)))
by A6, Th52
.=
(Product (Det (R | n))) * (Det (R . (n + 1)))
by A2, A4
.=
Product ((Det (R | n)) ^ <*(Det (R . (n + 1)))*>)
by GROUP_4:6
.=
Product ((Det (R | n)) ^ (Det <*(R . (n + 1))*>))
by Th49
.=
Product (Det R)
by A5, Th50
;
verum
end;
A7:
S1[ 0 ]
for n being Nat holds S1[n]
from NAT_1:sch 2(A7, A1);
hence
Det (block_diagonal (R,(0. K))) = Product (Det R)
; verum