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:22;
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_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 for i being Nat st 1 <= i & i <= len N holds
(LaplaceExpC (N,1)) . i = ((len N) |-> (0. K)) . ilet 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;
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 0. K = (LaplaceExpC (N,1)) . iper 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
;
0. K = (LaplaceExpC (N,1)) . inow Det (Delete (N,i,1)) = 0. Kper 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: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 for j being Element of NAT st j in Seg (n -' 1) holds
(Col ((Delete (N,i,1)),1)) . j = 0. KA36:
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 ;
( 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:40, 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: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
;
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_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;
verum end; then
0. K = Cofactor (
N,
i,1)
;
hence
0. K = (LaplaceExpC (N,1)) . i
by A23;
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: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;
verum end; hence
(LaplaceExpC (N,1)) . i = ((len N) |-> (0. K)) . i
by A11, A22, FINSEQ_2:57;
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;
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: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;
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: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
;
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