let n', m', i be Nat; :: thesis: for K being Field
for a being Element of
for M' being Matrix of the carrier of K,n', 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
for M' being Matrix of the carrier of K,n', st a <> 0. K holds
the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))
let a be Element of ; :: thesis: for M' being Matrix of the carrier of K,n', st a <> 0. K holds
the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))
let M' be Matrix of the carrier of K,n',; :: thesis: ( a <> 0. K implies 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));
A1: Indices M' = Indices (RLine M',i,(a * (Line M',i))) by MATRIX_1:27;
consider P, Q being finite without_zero Subset of such that
A2: [:P,Q:] c= Indices M' and
A3: card P = card Q and
A4: card P = the_rank_of M' and
A5: Det (EqSegm M',P,Q) <> 0. K by Def4;
assume A6: a <> 0. K ; :: thesis: the_rank_of M' = the_rank_of (RLine M',i,(a * (Line M',i)))

A7: now

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

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

A9: len (Line M',i) = width M' by MATRIX_1:def 8;
then A10: dom (Line M',i) = Seg (width M') 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 M') by A2, A3, Th67;
then Line (Segm M',P,Q),x = (Line M',i) * (Sgm Q) by A14, A15, A13, Th47;
then A17: a * (Line (Segm M',P,Q),x) = (a * (Line M',i)) * (Sgm Q) by A11, A16, A10, Th87;
A18: len (a * (Line M',i)) = len (Line M',i) by 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 A3, Def3
.= RLine (Segm M',P,Q),x,(a * (Line (Segm M',P,Q),x)) by A3, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P,Q by A2, A15, A9, A17, A18, Th59
.= EqSegm (RLine M',i,(a * (Line M',i))),P,Q by A3, Def3 ;
then Det (EqSegm (RLine M',i,(a * (Line M',i))),P,Q) = a * (Det (EqSegm M',P,Q)) by A14, A13, MATRIX11:35;
then Det (EqSegm (RLine M',i,(a * (Line M',i))),P,Q) <> 0. K by A6, A5, VECTSP_1:44;
hence the_rank_of (RLine M',i,(a * (Line M',i))) >= the_rank_of M' by A2, A3, A4, A1, Def4; :: thesis: verum

end;

suppose A19: 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 A3, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P,Q by A2, A19, Th60
.= EqSegm (RLine M',i,(a * (Line M',i))),P,Q by A3, Def3 ;
hence the_rank_of (RLine M',i,(a * (Line M',i))) >= the_rank_of M' by A2, A3, A4, A5, A1, Def4; :: thesis: verum

end;

end;

end;

consider P1, Q1 being finite without_zero Subset of such that
A20: [:P1,Q1:] c= Indices (RLine M',i,(a * (Line M',i))) and
A21: card P1 = card Q1 and
A22: card P1 = the_rank_of (RLine M',i,(a * (Line M',i))) and
A23: 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 A24: i in P1 ; :: thesis: the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i)))

A25: len (Line M',i) = width M' by MATRIX_1:def 8;
then A26: dom (Line M',i) = Seg (width M') 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 M') by A1, A20, A21, Th67;
then Line (Segm M',P1,Q1),x = (Line M',i) * (Sgm Q1) by A30, A31, A29, Th47;
then A33: a * (Line (Segm M',P1,Q1),x) = (a * (Line M',i)) * (Sgm Q1) by A27, A32, A26, Th87;
A34: len (a * (Line M',i)) = len (Line M',i) by 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 A21, Def3
.= RLine (Segm M',P1,Q1),x,(a * (Line (Segm M',P1,Q1),x)) by A21, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P1,Q1 by A1, A20, A31, A25, A33, A34, Th59
.= EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1 by A21, Def3 ;
then Det (EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1) = a * (Det (EqSegm M',P1,Q1)) by A30, A29, MATRIX11:35;
then Det (EqSegm M',P1,Q1) <> 0. K by A23, VECTSP_1:44;
hence the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i))) by A1, A20, A21, A22, Def4; :: thesis: verum

end;

suppose A35: 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 A21, Def3
.= Segm (RLine M',i,(a * (Line M',i))),P1,Q1 by A1, A20, A35, Th60
.= EqSegm (RLine M',i,(a * (Line M',i))),P1,Q1 by A21, Def3 ;
hence the_rank_of M' >= the_rank_of (RLine M',i,(a * (Line M',i))) by A1, A20, A21, A22, A23, Def4; :: thesis: verum

end;

end;

end;

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