let n, m be Nat; :: thesis: for K being Field
for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
let K be Field; :: thesis: for A being Matrix of n,m,K st ( n = 0 implies m = 0 ) & the_rank_of A = n holds
ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
let A be Matrix of n,m,K; :: thesis: ( ( n = 0 implies m = 0 ) & the_rank_of A = n implies ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m )
set V = m -VectSp_over K;
set L = lines A;
assume that
A1: ( n = 0 implies m = 0 ) and
A2: the_rank_of A = n ; :: thesis: ex B being Matrix of m -' n,m,K st the_rank_of (A ^ B) = m
A3: len A = n by A1, MATRIX13:1;
lines A is linearly-independent by A2, MATRIX13:121;
then consider B being Subset of (m -VectSp_over K) such that
A4: lines A c= B and
a5: B is base by VECTSP_7:17;
A5: B is linearly-independent by a5, VECTSP_7:def 3;
A6: Lin B = ModuleStr(# the carrier of (m -VectSp_over K), the addF of (m -VectSp_over K), the ZeroF of (m -VectSp_over K), the lmult of (m -VectSp_over K) #) by a5, VECTSP_7:def 3;
reconsider B = B as finite Subset of (m -VectSp_over K) by A5, VECTSP_9:21;
B is Basis of (m -VectSp_over K) by A5, A6, VECTSP_7:def 3;
then A7: card B = dim (m -VectSp_over K) by VECTSP_9:def 1
.= m by MATRIX13:112 ;
width A = m by A1, MATRIX13:1;
then A8: m - n >= 0 by A2, MATRIX13:74, XREAL_1:48;
then A9: m - n = m -' n by XREAL_0:def 2;
A10: A is without_repeated_line by A2, MATRIX13:121;
then A11: len A = card (lines A) by FINSEQ_4:62;
set BL = B \ (lines A);
consider p being FinSequence such that
A12: rng p = B \ (lines A) and
A13: p is one-to-one by FINSEQ_4:58;
reconsider p = p as FinSequence of (m -VectSp_over K) by A12, FINSEQ_1:def 4;
len p = card (B \ (lines A)) by A12, A13, FINSEQ_4:62
.= (card B) - (card (lines A)) by A4, CARD_2:44
.= m -' n by A3, A11, A7, A8, XREAL_0:def 2 ;
then reconsider P = FinS2MX p as Matrix of m -' n,m,K ;
rng A misses rng P by A12, XBOOLE_1:79;
then A14: A ^ P is without_repeated_line by A10, A13, FINSEQ_3:91;
take P ; :: thesis: the_rank_of (A ^ P) = m
lines (A ^ P) = (lines A) \/ (rng P) by FINSEQ_1:31
.= (lines A) \/ B by A12, XBOOLE_1:39
.= B by A4, XBOOLE_1:12 ;
hence the_rank_of (A ^ P) = m by A5, A9, A14, MATRIX13:121; :: thesis: verum