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

A7: now

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

suppose A8: i in P ; :: thesis: the_rank_of (RLine M9,i,(a * (Line M9,i))) >= the_rank_of M9

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

end;

suppose A19: not i in P ; :: thesis: the_rank_of (RLine M9,i,(a * (Line M9,i))) >= the_rank_of M9

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

end;

end;

end;

consider P1, Q1 being finite without_zero Subset of NAT such that
A20: [:P1,Q1:] c= Indices (RLine M9,i,(a * (Line M9,i))) and
A21: card P1 = card Q1 and
A22: card P1 = the_rank_of (RLine M9,i,(a * (Line M9,i))) and
A23: Det (EqSegm (RLine M9,i,(a * (Line M9,i))),P1,Q1) <> 0. K by Def4;

now

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

suppose A24: i in P1 ; :: thesis: the_rank_of M9 >= the_rank_of (RLine M9,i,(a * (Line M9,i)))

A25: len (Line M9,i) = width M9 by MATRIX_1:def 8;
then A26: dom (Line M9,i) = Seg (width M9) by FINSEQ_1:def 3;
ex n being Nat st Q1 c= Seg n by Th43;
then A27: rng (Sgm Q1) = Q1 by FINSEQ_1:def 13;
A28: ex k being Nat st P1 c= Seg k by Th43;
then A29: dom (Sgm P1) = Seg (card P1) by FINSEQ_3:45;
rng (Sgm P1) = P1 by A28, FINSEQ_1:def 13;
then consider x being set such that
A30: x in dom (Sgm P1) and
A31: (Sgm P1) . x = i by A24, FUNCT_1:def 5;
reconsider x = x as Element of NAT by A30;
A32: Q1 c= Seg (width M9) by A1, A20, A21, Th67;
then Line (Segm M9,P1,Q1),x = (Line M9,i) * (Sgm Q1) by A30, A31, A29, Th47;
then A33: a * (Line (Segm M9,P1,Q1),x) = (a * (Line M9,i)) * (Sgm Q1) by A27, A32, A26, Th87;
A34: len (a * (Line M9,i)) = len (Line M9,i) by MATRIXR1:16;
RLine (EqSegm M9,P1,Q1),x,(a * (Line (EqSegm M9,P1,Q1),x)) = RLine (Segm M9,P1,Q1),x,(a * (Line (EqSegm M9,P1,Q1),x)) by A21, Def3
.= RLine (Segm M9,P1,Q1),x,(a * (Line (Segm M9,P1,Q1),x)) by A21, Def3
.= Segm (RLine M9,i,(a * (Line M9,i))),P1,Q1 by A1, A20, A31, A25, A33, A34, Th59
.= EqSegm (RLine M9,i,(a * (Line M9,i))),P1,Q1 by A21, Def3 ;
then Det (EqSegm (RLine M9,i,(a * (Line M9,i))),P1,Q1) = a * (Det (EqSegm M9,P1,Q1)) by A30, A29, MATRIX11:35;
then Det (EqSegm M9,P1,Q1) <> 0. K by A23, VECTSP_1:44;
hence the_rank_of M9 >= the_rank_of (RLine M9,i,(a * (Line M9,i))) by A1, A20, A21, A22, Def4; :: thesis: verum

end;

suppose A35: not i in P1 ; :: thesis: the_rank_of M9 >= the_rank_of (RLine M9,i,(a * (Line M9,i)))

EqSegm M9,P1,Q1 = Segm M9,P1,Q1 by A21, Def3
.= Segm (RLine M9,i,(a * (Line M9,i))),P1,Q1 by A1, A20, A35, Th60
.= EqSegm (RLine M9,i,(a * (Line M9,i))),P1,Q1 by A21, Def3 ;
hence the_rank_of M9 >= the_rank_of (RLine M9,i,(a * (Line M9,i))) by A1, A20, A21, A22, A23, Def4; :: thesis: verum

end;

end;

end;

hence the_rank_of M9 = the_rank_of (RLine M9,i,(a * (Line M9,i))) by A7, XXREAL_0:1; :: thesis: verum