let K be Field; :: thesis: for a being Element of K
for M being Matrix of K st a <> 0. K holds
the_rank_of M = the_rank_of (a * M)
let a be Element of K; :: thesis: for M being Matrix of K st a <> 0. K holds
the_rank_of M = the_rank_of (a * M)
let M be Matrix of K; :: thesis: ( a <> 0. K implies the_rank_of M = the_rank_of (a * M) )
consider P, Q being finite without_zero Subset of NAT such that
A1: [:P,Q:] c= Indices M and
A2: card P = card Q and
A3: card P = the_rank_of M and
A4: Det (EqSegm (M,P,Q)) <> 0. K by Def4;
consider P1, Q1 being finite without_zero Subset of NAT such that
A5: [:P1,Q1:] c= Indices (a * M) and
A6: card P1 = card Q1 and
A7: card P1 = the_rank_of (a * M) and
A8: Det (EqSegm ((a * M),P1,Q1)) <> 0. K by Def4;
A9: Indices M = Indices (a * M) by MATRIXR1:18;
then Det (EqSegm ((a * M),P1,Q1)) = ((power K) . (a,(card P1))) * (Det (EqSegm (M,P1,Q1))) by A5, A6, Th72;
then Det (EqSegm (M,P1,Q1)) <> 0. K by A8;
then A10: the_rank_of M >= the_rank_of (a * M) by A9, A5, A6, A7, Def4;
assume a <> 0. K ; :: thesis: the_rank_of M = the_rank_of (a * M)
then A11: (power K) . (a,(card P)) <> 0. K by Lm6;
Det (EqSegm ((a * M),P,Q)) = ((power K) . (a,(card P))) * (Det (EqSegm (M,P,Q))) by A1, A2, Th72;
then Det (EqSegm ((a * M),P,Q)) <> 0. K by A4, A11, VECTSP_1:12;
then the_rank_of (a * M) >= the_rank_of M by A9, A1, A2, A3, Def4;
hence the_rank_of M = the_rank_of (a * M) by A10, XXREAL_0:1; :: thesis: verum