let i, m9, n9 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_0:26;
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 :: thesis: the_rank_of (RLine (M9,i,(a * (Line (M9,i))))) >= the_rank_of M9
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_0:def 7;
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:40;
rng (Sgm P) = P by A12, FINSEQ_1:def 13;
then consider x being object such that
A14: x in dom (Sgm P) and
A15: (Sgm P) . x = i by A8, FUNCT_1:def 3;
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:12;
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 :: thesis: the_rank_of M9 >= the_rank_of (RLine (M9,i,(a * (Line (M9,i)))))
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_0:def 7;
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:40;
rng (Sgm P1) = P1 by A28, FINSEQ_1:def 13;
then consider x being object such that
A30: x in dom (Sgm P1) and
A31: (Sgm P1) . x = i by A24, FUNCT_1:def 3;
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;
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