let n be Nat; :: thesis: for K being Field
for G being FinSequence_of_Matrix of K st Len G <> Width G holds
for M being Matrix of n,K st M = block_diagonal (G,(0. K)) holds
Det M = 0. K
let K be Field; :: thesis: for G being FinSequence_of_Matrix of K st Len G <> Width G holds
for M being Matrix of n,K st M = block_diagonal (G,(0. K)) holds
Det M = 0. K
let G be FinSequence_of_Matrix of K; :: thesis: ( Len G <> Width G implies for M being Matrix of n,K st M = block_diagonal (G,(0. K)) holds
Det M = 0. K )
set B = block_diagonal (G,(0. K));
defpred S₁[ Nat] means ( $1 in Seg (len G) & (Len G) . $1 <> (Width G) . $1 );
A1: Seg (len G) = dom G by FINSEQ_1:def 3;
assume Len G <> Width G ; :: thesis: for M being Matrix of n,K st M = block_diagonal (G,(0. K)) holds
Det M = 0. K
then A2: ex k being Nat st S₁[k] by FINSEQ_2:119;
consider k being Nat such that
A3: S₁[k] and
A4: for n being Nat st S₁[n] holds
k <= n from NAT_1:sch 5(A2);
1 <= k by A3, FINSEQ_1:1;
then reconsider k1 = k - 1 as Element of NAT by NAT_1:21;
set Gk = G | k1;
A5: len G = len (Width G) by CARD_1:def 7;
then k in dom (Width G) by A3, FINSEQ_1:def 3;
then A6: width (G . k) = (Width G) . k by Def4;
set bGk = block_diagonal ((G | k1),(0. K));
set bGk1 = block_diagonal ((G /^ k),(0. K));
set bGG = block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K));
k1 + 1 <= len G by A3, FINSEQ_1:1;
then A7: k1 < len G by NAT_1:13;
then len ((Width G) | k1) = k1 by A5, FINSEQ_1:59;
then A8: dom ((Width G) | k1) = Seg k1 by FINSEQ_1:def 3;
A9: len G = len (Len G) by CARD_1:def 7;
then len ((Len G) | k1) = k1 by A7, FINSEQ_1:59;
then A10: dom ((Len G) | k1) = Seg k1 by FINSEQ_1:def 3;
A11: Seg k1 c= Seg (len G) by A7, FINSEQ_1:5;

A12: now :: thesis: for j being Nat st j in Seg k1 holds
(Len (G | k1)) . j = (Width (G | k1)) . j

let j be Nat; :: thesis: ( j in Seg k1 implies (Len (G | k1)) . j = (Width (G | k1)) . j )
assume A13: j in Seg k1 ; :: thesis: (Len (G | k1)) . j = (Width (G | k1)) . j
j <= k1 by A13, FINSEQ_1:1;
then j < k1 + 1 by NAT_1:13;
then A14: (Len G) . j = (Width G) . j by A4, A11, A13;
thus (Len (G | k1)) . j = ((Len G) | k1) . j by Th17
.= (Len G) . j by A10, A13, FUNCT_1:47
.= ((Width G) | k1) . j by A8, A13, A14, FUNCT_1:47
.= (Width (G | k1)) . j by Th21 ; :: thesis: verum

end;

len (G | k1) = k1 by A7, FINSEQ_1:59;
then Len (G | k1) = Width (G | k1) by A12, FINSEQ_2:119;
then reconsider bGk = block_diagonal ((G | k1),(0. K)) as Matrix of Sum (Len (G | k1)),K ;
let M be Matrix of n,K; :: thesis: ( M = block_diagonal (G,(0. K)) implies Det M = 0. K )
assume M = block_diagonal (G,(0. K)) ; :: thesis: Det M = 0. K
then A15: M = block_diagonal (((G | (k1 + 1)) ^ (G /^ k)),(0. K)) by RFINSEQ:8
.= block_diagonal ((((G | k1) ^ <*(G . k)*>) ^ (G /^ k)),(0. K)) by A3, A1, FINSEQ_5:10
.= block_diagonal (((G | k1) ^ (<*(G . k)*> ^ (G /^ k))),(0. K)) by FINSEQ_1:32
.= block_diagonal ((<*bGk*> ^ (<*(G . k)*> ^ (G /^ k))),(0. K)) by Th35
.= block_diagonal ((<*bGk*> ^ <*(block_diagonal ((<*(G . k)*> ^ (G /^ k)),(0. K)))*>),(0. K)) by Th36
.= block_diagonal (<*bGk,(block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))*>,(0. K)) by Th36 ;
then A16: len M = Sum (Len <*bGk,(block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))*>) by Def5;
A17: Sum (Width <*bGk,(block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))*>) = (width bGk) + (width (block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))) by Th20;
A18: width bGk = Sum (Len (G | k1)) by MATRIX_0:24;
A19: len bGk = Sum (Len (G | k1)) by Def5;
A20: width M = n by MATRIX_0:24;
A21: Sum (Len <*bGk,(block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))*>) = (len bGk) + (len (block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))) by Th16;
A22: len M = n by MATRIX_0:24;
width M = Sum (Width <*bGk,(block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)))*>) by A15, Def5;
then reconsider bGG9 = block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K)) as Matrix of len (block_diagonal (<*(G . k),(block_diagonal ((G /^ k),(0. K)))*>,(0. K))),K by A16, A22, A20, A21, A19, A18, A17, MATRIX_0:51;
k in dom (Len G) by A3, A9, FINSEQ_1:def 3;
then len (G . k) = (Len G) . k by Def3;
then Det bGG9 = 0. K by A3, A6, Th54;
hence Det M = (Det bGk) * (0. K) by A15, A16, A22, Th52
.= 0. K ;
:: thesis: verum