let K be Field; :: thesis: 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; :: thesis: ( 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 ) ; :: thesis: 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)

Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)

let A, B be Matrix of K; :: thesis: ( 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 ) ; :: thesis: 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

hence
Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B)
by A5, VECTSP_4:27; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( 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) ; :: thesis: 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;

hence x in the carrier of (Space_of_Solutions_of AB) by A1, A2, A3, A4, A5, A6, Def5; :: thesis: verum

end;assume x in the carrier of (Space_of_Solutions_of B) ; :: thesis: 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 :: thesis: X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))end;

then
f in Solutions_of (AB,((len AB) |-> (0. K)))
by A8;per cases
( len A = 0 or len A <> 0 )
;

end;

suppose
len A = 0
; :: thesis: X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K))))

then
( Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) = {{}} & X = {} )
by A4, A5, A9, A12, Th51, MATRIX_0:def 3;

hence X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) by TARSKI:def 1; :: thesis: verum

end;hence X in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) by TARSKI:def 1; :: thesis: verum

suppose A14:
len A <> 0
; :: thesis: 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; :: thesis: verum

end;.= 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; :: thesis: verum

hence x in the carrier of (Space_of_Solutions_of AB) by A1, A2, A3, A4, A5, A6, Def5; :: thesis: verum