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)

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

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

( width A = 0 implies len A = 0 )
by A6, MATRIX_0:24;
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 ;

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;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)

then
B * X = ColVec2Mx ((len AB) |-> (0. K))
by Th32;end;

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

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