let n, m be Nat; for K being Field
for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
let K be Field; for A being Matrix of n,m,K st the_rank_of A = m holds
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
let A be Matrix of n,m,K; ( the_rank_of A = m implies ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n )
assume A1:
the_rank_of A = m
; ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
A2:
len A = n
by MATRIX_0:def 2;
per cases
( m = 0 or m > 0 )
;
suppose A3:
m = 0
;
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = nthen
n -' m = n - m
by XREAL_0:def 2;
then reconsider ONE =
1. (
K,
n) as
Matrix of
n,
n -' m,
K by A3;
A4:
len (1. (K,n)) = n
by MATRIX_0:24;
Det (1. (K,n)) <> 0. K
by LAPLACE:34;
then A5:
the_rank_of ONE = n
by MATRIX13:83;
width A = m
by A3, MATRIX13:1;
then
A ^^ ONE = ONE
by A2, A3, A4, MATRIX15:22;
hence
ex
B being
Matrix of
n,
n -' m,
K st
the_rank_of (A ^^ B) = n
by A5;
verum end; suppose A6:
m > 0
;
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = n
n - m >= 0
by A1, A2, MATRIX13:74, XREAL_1:48;
then A7:
n -' m = n - m
by XREAL_0:def 2;
A8:
n > 0
by A1, A2, A6, MATRIX13:74;
then A9:
width A = m
by MATRIX13:1;
per cases
( n = m or n <> m )
;
suppose A11:
n <> m
;
ex B being Matrix of n,n -' m,K st the_rank_of (A ^^ B) = nA12:
width (A @) = n
by A2, A6, A9, MATRIX_0:54;
len (A @) = m
by A6, A9, MATRIX_0:54;
then reconsider A1 =
A @ as
Matrix of
m,
n,
K by A12, MATRIX_0:51;
the_rank_of A1 = m
by A1, MATRIX13:84;
then consider B being
Matrix of
n -' m,
n,
K such that A13:
the_rank_of (A1 ^ B) = n
by Th16;
A14:
n -' m <> 0
by A7, A11;
then A15:
width B = n
by MATRIX13:1;
then A16:
len (B @) = n
by A8, MATRIX_0:54;
len B = n -' m
by A14, MATRIX13:1;
then
width (B @) = n -' m
by A8, A15, MATRIX_0:54;
then reconsider B1 =
B @ as
Matrix of
n,
n -' m,
K by A16, MATRIX_0:51;
A1 @ = A
by A2, A6, A8, A9, MATRIX_0:57;
then A17:
(A1 ^ B) @ = A ^^ B1
by A12, A15, MATRLIN:28;
the_rank_of ((A1 ^ B) @) = n
by A13, MATRIX13:84;
hence
ex
B being
Matrix of
n,
n -' m,
K st
the_rank_of (A ^^ B) = n
by A17;
verum end; end;