let K be Field; for M being Matrix of K holds the_rank_of M = the_rank_of (M @)
let M be Matrix of K; the_rank_of M = the_rank_of (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;
A5:
[:Q,P:] c= Indices (M @)
by A1, A2, Th69;
consider P1, Q1 being finite without_zero Subset of NAT such that
A6:
[:P1,Q1:] c= Indices (M @)
and
A7:
card P1 = card Q1
and
A8:
card P1 = the_rank_of (M @)
and
A9:
Det (EqSegm ((M @),P1,Q1)) <> 0. K
by Def4;
A10:
[:Q1,P1:] c= Indices M
by A6, A7, Th69;
then
Det (EqSegm (M,Q1,P1)) <> 0. K
by A7, A9, Th70;
then A11:
the_rank_of M >= the_rank_of (M @)
by A7, A8, A10, Def4;
Det (EqSegm ((M @),Q,P)) <> 0. K
by A1, A2, A4, Th70;
then
the_rank_of (M @) >= the_rank_of M
by A2, A3, A5, Def4;
hence
the_rank_of M = the_rank_of (M @)
by A11, XXREAL_0:1; verum