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) )
assume A1: a <> 0. K ; :: thesis: the_rank_of M = the_rank_of (a * M)
A2: Indices M = Indices (a * M) by MATRIXR1:18;
consider P, Q being finite without_zero Subset of NAT such that
A3: ( [:P,Q:] c= Indices M & card P = card Q ) and
A4: ( card P = the_rank_of M & Det (EqSegm M,P,Q) <> 0. K ) by Def4;
( Det (EqSegm (a * M),P,Q) = ((power K) . a,(card P)) * (Det (EqSegm M,P,Q)) & (power K) . a,(card P) <> 0. K ) by A1, A3, Lm6, Th72;
then Det (EqSegm (a * M),P,Q) <> 0. K by A4, VECTSP_1:44;
then A5: the_rank_of (a * M) >= the_rank_of M by A2, A3, A4, Def4;
consider P1, Q1 being finite without_zero Subset of NAT such that
A6: ( [:P1,Q1:] c= Indices (a * M) & card P1 = card Q1 ) and
A7: ( card P1 = the_rank_of (a * M) & Det (EqSegm (a * M),P1,Q1) <> 0. K ) by Def4;
Det (EqSegm (a * M),P1,Q1) = ((power K) . a,(card P1)) * (Det (EqSegm M,P1,Q1)) by A2, A6, Th72;
then Det (EqSegm M,P1,Q1) <> 0. K by A7, VECTSP_1:44;
then the_rank_of M >= the_rank_of (a * M) by A2, A6, A7, Def4;
hence the_rank_of M = the_rank_of (a * M) by A5, XXREAL_0:1; :: thesis: verum