let n be Nat; :: thesis: for K being Field
for A1, A2 being Matrix of K
for N being Matrix of n,K st len A1 <> width A1 & N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
let K be Field; :: thesis: for A1, A2 being Matrix of K
for N being Matrix of n,K st len A1 <> width A1 & N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
let A1, A2 be Matrix of K; :: thesis: for N being Matrix of n,K st len A1 <> width A1 & N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
let N be Matrix of n,K; :: thesis: ( len A1 <> width A1 & N = block_diagonal (<*A1,A2*>,(0. K)) implies Det N = 0. K )
defpred S₁[ Nat] means for A1 being Matrix of K st len A1 <> width A1 & width A1 = $1 holds
for n being Nat
for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K;
A1: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A2: S₁[k] ; :: thesis: S₁[k + 1]
set k1 = k + 1;
let A1 be Matrix of K; :: thesis: ( len A1 <> width A1 & width A1 = k + 1 implies for n being Nat
for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K )
assume that
A3: len A1 <> width A1 and
A4: width A1 = k + 1 ; :: thesis: for n being Nat
for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
A5: Sum (Len <*A1,A2*>) = (len A1) + (len A2) by Th16;
1 <= k + 1 by NAT_1:14;
then A6: 1 in Seg (width A1) by A4;
A7: len (A1 ^ A2) = (len A1) + (len A2) by FINSEQ_1:22;
A8: Sum (Width <*A1,A2*>) = (width A1) + (width A2) by Th20;
let n be Nat; :: thesis: for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
let N be Matrix of n,K; :: thesis: ( N = block_diagonal (<*A1,A2*>,(0. K)) implies Det N = 0. K )
assume A9: N = block_diagonal (<*A1,A2*>,(0. K)) ; :: thesis: Det N = 0. K
A10: len N = Sum (Len <*A1,A2*>) by A9, Def5;
set C = LaplaceExpC (N,1);
A11: n = len N by MATRIX_0:24;
then A12: len (LaplaceExpC (N,1)) = len N by LAPLACE:def 8;
A13: len A1 <> 0 by A3, MATRIX_0:def 3;
then A14: 1 + 0 <= len N by A10, A5, NAT_1:14;
then A15: 1 in Seg n by A11;
A16: width N = Sum (Width <*A1,A2*>) by A9, Def5;
set L0 = (len N) |-> (0. K);
A17: n = width N by MATRIX_0:24;
A18: len A1 >= 1 by A13, NAT_1:14;

A19: now :: thesis: for i being Nat st 1 <= i & i <= len N holds
(LaplaceExpC (N,1)) . i = ((len N) |-> (0. K)) . i

let i be Nat; :: thesis: ( 1 <= i & i <= len N implies (LaplaceExpC (N,1)) . i = ((len N) |-> (0. K)) . i )
assume that
A20: 1 <= i and
A21: i <= len N ; :: thesis: (LaplaceExpC (N,1)) . i = ((len N) |-> (0. K)) . i
A22: i in Seg n by A11, A20, A21;
i in dom (LaplaceExpC (N,1)) by A12, A20, A21, FINSEQ_3:25;
then A23: (LaplaceExpC (N,1)) . i = (N * (i,1)) * (Cofactor (N,i,1)) by LAPLACE:def 8;
A24: N * (i,1) = (Line (N,i)) . 1 by A17, A15, MATRIX_0:def 7;
A25: i in dom (A1 ^ A2) by A10, A5, A7, A20, A21, FINSEQ_3:25;

now :: thesis: 0. K = (LaplaceExpC (N,1)) . i

per cases ( i in dom A1 or ex j being Nat st
( j in dom A2 & i = (len A1) + j ) ) by A25, FINSEQ_1:25;

suppose A26: i in dom A1 ; :: thesis: 0. K = (LaplaceExpC (N,1)) . i

now :: thesis: Det (Delete (N,i,1)) = 0. K

per cases ( len A1 = 1 or len A1 > 1 ) by A18, XXREAL_0:1;

suppose A27: len A1 = 1 ; :: thesis: Det (Delete (N,i,1)) = 0. K

then k <> 0 by A3, A4;
then k in Seg k by FINSEQ_1:3;
then A28: 1 <= k by FINSEQ_1:1;
then 1 + 1 <= k + 1 by XREAL_1:7;
then A29: 2 in Seg (k + 1) ;
A30: 1 <= i by A26, FINSEQ_3:25;
i <= 1 by A26, A27, FINSEQ_3:25;
then A31: i = 1 by A30, XXREAL_0:1;
set Q = (Seg n) \ {1};
Seg 1 c= Seg n by A11, A14, FINSEQ_1:5;
then A32: card ((Seg n) \ {1}) = (card (Seg n)) - (card (Seg 1)) by CARD_2:44, FINSEQ_1:2
.= (card (Seg n)) - 1 by FINSEQ_1:57
.= n - 1 by FINSEQ_1:57
.= k + (width A2) by A4, A17, A16, A8 ;
then A33: card ((Seg n) \ {1}) = ((k + (width A2)) + 1) -' 1 by NAT_D:34
.= n -' 1 by A4, A9, A17, A8, Def5 ;
1 + 0 <= card ((Seg n) \ {1}) by A32, A28, XREAL_1:7;
then A34: 1 in Seg (card ((Seg n) \ {1})) ;
Delete (N,i,1) = Deleting (N,i,1) by A15, A22, LAPLACE:def 1
.= Segm (N,((Seg n) \ {1}),((Seg n) \ {1})) by A31, MATRIX13:58 ;
then A35: Col ((Delete (N,i,1)),1) = (Col (N,((Sgm ((Seg n) \ {1})) . 1))) * (Sgm ((Seg n) \ {1})) by A11, A34, MATRIX13:49, XBOOLE_1:36;

now :: thesis: for j being Element of NAT st j in Seg (n -' 1) holds
(Col ((Delete (N,i,1)),1)) . j = 0. K

A36: dom ((len A2) |-> (0. K)) = Seg (len A2) by FINSEQ_2:124;
A37: n = 1 + (card ((Seg n) \ {1})) by A4, A9, A17, A8, A32, Def5;
A38: len (Col (A1,2)) = 1 by A27, CARD_1:def 7;
let j be Element of NAT ; :: thesis: ( j in Seg (n -' 1) implies (Col ((Delete (N,i,1)),1)) . j = 0. K )
assume A39: j in Seg (n -' 1) ; :: thesis: (Col ((Delete (N,i,1)),1)) . j = 0. K
dom (Sgm ((Seg n) \ {1})) = Seg (card ((Seg n) \ {1})) by FINSEQ_3:40;
hence (Col ((Delete (N,i,1)),1)) . j = (Col (N,((Sgm ((Seg n) \ {1})) . 1))) . ((Sgm ((Seg n) \ {1})) . j) by A33, A35, A39, FUNCT_1:13
.= (Col (N,(1 + 1))) . ((Sgm ((Seg n) \ {1})) . j) by A34, A37, FINSEQ_1:2, MATRIX15:8
.= (Col (N,(1 + 1))) . (j + 1) by A33, A39, A37, FINSEQ_1:2, MATRIX15:8
.= ((Col (A1,2)) ^ ((len A2) |-> (0. K))) . (j + 1) by A4, A9, A29, Th24
.= ((len A2) |-> (0. K)) . j by A4, A10, A11, A17, A16, A5, A8, A27, A32, A33, A39, A38, A36, FINSEQ_1:def 7
.= 0. K by A4, A10, A11, A17, A16, A5, A8, A27, A32, A33, A39, FINSEQ_2:57 ;
:: thesis: verum

end;

hence Det (Delete (N,i,1)) = 0. K by A33, A34, MATRIX_9:53; :: thesis: verum

end;

suppose A40: len A1 > 1 ; :: thesis: 0. K = Det (Delete (N,i,1))

set DL = DelLine (A1,i);
set DC = DelCol ((DelLine (A1,i)),1);
A41: (k + 1) -' 1 = k by NAT_D:34;
reconsider L1 = (len A1) - 1 as Element of NAT by A40, NAT_1:21;
A42: len (DelCol ((DelLine (A1,i)),1)) = len (DelLine (A1,i)) by MATRIX_0:def 13;
A43: width A1 = width (DelLine (A1,i)) by A40, LAPLACE:4;
then A44: width (DelCol ((DelLine (A1,i)),1)) = (width A1) -' 1 by A6, LAPLACE:3;
A45: Delete (N,i,1) = Deleting (N,i,1) by A15, A22, LAPLACE:def 1
.= DelCol ((DelLine (N,i)),1)
.= DelCol ((block_diagonal ((<*(DelLine (A1,i))*> ^ <*A2*>),(0. K))),1) by A9, A26, A43, Th41
.= block_diagonal (<*(DelCol ((DelLine (A1,i)),1)),A2*>,(0. K)) by A6, A43, Th43 ;
len A1 = L1 + 1 ;
then len (DelCol ((DelLine (A1,i)),1)) <> width (DelCol ((DelLine (A1,i)),1)) by A3, A4, A26, A44, A42, A41, FINSEQ_3:109;
hence 0. K = Det (Delete (N,i,1)) by A2, A4, A44, A45, NAT_D:34; :: thesis: verum

end;

end;

end;

then 0. K = Cofactor (N,i,1) ;
hence 0. K = (LaplaceExpC (N,1)) . i by A23; :: thesis: verum

end;

suppose A46: ex j being Nat st
( j in dom A2 & i = (len A1) + j ) ; :: thesis: 0. K = (LaplaceExpC (N,1)) . i

A47: dom ((width A1) |-> (0. K)) = Seg (width A1) by FINSEQ_2:124;
consider j being Nat such that
A48: j in dom A2 and
A49: i = (len A1) + j by A46;
N * (i,1) = (((width A1) |-> (0. K)) ^ (Line (A2,j))) . 1 by A9, A24, A48, A49, Th23
.= ((width A1) |-> (0. K)) . 1 by A6, A47, FINSEQ_1:def 7
.= 0. K by A6, FINSEQ_2:57 ;
hence 0. K = (LaplaceExpC (N,1)) . i by A23; :: thesis: verum

end;

end;

end;

hence (LaplaceExpC (N,1)) . i = ((len N) |-> (0. K)) . i by A11, A22, FINSEQ_2:57; :: thesis: verum

end;

len ((len N) |-> (0. K)) = len N by CARD_1:def 7;
then LaplaceExpC (N,1) = (len N) |-> (0. K) by A12, A19;
then LaplaceExpC (N,1) = (len N) |-> ((0. K) * (0. K)) ;
then Sum (LaplaceExpC (N,1)) = Sum ((0. K) * ((len N) |-> (0. K))) by FVSUM_1:53
.= (0. K) * (Sum ((len N) |-> (0. K))) by FVSUM_1:73
.= 0. K ;
hence Det N = 0. K by A15, LAPLACE:27; :: thesis: verum

end;

A50: S₁[ 0 ]

proof

let A1 be Matrix of K; :: thesis: ( len A1 <> width A1 & width A1 = 0 implies for n being Nat
for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K )
assume that
A51: len A1 <> width A1 and
A52: width A1 = 0 ; :: thesis: for n being Nat
for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
A53: len A1 in Seg (len A1) by A51, A52, FINSEQ_1:3;
A54: Sum (Width <*A1,A2*>) = (width A1) + (width A2) by Th20;
A55: Sum (Len <*A1,A2*>) = (len A1) + (len A2) by Th16;
A56: len A1 <= (len A1) + (len A2) by NAT_1:11;
let n be Nat; :: thesis: for N being Matrix of n,K st N = block_diagonal (<*A1,A2*>,(0. K)) holds
Det N = 0. K
let N be Matrix of n,K; :: thesis: ( N = block_diagonal (<*A1,A2*>,(0. K)) implies Det N = 0. K )
assume A57: N = block_diagonal (<*A1,A2*>,(0. K)) ; :: thesis: Det N = 0. K
A58: width N = Sum (Width <*A1,A2*>) by A57, Def5;
len N = Sum (Len <*A1,A2*>) by A57, Def5;
then A59: Seg (len A1) c= Seg (len N) by A55, A56, FINSEQ_1:5;
A60: n = len N by MATRIX_0:def 2;
dom A1 = Seg (len A1) by FINSEQ_1:def 3;
then Line (N,(len A1)) = (Line (A1,(len A1))) ^ ((width A2) |-> (0. K)) by A57, A53, Th23
.= (<*> the carrier of K) ^ ((width A2) |-> (0. K)) by A52
.= (width A2) |-> (0. K) by FINSEQ_1:34
.= (0. K) * (Line (N,(len A1))) by A52, A58, A54, FVSUM_1:58 ;
hence Det N = Det (RLine (N,(len A1),((0. K) * (Line (N,(len A1)))))) by MATRIX11:30
.= (0. K) * (Det N) by A60, A53, A59, MATRIX11:35
.= 0. K ;
:: thesis: verum

end;

for n being Nat holds S₁[n] from NAT_1:sch 2(A50, A1);
hence ( len A1 <> width A1 & N = block_diagonal (<*A1,A2*>,(0. K)) implies Det N = 0. K ) ; :: thesis: verum