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:
set AB = A * B;
A4: len (A * B) = len A by ;
A5: width (A * B) = width B by ;
A6: len A = n by MATRIX_0:24;
reconsider AB = A * B as Matrix of n, width B,K by ;
A7: width A = n by MATRIX_0:24;
A8: the carrier of c= the carrier of
proof
A is invertible by ;
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 or x in the carrier of )
assume x in the carrier of ; :: thesis: x in the carrier of
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 ;
then A19: B * X = (1. (K,n)) * (B * X) by
.= (A ~) * (A * (B * X)) by
.= (A ~) * (ColVec2Mx ((len AB) |-> (0. K))) by
.= (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 ; :: thesis: verum
end;
suppose n > 0 ; :: thesis: B * X = 0. (K,(len AB),1)
hence B * X = 0. (K,(len AB),1) by ; :: 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 by ; :: thesis: verum
end;
( width A = 0 implies len A = 0 ) by ;
then Space_of_Solutions_of B is Subspace of Space_of_Solutions_of (A * B) by A2, A3, Th72;
then the carrier of c= the carrier of (Space_of_Solutions_of (A * B)) by VECTSP_4:def 2;
then the carrier of = the carrier of (Space_of_Solutions_of (A * B)) by A8;
hence Space_of_Solutions_of B = Space_of_Solutions_of (A * B) by ; :: thesis: verum