let n be Nat; 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; 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; 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; ( 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
; 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 )
;
suppose A6:
width (B * A) > 0
;
the_rank_of (B * A) = the_rank_of Bthen 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
;
verum end;