let K be Field; for A, B being Matrix of K st width A = len B holds
( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )
let A, B be Matrix of K; ( width A = len B implies ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B ) )
assume A1:
width A = len B
; ( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )
set AB = A * B;
A2:
width (A * B) = width B
by A1, MATRIX_3:def 4;
per cases
( the_rank_of (A * B) = 0 or the_rank_of (A * B) > 0 )
;
suppose A3:
the_rank_of (A * B) > 0
;
( the_rank_of (A * B) <= the_rank_of A & the_rank_of (A * B) <= the_rank_of B )set AT =
A @ ;
A4:
width (A * B) > 0
by A3, MATRIX13:74;
then A5:
width A > 0
by A1, A2, MATRIX_0:def 3;
then A6:
len (A @) = width A
by MATRIX_0:54;
set BT =
B @ ;
set BA =
(B @) * (A @);
width (A @) = len A
by A5, MATRIX_0:54;
then A7:
(
width (A @) = 0 implies
len (A @) = 0 )
by A5, MATRIX_0:def 3;
then A8:
dim (Space_of_Solutions_of (A @)) = (width (A @)) - (the_rank_of (A @))
by Th68;
A9:
width (B @) = len B
by A2, A4, MATRIX_0:54;
then
(
width (B @) = 0 implies
len (B @) = 0 )
by A2, A4, MATRIX_0:def 3;
then A10:
Space_of_Solutions_of (A @) is
Subspace of
Space_of_Solutions_of ((B @) * (A @))
by A1, A6, A9, A7, Th72;
A11:
width ((B @) * (A @)) = width (A @)
by A1, A6, A9, MATRIX_3:def 4;
then
dim (Space_of_Solutions_of ((B @) * (A @))) = (width ((B @) * (A @))) - (the_rank_of ((B @) * (A @)))
by A5, A7, Th68, MATRIX_0:54;
then
(width (A @)) - (the_rank_of (A @)) <= (width (A @)) - (the_rank_of ((B @) * (A @)))
by A11, A10, A8, VECTSP_9:25;
then
the_rank_of (A @) >= the_rank_of ((B @) * (A @))
by XREAL_1:10;
then A12:
the_rank_of A >= the_rank_of ((B @) * (A @))
by MATRIX13:84;
(
width A = 0 implies
len A = 0 )
by A1, A2, A4, MATRIX_0:def 3;
then A13:
Space_of_Solutions_of B is
Subspace of
Space_of_Solutions_of (A * B)
by A1, A2, A4, Th72;
(
dim (Space_of_Solutions_of B) = (width B) - (the_rank_of B) &
dim (Space_of_Solutions_of (A * B)) = (width (A * B)) - (the_rank_of (A * B)) )
by A2, A4, Th68;
then A14:
(width B) - (the_rank_of B) <= (width B) - (the_rank_of (A * B))
by A2, A13, VECTSP_9:25;
(B @) * (A @) = (A * B) @
by A1, A2, A4, MATRIX_3:22;
hence
(
the_rank_of (A * B) <= the_rank_of A &
the_rank_of (A * B) <= the_rank_of B )
by A14, A12, MATRIX13:84, XREAL_1:10;
verum end;