let K be Field; :: thesis: for M being Matrix of K
for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds
the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1)
let M be Matrix of K; :: thesis: for P, P1, Q, Q1 being finite without_zero Subset of NAT st P c= P1 & Q c= Q1 holds
the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1)
let P, P1, Q, Q1 be finite without_zero Subset of NAT ; :: thesis: ( P c= P1 & Q c= Q1 implies the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1) )
assume that
A1: P c= P1 and
A2: Q c= Q1 ; :: thesis: the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1)
set S1 = Segm M,P1,Q1;
set S = Segm M,P,Q;
consider P2, Q2 being finite without_zero Subset of NAT such that
A3: [:P2,Q2:] c= Indices (Segm M,P,Q) and
A4: card P2 = card Q2 and
A5: card P2 = the_rank_of (Segm M,P,Q) and
A6: Det (EqSegm (Segm M,P,Q),P2,Q2) <> 0. K by Def4;
( P2 = {} iff Q2 = {} ) by A4;
then consider P3, Q3 being finite without_zero Subset of NAT such that
A7: P3 c= P and
A8: Q3 c= Q and
P3 = (Sgm P) .: P2 and
Q3 = (Sgm Q) .: Q2 and
A9: card P3 = card P2 and
A10: card Q3 = card Q2 and
A11: Segm (Segm M,P,Q),P2,Q2 = Segm M,P3,Q3 by A3, Th57;
reconsider P4 = (Sgm P1) " P3, Q4 = (Sgm Q1) " Q3 as finite without_zero Subset of NAT by Th53;
A12: card Q4 = card P2 by A2, A4, A8, A10, Lm2, XBOOLE_1:1;
A13: card P4 = card P2 by A1, A7, A9, Lm2, XBOOLE_1:1;
ex k being Nat st Q4 c= Seg k by Th43;
then A14: rng (Sgm Q4) = Q4 by FINSEQ_1:def 13;
A15: Q3 c= Q1 by A2, A8, XBOOLE_1:1;
A16: P3 c= P1 by A1, A7, XBOOLE_1:1;
ex k being Nat st P4 c= Seg k by Th43;
then rng (Sgm P4) = P4 by FINSEQ_1:def 13;
then A17: [:P4,Q4:] c= Indices (Segm M,P1,Q1) by A16, A15, A14, Th56;
Segm (Segm M,P1,Q1),P4,Q4 = Segm M,P3,Q3 by A16, A15, Th56;
then EqSegm (Segm M,P,Q),P2,Q2 = Segm (Segm M,P1,Q1),P4,Q4 by A4, A11, Def3
.= EqSegm (Segm M,P1,Q1),P4,Q4 by A4, A10, A15, A13, Def3, Lm2 ;
hence the_rank_of (Segm M,P,Q) <= the_rank_of (Segm M,P1,Q1) by A5, A6, A13, A12, A17, Def4; :: thesis: verum