let n be Nat; 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; 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; 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; ( len A1 <> width A1 & N = block_diagonal <*A1,A2*>,(0. K) implies Det N = 0. K )
defpred S1[ 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 S1[k] holds
S1[k + 1]
proof
let k be
Nat;
( S1[k] implies S1[k + 1] )
assume A2:
S1[
k]
;
S1[k + 1]
set k1 =
k + 1;
let A1 be
Matrix of
K;
( 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
;
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:35;
A8:
Sum (Width <*A1,A2*>) = (width A1) + (width A2)
by Th20;
let n be
Nat;
for N being Matrix of n,K st N = block_diagonal <*A1,A2*>,(0. K) holds
Det N = 0. Klet N be
Matrix of
n,
K;
( N = block_diagonal <*A1,A2*>,(0. K) implies Det N = 0. K )
assume A9:
N = block_diagonal <*A1,A2*>,
(0. K)
;
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_1:25;
then A12:
len (LaplaceExpC N,1) = len N
by LAPLACE:def 8;
A13:
len A1 <> 0
by A3, MATRIX_1:def 4;
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_1:25;
A18:
len A1 >= 1
by A13, NAT_1:14;
A19:
now let i be
Nat;
( 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
;
(LaplaceExpC N,1) . i = ((len N) |-> (0. K)) . iA22:
i in Seg n
by A11, A20, A21, FINSEQ_1:3;
i in dom (LaplaceExpC N,1)
by A12, A20, A21, FINSEQ_3:27;
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_1:def 8;
A25:
i in dom (A1 ^ A2)
by A10, A5, A7, A20, A21, FINSEQ_3:27;
now per cases
( i in dom A1 or ex j being Nat st
( j in dom A2 & i = (len A1) + j ) )
by A25, FINSEQ_1:38;
suppose A26:
i in dom A1
;
0. K = (LaplaceExpC N,1) . inow per cases
( len A1 = 1 or len A1 > 1 )
by A18, XXREAL_0:1;
suppose A27:
len A1 = 1
;
Det (Delete N,i,1) = 0. Kthen
k <> 0
by A3, A4;
then
k in Seg k
by FINSEQ_1:5;
then A28:
1
<= k
by FINSEQ_1:3;
then
1
+ 1
<= k + 1
by XREAL_1:9;
then A29:
2
in Seg (k + 1)
;
A30:
1
<= i
by A26, FINSEQ_3:27;
i <= 1
by A26, A27, FINSEQ_3:27;
then A31:
i = 1
by A30, XXREAL_0:1;
set Q =
(Seg n) \ {1};
Seg 1
c= Seg n
by A11, A14, FINSEQ_1:7;
then A32:
card ((Seg n) \ {1}) =
(card (Seg n)) - (card (Seg 1))
by CARD_2:63, FINSEQ_1:4
.=
(card (Seg n)) - 1
by FINSEQ_1:78
.=
n - 1
by FINSEQ_1:78
.=
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:9;
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 A36:
dom ((len A2) |-> (0. K)) = Seg (len A2)
by FINSEQ_2:144;
A37:
n = 1
+ (card ((Seg n) \ {1}))
by A4, A9, A17, A8, A32, Def5;
A38:
len (Col A1,2) = 1
by A27, FINSEQ_1:def 18;
let j be
Element of
NAT ;
( j in Seg (n -' 1) implies (Col (Delete N,i,1),1) . j = 0. K )assume A39:
j in Seg (n -' 1)
;
(Col (Delete N,i,1),1) . j = 0. K
dom (Sgm ((Seg n) \ {1})) = Seg (card ((Seg n) \ {1}))
by FINSEQ_3:45, XBOOLE_1:36;
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:23
.=
(Col N,(1 + 1)) . ((Sgm ((Seg n) \ {1})) . j)
by A34, A37, FINSEQ_1:4, MATRIX15:8
.=
(Col N,(1 + 1)) . (j + 1)
by A33, A39, A37, FINSEQ_1:4, 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:71
;
verum end; hence
Det (Delete N,i,1) = 0. K
by A33, A34, MATRIX_9:53;
verum end; suppose A40:
len A1 > 1
;
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_2:def 6;
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
by MATRIX_2:def 8
.=
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:118;
hence
0. K = Det (Delete N,i,1)
by A2, A4, A44, A45, NAT_D:34;
verum end; then
0. K = Cofactor N,
i,1
by VECTSP_1:36;
hence
0. K = (LaplaceExpC N,1) . i
by A23, VECTSP_1:36;
verum suppose A46:
ex
j being
Nat st
(
j in dom A2 &
i = (len A1) + j )
;
0. K = (LaplaceExpC N,1) . iA47:
dom ((width A1) |-> (0. K)) = Seg (width A1)
by FINSEQ_2:144;
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:71
;
hence
0. K = (LaplaceExpC N,1) . i
by A23, VECTSP_1:36;
verum end; hence
(LaplaceExpC N,1) . i = ((len N) |-> (0. K)) . i
by A11, A22, FINSEQ_2:71;
verum end;
len ((len N) |-> (0. K)) = len N
by FINSEQ_1:def 18;
then
LaplaceExpC N,1
= (len N) |-> (0. K)
by A12, A19, FINSEQ_1:18;
then
LaplaceExpC N,1
= (len N) |-> ((0. K) * (0. K))
by VECTSP_1:39;
then Sum (LaplaceExpC N,1) =
Sum ((0. K) * ((len N) |-> (0. K)))
by FVSUM_1:66
.=
(0. K) * (Sum ((len N) |-> (0. K)))
by FVSUM_1:92
.=
0. K
by VECTSP_1:36
;
hence
Det N = 0. K
by A15, LAPLACE:27;
verum
end;
A50:
S1[ 0 ]
proof
let A1 be
Matrix of
K;
( 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
;
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:5;
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;
for N being Matrix of n,K st N = block_diagonal <*A1,A2*>,(0. K) holds
Det N = 0. Klet N be
Matrix of
n,
K;
( N = block_diagonal <*A1,A2*>,(0. K) implies Det N = 0. K )
assume A57:
N = block_diagonal <*A1,A2*>,
(0. K)
;
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:7;
A60:
n = len N
by MATRIX_1:def 3;
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:47
.=
(0. K) * (Line N,(len A1))
by A52, A58, A54, FVSUM_1:71
;
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
by VECTSP_1:36
;
verum
end;
for n being Nat holds S1[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 )
; verum