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