let n be Nat; :: thesis: for K being Field

for A being Matrix of n,n,K

for B being Matrix of K st len A = width B & Det A <> 0. K holds

the_rank_of (B * A) = the_rank_of B

let K be Field; :: thesis: for A being Matrix of n,n,K

for B being Matrix of K st len A = width B & Det A <> 0. K holds

the_rank_of (B * A) = the_rank_of B

let A be Matrix of n,n,K; :: thesis: for B being Matrix of K st len A = width B & Det A <> 0. K holds

the_rank_of (B * A) = the_rank_of B

let B be Matrix of K; :: thesis: ( len A = width B & Det A <> 0. K implies the_rank_of (B * A) = the_rank_of B )

assume that

A1: width B = len A and

A2: Det A <> 0. K ; :: thesis: the_rank_of (B * A) = the_rank_of B

set BA = B * A;

A3: len (B * A) = len B by A1, MATRIX_3:def 4;

A4: width (B * A) = width A by A1, MATRIX_3:def 4;

A5: ( len A = n & width A = n ) by MATRIX_0:24;

for A being Matrix of n,n,K

for B being Matrix of K st len A = width B & Det A <> 0. K holds

the_rank_of (B * A) = the_rank_of B

let K be Field; :: thesis: for A being Matrix of n,n,K

for B being Matrix of K st len A = width B & Det A <> 0. K holds

the_rank_of (B * A) = the_rank_of B

let A be Matrix of n,n,K; :: thesis: for B being Matrix of K st len A = width B & Det A <> 0. K holds

the_rank_of (B * A) = the_rank_of B

let B be Matrix of K; :: thesis: ( len A = width B & Det A <> 0. K implies the_rank_of (B * A) = the_rank_of B )

assume that

A1: width B = len A and

A2: Det A <> 0. K ; :: thesis: the_rank_of (B * A) = the_rank_of B

set BA = B * A;

A3: len (B * A) = len B by A1, MATRIX_3:def 4;

A4: width (B * A) = width A by A1, MATRIX_3:def 4;

A5: ( len A = n & width A = n ) by MATRIX_0:24;

per cases
( width (B * A) = 0 or width (B * A) > 0 )
;

end;

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

then A7:
( width (A @) = len A & len (B @) = width B )
by A1, A4, A5, MATRIX_0:54;

A8: Det (A @) <> 0. K by A2, MATRIXR2:43;

thus the_rank_of (B * A) = the_rank_of ((B * A) @) by MATRIX13:84

.= the_rank_of ((A @) * (B @)) by A1, A4, A6, MATRIX_3:22

.= the_rank_of (B @) by A1, A8, A7, Th75

.= the_rank_of B by MATRIX13:84 ; :: thesis: verum

end;A8: Det (A @) <> 0. K by A2, MATRIXR2:43;

thus the_rank_of (B * A) = the_rank_of ((B * A) @) by MATRIX13:84

.= the_rank_of ((A @) * (B @)) by A1, A4, A6, MATRIX_3:22

.= the_rank_of (B @) by A1, A8, A7, Th75

.= the_rank_of B by MATRIX13:84 ; :: thesis: verum