let K be Field; for M being Matrix of K
for P, Q being finite without_zero Subset of NAT
for i being Nat st i in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
let M be Matrix of K; for P, Q being finite without_zero Subset of NAT
for i being Nat st i in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
let P, Q be finite without_zero Subset of NAT; for i being Nat st i in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K holds
ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
let i be Nat; ( i in Seg (card P) & Det (EqSegm (M,P,Q)) <> 0. K implies ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K ) )
assume that
A1:
i in Seg (card P)
and
A2:
Det (EqSegm (M,P,Q)) <> 0. K
; ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
set C = card P;
set E = EqSegm (M,P,Q);
set LL = LaplaceExpL ((EqSegm (M,P,Q)),i);
set CC = (card P) |-> (0. K);
Sum ((card P) |-> (0. K)) = 0. K
by MATRIX_3:11;
then A3:
LaplaceExpL ((EqSegm (M,P,Q)),i) <> (card P) |-> (0. K)
by A1, A2, LAPLACE:25;
len (LaplaceExpL ((EqSegm (M,P,Q)),i)) = card P
by LAPLACE:def 7;
then A4:
dom (LaplaceExpL ((EqSegm (M,P,Q)),i)) = Seg (card P)
by FINSEQ_1:def 3;
consider j being Nat such that
A5:
j in dom (LaplaceExpL ((EqSegm (M,P,Q)),i))
and
A6:
(LaplaceExpL ((EqSegm (M,P,Q)),i)) . j <> ((card P) |-> (0. K)) . j
by A3, A4;
A7:
(LaplaceExpL ((EqSegm (M,P,Q)),i)) . j = ((EqSegm (M,P,Q)) * (i,j)) * (Cofactor ((EqSegm (M,P,Q)),i,j))
by A5, LAPLACE:def 7;
((card P) |-> (0. K)) . j = 0. K
by A4, A5, FINSEQ_2:57;
then
Cofactor ((EqSegm (M,P,Q)),i,j) <> 0. K
by A6, A7;
then
Minor ((EqSegm (M,P,Q)),i,j) <> 0. K
;
hence
ex j being Nat st
( j in Seg (card P) & Det (Delete ((EqSegm (M,P,Q)),i,j)) <> 0. K )
by A4, A5; verum