let m be Nat; :: thesis: for K being Field
for A, B being Matrix of K st B = 0. (K,(len A),m) holds
the_rank_of A = the_rank_of (A ^^ B)

let K be Field; :: thesis: for A, B being Matrix of K st B = 0. (K,(len A),m) holds
the_rank_of A = the_rank_of (A ^^ B)

let A, B be Matrix of K; :: thesis: ( B = 0. (K,(len A),m) implies the_rank_of A = the_rank_of (A ^^ B) )
assume A1: B = 0. (K,(len A),m) ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
A2: len B = len A by ;
set L = len A;
reconsider B9 = B as Matrix of len A, width B,K by ;
reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;
set AB = A9 ^^ B9;
per cases ( width B = 0 or width B > 0 ) ;
suppose width B = 0 ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
hence the_rank_of A = the_rank_of (A ^^ B) by ; :: thesis: verum
end;
suppose width B > 0 ; :: thesis: the_rank_of A = the_rank_of (A ^^ B)
then A3: len A > 0 by ;
then A4: width (A9 ^^ B9) = () + () by MATRIX_0:23;
A5: len (A9 ^^ B9) = len A by ;
A6: now :: thesis: for i being Nat st i in (Seg (width (A9 ^^ B9))) \ (Seg ()) holds
Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)
set L0 = (len (A9 ^^ B9)) |-> (0. K);
let i be Nat; :: thesis: ( i in (Seg (width (A9 ^^ B9))) \ (Seg ()) implies Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) )
assume A7: i in (Seg (width (A9 ^^ B9))) \ (Seg ()) ; :: thesis: Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)
A8: i in Seg (width (A9 ^^ B9)) by ;
not i in Seg () by ;
then A9: ( i < 1 or i > width A ) ;
then reconsider n = i - () as Element of NAT by ;
A10: i = n + () ;
n <> 0 by ;
then A11: n in Seg () by ;
A12: now :: thesis: for i being Nat st 1 <= i & i <= len A holds
(Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i
let i be Nat; :: thesis: ( 1 <= i & i <= len A implies (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i )
assume A13: ( 1 <= i & i <= len A ) ; :: thesis: (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i
A14: i in Seg (len A) by A13;
then A15: ((len (A9 ^^ B9)) |-> (0. K)) . i = 0. K by ;
Seg (len A) = dom B by ;
then ( (Col (B9,n)) . i = B9 * (i,n) & [i,n] in Indices B ) by ;
hence (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i by ; :: thesis: verum
end;
A16: ( len (Col (B,n)) = len A & len ((len (A9 ^^ B9)) |-> (0. K)) = len A ) by ;
Col ((A9 ^^ B9),i) = Col (B9,n) by ;
hence Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) by ; :: thesis: verum
end;
width A <= width (A9 ^^ B9) by ;
then Seg () c= Seg (width (A9 ^^ B9)) by FINSEQ_1:5;
hence the_rank_of (A ^^ B) = the_rank_of (Segm ((A9 ^^ B9),(Seg (len (A9 ^^ B9))),(Seg ()))) by
.= the_rank_of A by ;
:: thesis: verum
end;
end;