let K be Field; for A, B being Matrix of K st width A = len B & ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
let A, B be Matrix of K; ( width A = len B & ( width A = 0 implies len A = 0 ) & ( width B = 0 implies len B = 0 ) implies Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) )
assume that
A1:
width A = len B
and
A2:
( width A = 0 implies len A = 0 )
and
A3:
( width B = 0 implies len B = 0 )
; Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
set AB = A * B;
A4:
len (A * B) = len A
by A1, MATRIX_3:def 4;
A5:
width (A * B) = width B
by A1, MATRIX_3:def 4;
then reconsider AB = A * B as Matrix of len A, width B,K by A4, MATRIX_0:51;
the carrier of (Space_of_Solutions_of B) c= the carrier of (Space_of_Solutions_of AB)
proof
let x be
object ;
TARSKI:def 3 ( not x in the carrier of (Space_of_Solutions_of B) or x in the carrier of (Space_of_Solutions_of AB) )
assume
x in the
carrier of
(Space_of_Solutions_of B)
;
x in the carrier of (Space_of_Solutions_of AB)
then
x in Solutions_of (
B,
((len B) |-> (0. K)))
by A3, Def5;
then consider f being
FinSequence of
K such that A6:
f = x
and A7:
ColVec2Mx f in Solutions_of (
B,
(ColVec2Mx ((len B) |-> (0. K))))
;
consider X being
Matrix of
K such that A8:
X = ColVec2Mx f
and A9:
len X = width B
and A10:
width X = width (ColVec2Mx ((len B) |-> (0. K)))
and A11:
B * X = ColVec2Mx ((len B) |-> (0. K))
by A7;
A12:
ColVec2Mx ((len AB) |-> (0. K)) = 0. (
K,
(len A),1)
by A4, Th32;
A13:
ColVec2Mx ((len B) |-> (0. K)) = 0. (
K,
(len B),1)
by Th32;
now X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))per cases
( len A = 0 or len A <> 0 )
;
suppose A14:
len A <> 0
;
X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))then A15:
width (ColVec2Mx ((len AB) |-> (0. K))) =
1
by A4, Th26
.=
width (ColVec2Mx ((len B) |-> (0. K)))
by A1, A2, A14, Th26
;
ColVec2Mx ((len AB) |-> (0. K)) =
A * (B * X)
by A1, A2, A11, A13, A12, A14, MATRIXR2:18
.=
AB * X
by A1, A9, MATRIX_3:33
;
hence
X in Solutions_of (
AB,
(ColVec2Mx ((len AB) |-> (0. K))))
by A5, A9, A10, A15;
verum end;
then
f in Solutions_of (
AB,
((len AB) |-> (0. K)))
by A8;
hence
x in the
carrier of
(Space_of_Solutions_of AB)
by A1, A2, A3, A4, A5, A6, Def5;
verum
end;
hence
Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
by A5, VECTSP_4:27; verum