let K be Field; :: thesis: for A being Matrix of K
for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] c= Indices A holds
for i, j being Nat st i in (dom A) \ P & j in (Seg ()) \ Q & A * (i,j) <> 0. K & Q c= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))

let A be Matrix of K; :: thesis: for P, Q, Q9 being finite without_zero Subset of NAT st [:P,Q9:] c= Indices A holds
for i, j being Nat st i in (dom A) \ P & j in (Seg ()) \ Q & A * (i,j) <> 0. K & Q c= Q9 & (Line (A,i)) * (Sgm Q9) = (card Q9) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))

let P, Q, R be finite without_zero Subset of NAT; :: thesis: ( [:P,R:] c= Indices A implies for i, j being Nat st i in (dom A) \ P & j in (Seg ()) \ Q & A * (i,j) <> 0. K & Q c= R & (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q)) )

assume A1: [:P,R:] c= Indices A ; :: thesis: for i, j being Nat st i in (dom A) \ P & j in (Seg ()) \ Q & A * (i,j) <> 0. K & Q c= R & (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) holds
the_rank_of A > the_rank_of (Segm (A,P,Q))

let i, j be Nat; :: thesis: ( i in (dom A) \ P & j in (Seg ()) \ Q & A * (i,j) <> 0. K & Q c= R & (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) implies the_rank_of A > the_rank_of (Segm (A,P,Q)) )
assume that
A2: i in (dom A) \ P and
A3: j in (Seg ()) \ Q and
A4: A * (i,j) <> 0. K and
A5: Q c= R and
A6: (Line (A,i)) * (Sgm R) = (card R) |-> (0. K) ; :: thesis: the_rank_of A > the_rank_of (Segm (A,P,Q))
A7: dom A = Seg (len A) by FINSEQ_1:def 3;
then A8: i in Seg (len A) by ;
A9: [:P,Q:] c= [:P,R:] by ;
then A10: [:P,Q:] c= Indices A by A1;
reconsider i0 = i, j0 = j as non zero Element of NAT by A2, A3, A7;
A11: j in Seg () by ;
set S = Segm (A,P,Q);
consider P9, Q9 being finite without_zero Subset of NAT such that
A12: [:P9,Q9:] c= Indices (Segm (A,P,Q)) and
A13: card P9 = card Q9 and
A14: card P9 = the_rank_of (Segm (A,P,Q)) and
A15: Det (EqSegm ((Segm (A,P,Q)),P9,Q9)) <> 0. K by MATRIX13:def 4;
( P9 = {} iff Q9 = {} ) by A13;
then consider P2, Q2 being finite without_zero Subset of NAT such that
A16: P2 c= P and
A17: Q2 c= Q and
P2 = (Sgm P) .: P9 and
Q2 = (Sgm Q) .: Q9 and
A18: card P2 = card P9 and
A19: card Q2 = card Q9 and
A20: Segm ((Segm (A,P,Q)),P9,Q9) = Segm (A,P2,Q2) by ;
set Q2j = Q2 \/ {j0};
set P2i = P2 \/ {i0};
set ESS = EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}));
set SS = Segm (A,(P2 \/ {i0}),(Q2 \/ {j0}));
per cases ( [:P,Q:] = {} or [:P,Q:] <> {} ) ;
suppose [:P,Q:] = {} ; :: thesis: the_rank_of A > the_rank_of (Segm (A,P,Q))
then ( card P = 0 or card Q = 0 ) by ;
then A21: the_rank_of (Segm (A,P,Q)) = 0 by MATRIX13:77;
[i,j] in Indices A by ;
hence the_rank_of A > the_rank_of (Segm (A,P,Q)) by ; :: thesis: verum
end;
suppose A22: [:P,Q:] <> {} ; :: thesis: the_rank_of A > the_rank_of (Segm (A,P,Q))
then P c= dom A by ;
then A23: P2 c= dom A by A16;
[:P,R:] <> {} by ;
then A24: R c= Seg () by ;
then A25: dom (Sgm R) = Seg (card R) by FINSEQ_3:40;
Q c= Seg () by ;
then A26: Q2 c= Seg () by A17;
A27: {j0} c= Seg () by ;
then A28: Sgm (Q2 \/ {j0}) is one-to-one by ;
A29: Q2 \/ {j0} c= Seg () by ;
then A30: rng (Sgm (Q2 \/ {j0})) = Q2 \/ {j0} by FINSEQ_1:def 13;
A31: {i0} c= dom A by ;
then A32: P2 \/ {i0} c= dom A by ;
then A33: [:(P2 \/ {i0}),(Q2 \/ {j0}):] c= Indices A by ;
A34: dom (Sgm (P2 \/ {i0})) = Seg (card (P2 \/ {i0})) by ;
i in {i} by TARSKI:def 1;
then A35: i in P2 \/ {i0} by XBOOLE_0:def 3;
A36: not i in P2 by ;
then A37: card (P2 \/ {i0}) = (card P2) + 1 by CARD_2:41;
then A38: (card (P2 \/ {i0})) -' 1 = card P9 by ;
A39: not j in Q2 by ;
then A40: card (Q2 \/ {j0}) = (card Q2) + 1 by CARD_2:41;
then A41: EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0})) = Segm (A,(P2 \/ {i0}),(Q2 \/ {j0})) by ;
j in {j} by TARSKI:def 1;
then j in Q2 \/ {j0} by XBOOLE_0:def 3;
then consider y being object such that
A42: y in dom (Sgm (Q2 \/ {j0})) and
A43: (Sgm (Q2 \/ {j0})) . y = j by ;
rng (Sgm (P2 \/ {i0})) = P2 \/ {i0} by ;
then consider x being object such that
A44: x in dom (Sgm (P2 \/ {i0})) and
A45: (Sgm (P2 \/ {i0})) . x = i by ;
reconsider x = x, y = y as Element of NAT by ;
- (1_ K) <> 0. K by VECTSP_1:28;
then A46: (power K) . ((- (1_ K)),(x + y)) <> 0. K by Lm2;
set L = LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x);
A47: dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) = Seg (len (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x))) by FINSEQ_1:def 3
.= Seg (card (P2 \/ {i0})) by LAPLACE:def 7 ;
then A48: y in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) by ;
A49: dom (Sgm (Q2 \/ {j0})) = Seg (card (Q2 \/ {j0})) by ;
then Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y) = EqSegm (A,((P2 \/ {i0}) \ {i}),((Q2 \/ {j0}) \ {j})) by
.= EqSegm (A,P2,((Q2 \/ {j0}) \ {j})) by
.= EqSegm (A,P2,Q2) by
.= Segm (A,P2,Q2) by
.= EqSegm ((Segm (A,P,Q)),P9,Q9) by ;
then A50: ((power K) . ((- (1_ K)),(x + y))) * (Det (Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y))) <> 0. K by ;
A51: Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) = [:(Seg (card (P2 \/ {i0}))),(Seg (card (P2 \/ {i0}))):] by MATRIX_0:24;
then A52: [x,y] in Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) by ;
A53: rng (Sgm R) = R by ;
now :: thesis: for k being Nat st k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) & k <> y holds
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K
let k be Nat; :: thesis: ( k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) & k <> y implies (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K )
assume that
A54: k in dom (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) and
A55: k <> y ; :: thesis: (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = 0. K
(Sgm (Q2 \/ {j0})) . k <> j by ;
then A56: not (Sgm (Q2 \/ {j0})) . k in {j} by TARSKI:def 1;
(Sgm (Q2 \/ {j0})) . k in Q2 \/ {j0} by ;
then (Sgm (Q2 \/ {j0})) . k in Q2 by ;
then A57: (Sgm (Q2 \/ {j0})) . k in Q by A17;
then A58: (Sgm (Q2 \/ {j0})) . k in R by A5;
consider z being object such that
A59: z in dom (Sgm R) and
A60: (Sgm R) . z = (Sgm (Q2 \/ {j0})) . k by ;
reconsider z = z as Element of NAT by A59;
[x,k] in Indices (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) by ;
then (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) * (x,k) = A * (i,((Sgm (Q2 \/ {j0})) . k)) by
.= (Line (A,i)) . ((Sgm R) . z) by
.= ((card R) |-> (0. K)) . z by
.= 0. K by ;
hence (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . k = (0. K) * (Cofactor ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,k)) by
.= 0. K ;
:: thesis: verum
end;
then A61: (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . y = Sum (LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) by
.= Det (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) by ;
(LaplaceExpL ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x)) . y = ((Segm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) * (x,y)) * (Cofactor ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y)) by
.= (A * (i,j)) * ((() . ((- (1_ K)),(x + y))) * (Det (Delete ((EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))),x,y)))) by ;
then Det (EqSegm (A,(P2 \/ {i0}),(Q2 \/ {j0}))) <> 0. K by ;
then the_rank_of A >= card (P2 \/ {i0}) by ;
hence the_rank_of A > the_rank_of (Segm (A,P,Q)) by ; :: thesis: verum
end;
end;