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 A1, MATRIX_0:def 2;

set L = len A;

reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_0:51;

reconsider A9 = A as Matrix of len A, width A,K by MATRIX_0:51;

set AB = A9 ^^ B9;

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 A1, MATRIX_0:def 2;

set L = len A;

reconsider B9 = B as Matrix of len A, width B,K by A2, MATRIX_0:51;

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 )
;

end;

suppose
width B > 0
; :: thesis: the_rank_of A = the_rank_of (A ^^ B)

then A3:
len A > 0
by A2, MATRIX_0:def 3;

then A4: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_0:23;

A5: len (A9 ^^ B9) = len A by A3, MATRIX_0:23;

then Seg (width A) 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 (width A)))) by A6, Th12

.= the_rank_of A by A5, Th19 ;

:: thesis: verum

end;then A4: width (A9 ^^ B9) = (width A) + (width B) by MATRIX_0:23;

A5: len (A9 ^^ B9) = len A by A3, MATRIX_0:23;

A6: now :: thesis: for i being Nat st i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) holds

Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)

width A <= width (A9 ^^ B9)
by A4, NAT_1:11;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 (width A)) implies Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) )

assume A7: i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) ; :: thesis: Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)

A8: i in Seg (width (A9 ^^ B9)) by A7, XBOOLE_0:def 5;

not i in Seg (width A) by A7, XBOOLE_0:def 5;

then A9: ( i < 1 or i > width A ) ;

then reconsider n = i - (width A) as Element of NAT by A8, FINSEQ_1:1, NAT_1:21;

A10: i = n + (width A) ;

n <> 0 by A8, A9, FINSEQ_1:1;

then A11: n in Seg (width B) by A4, A8, A10, FINSEQ_1:61;

Col ((A9 ^^ B9),i) = Col (B9,n) by A10, A11, Th17;

hence Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) by A16, A12; :: thesis: verum

end;let i be Nat; :: thesis: ( i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) implies Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) )

assume A7: i in (Seg (width (A9 ^^ B9))) \ (Seg (width A)) ; :: thesis: Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K)

A8: i in Seg (width (A9 ^^ B9)) by A7, XBOOLE_0:def 5;

not i in Seg (width A) by A7, XBOOLE_0:def 5;

then A9: ( i < 1 or i > width A ) ;

then reconsider n = i - (width A) as Element of NAT by A8, FINSEQ_1:1, NAT_1:21;

A10: i = n + (width A) ;

n <> 0 by A8, A9, FINSEQ_1:1;

then A11: n in Seg (width B) by A4, A8, A10, FINSEQ_1:61;

A12: now :: thesis: for i being Nat st 1 <= i & i <= len A holds

(Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i

A16:
( len (Col (B,n)) = len A & len ((len (A9 ^^ B9)) |-> (0. K)) = len A )
by A2, A5, CARD_1:def 7;(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 A5, FINSEQ_2:57;

Seg (len A) = dom B by A2, FINSEQ_1:def 3;

then ( (Col (B9,n)) . i = B9 * (i,n) & [i,n] in Indices B ) by A11, A14, MATRIX_0:def 8, ZFMISC_1:87;

hence (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i by A1, A15, MATRIX_3:1; :: thesis: verum

end;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 A5, FINSEQ_2:57;

Seg (len A) = dom B by A2, FINSEQ_1:def 3;

then ( (Col (B9,n)) . i = B9 * (i,n) & [i,n] in Indices B ) by A11, A14, MATRIX_0:def 8, ZFMISC_1:87;

hence (Col (B9,n)) . i = ((len (A9 ^^ B9)) |-> (0. K)) . i by A1, A15, MATRIX_3:1; :: thesis: verum

Col ((A9 ^^ B9),i) = Col (B9,n) by A10, A11, Th17;

hence Col ((A9 ^^ B9),i) = (len (A9 ^^ B9)) |-> (0. K) by A16, A12; :: thesis: verum

then Seg (width A) 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 (width A)))) by A6, Th12

.= the_rank_of A by A5, Th19 ;

:: thesis: verum