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;
A14: rng (Sgm Q4) = Q4 by FINSEQ_1:def 14;
A15: Q3 c= Q1 by A2, A8;
A16: P3 c= P1 by A1, A7;
rng (Sgm P4) = P4 by FINSEQ_1:def 14;
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