let n be Nat; 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; 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; 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; ( 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 )
; 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 ;
TARSKI:def 3 ( 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)
;
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
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;
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; verum