let n be Nat; :: thesis: for K being Field
for A being Matrix of n,n,K
for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
let K be Field; :: thesis: for A being Matrix of n,n,K
for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
let A be Matrix of n,n,K; :: thesis: for B being Matrix of K st Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) holds
Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
let B be Matrix of K; :: thesis: ( Det A <> 0. K & width A = len B & ( width B = 0 implies len B = 0 ) implies Space_of_Solutions_of B = Space_of_Solutions_of (A * B) )
assume that
A1: Det A <> 0. K and
A2: width A = len B and
A3: ( width B = 0 implies len B = 0 ) ; :: thesis: Space_of_Solutions_of B = Space_of_Solutions_of (A * B)
set AB = A * B;
A4: len (A * B) = len A by A2, MATRIX_3:def 4;
A5: width (A * B) = width B by A2, MATRIX_3:def 4;
A6: len A = n by MATRIX_0:24;
reconsider AB = A * B as Matrix of n, width B,K by A4, A5, MATRIX_0:24, MATRIX_0:51;
A7: width A = n by MATRIX_0:24;
A8: the carrier of (Space_of_Solutions_of AB) c= the carrier of (Space_of_Solutions_of B)

proof

A is invertible by A1, LAPLACE:34;
then A is_reverse_of A ~ by MATRIX_6:def 4;
then A9: 1. (K,n) = (A ~) * A by MATRIX_6:def 2;
A10: len (A ~) = n by MATRIX_0:24;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in the carrier of (Space_of_Solutions_of AB) or x in the carrier of (Space_of_Solutions_of B) )
assume x in the carrier of (Space_of_Solutions_of AB) ; :: thesis: x in the carrier of (Space_of_Solutions_of B)
then x in Solutions_of (AB,((len AB) |-> (0. K))) by A2, A3, A6, A7, A4, A5, Def5;
then consider f being FinSequence of K such that
A11: f = x and
A12: ColVec2Mx f in Solutions_of (AB,(ColVec2Mx ((len AB) |-> (0. K)))) ;
consider X being Matrix of K such that
A13: X = ColVec2Mx f and
A14: len X = width AB and
A15: width X = width (ColVec2Mx ((len AB) |-> (0. K))) and
A16: AB * X = ColVec2Mx ((len AB) |-> (0. K)) by A12;
A17: width (A ~) = n by MATRIX_0:24;
set BX = B * X;
A18: len (B * X) = len B by A5, A14, MATRIX_3:def 4;
then A19: B * X = (1. (K,n)) * (B * X) by A2, A7, MATRIXR2:68
.= (A ~) * (A * (B * X)) by A2, A6, A9, A17, A18, MATRIX_3:33
.= (A ~) * (ColVec2Mx ((len AB) |-> (0. K))) by A2, A5, A14, A16, MATRIX_3:33
.= (A ~) * (0. (K,(len AB),1)) by Th32 ;

now :: thesis: B * X = 0. (K,(len AB),1)

per cases ( n = 0 or n > 0 ) ;

suppose A20: n = 0 ; :: thesis: B * X = 0. (K,(len AB),1)

then 0. (K,(len AB),1) = {} by A6, A4;
hence B * X = 0. (K,(len AB),1) by A2, A18, A20, MATRIX_0:24; :: thesis: verum

end;

suppose n > 0 ; :: thesis: B * X = 0. (K,(len AB),1)

hence B * X = 0. (K,(len AB),1) by A6, A4, A10, A17, A19, MATRIXR2:18; :: thesis: verum

end;

end;

end;

then B * X = ColVec2Mx ((len AB) |-> (0. K)) by Th32;
then ColVec2Mx f in Solutions_of (B,(ColVec2Mx ((len B) |-> (0. K)))) by A2, A6, A7, A4, A5, A13, A14, A15;
then f in Solutions_of (B,((len B) |-> (0. K))) ;
hence x in the carrier of (Space_of_Solutions_of B) by A3, A11, Def5; :: thesis: verum

end;

( width A = 0 implies len A = 0 ) by A6, MATRIX_0:24;
then Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) by A2, A3, Th72;
then the carrier of (Space_of_Solutions_of B) c= the carrier of (Space_of_Solutions_of (A * B)) by VECTSP_4:def 2;
then the carrier of (Space_of_Solutions_of B) = the carrier of (Space_of_Solutions_of (A * B)) by A8;
hence Space_of_Solutions_of B = Space_of_Solutions_of (A * B) by A5, VECTSP_4:29; :: thesis: verum