let n', m', i be Nat; :: thesis: for K being Field
for a being Element of K
for M' being Matrix of n',m',K st a <> 0. K holds
the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))
let K be Field; :: thesis: for a being Element of K
for M' being Matrix of n',m',K st a <> 0. K holds
the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))
let a be Element of K; :: thesis: for M' being Matrix of n',m',K st a <> 0. K holds
the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))
let M' be Matrix of n',m',K; :: thesis: ( a <> 0. K implies the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i))) )
assume A1: a <> 0. K ; :: thesis: the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))
set L = Line M',i;
set aL = a * (Line M',i);
set R = RLine M',i,(a * (Line M',i));
consider P, Q being finite without_zero Subset of NAT such that
A2: ( [:P,Q:] c= Indices M' & card P = card Q ) and
A3: ( card P = the_rank_of M' & Det (EqSegm M',P,Q) <> 0. K ) by Def4;
A4: Indices M' = Indices (RLine M',i,(a * (Line M',i))) by MATRIX_1:27;

A5: now

per cases ( i in P or not i in P ) ;

suppose A6: i in P ; :: thesis: the_rank_of (RLine M',i,(a * (Line M',i))) >= the_rank_of M'

consider k being Nat such that
A7: P c= Seg k by Th43;
rng (Sgm P) = P by A7, FINSEQ_1:def 13;
then consider x being set such that
A8: ( x in dom (Sgm P) & (Sgm P) . x = i ) by A6, FUNCT_1:def 5;
A9: dom (Sgm P) = Seg (card P) by A7, FINSEQ_3:45;
reconsider x = x as Element of NAT by A8;
consider n being Nat such that
A10: Q c= Seg n by Th43;
A11: rng (Sgm Q) = Q by A10, FINSEQ_1:def 13;
A12: len (Line M',i) = width M' by MATRIX_1:def 8;
then A13: ( Q c= Seg (width M') & dom (Line M',i) = Seg (width M') ) by A2, Th67, FINSEQ_1:def 3;
then Line (Segm M',P,Q),x = (Line M',i) * (Sgm Q) by A8, A9, Th47;
then A14: ( a * (Line (Segm M',P,Q),x) = (a * (Line M',i)) * (Sgm Q) & len (a * (Line M',i)) = len (Line M',i) ) by A11, A13, Th87, MATRIXR1:16;
RLine (EqSegm M',P,Q),x,(a * (Line (EqSegm M',P,Q),x)) = RLine (Segm M',P,Q),x,(a * (Line (EqSegm M',P,Q),x)) by A2, Def3
.= RLine (Segm M',P,Q),x,(a * (Line (Segm M',P,Q),x)) by A2, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P,Q by A2, A8, A12, A14, Th59
.= EqSegm (RLine M',i,(a * (Line M',i))),P,Q by A2, Def3 ;
then Det (EqSegm (RLine M',i,(a * (Line M',i))),P,Q) = a * (Det (EqSegm M',P,Q)) by A8, A9, MATRIX11:35;
then Det (EqSegm (RLine M',i,(a * (Line M',i))),P,Q) <> 0. K by A1, A3, VECTSP_1:44;
hence the_rank_of (RLine M',i,(a * (Line M',i))) >= the_rank_of M' by A2, A3, A4, Def4; :: thesis: verum

end;

suppose A15: not i in P ; :: thesis: the_rank_of (RLine M',i,(a * (Line M',i))) >= the_rank_of M'

EqSegm M',P,Q = Segm M',P,Q by A2, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P,Q by A2, A15, Th60
.= EqSegm (RLine M',i,(a * (Line M',i))),P,Q by A2, Def3 ;
hence the_rank_of (RLine M',i,(a * (Line M',i))) >= the_rank_of M' by A2, A3, A4, Def4; :: thesis: verum

end;

end;

end;

consider P1, Q1 being finite without_zero Subset of NAT such that
A16: ( [:P1,Q1:] c= Indices (RLine M',i,(a * (Line M',i))) & card P1 = card Q1 ) and
A17: ( card P1 = the_rank_of (RLine M',i,(a * (Line M',i))) & Det (EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1) <> 0. K ) by Def4;

now

per cases ( i in P1 or not i in P1 ) ;

suppose A18: i in P1 ; :: thesis: the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i)))

consider k being Nat such that
A19: P1 c= Seg k by Th43;
rng (Sgm P1) = P1 by A19, FINSEQ_1:def 13;
then consider x being set such that
A20: ( x in dom (Sgm P1) & (Sgm P1) . x = i ) by A18, FUNCT_1:def 5;
A21: dom (Sgm P1) = Seg (card P1) by A19, FINSEQ_3:45;
reconsider x = x as Element of NAT by A20;
consider n being Nat such that
A22: Q1 c= Seg n by Th43;
A23: rng (Sgm Q1) = Q1 by A22, FINSEQ_1:def 13;
A24: len (Line M',i) = width M' by MATRIX_1:def 8;
then A25: ( Q1 c= Seg (width M') & dom (Line M',i) = Seg (width M') ) by A4, A16, Th67, FINSEQ_1:def 3;
then Line (Segm M',P1,Q1),x = (Line M',i) * (Sgm Q1) by A20, A21, Th47;
then A26: ( a * (Line (Segm M',P1,Q1),x) = (a * (Line M',i)) * (Sgm Q1) & len (a * (Line M',i)) = len (Line M',i) ) by A23, A25, Th87, MATRIXR1:16;
RLine (EqSegm M',P1,Q1),x,(a * (Line (EqSegm M',P1,Q1),x)) = RLine (Segm M',P1,Q1),x,(a * (Line (EqSegm M',P1,Q1),x)) by A16, Def3
.= RLine (Segm M',P1,Q1),x,(a * (Line (Segm M',P1,Q1),x)) by A16, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P1,Q1 by A4, A16, A20, A24, A26, Th59
.= EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1 by A16, Def3 ;
then Det (EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1) = a * (Det (EqSegm M',P1,Q1)) by A20, A21, MATRIX11:35;
then Det (EqSegm M',P1,Q1) <> 0. K by A17, VECTSP_1:44;
hence the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i))) by A4, A16, A17, Def4; :: thesis: verum

end;

suppose A27: not i in P1 ; :: thesis: the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i)))

EqSegm M',P1,Q1 = Segm M',P1,Q1 by A16, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P1,Q1 by A4, A16, A27, Th60
.= EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1 by A16, Def3 ;
hence the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i))) by A4, A16, A17, Def4; :: thesis: verum

end;

end;

end;

hence the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i))) by A5, XXREAL_0:1; :: thesis: verum