let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; for V, X, Y being non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF st V is Subspace of X & X is Subspace of Y holds
V is Subspace of Y
let V, X, Y be non empty right_complementable vector-distributive scalar-distributive scalar-associative scalar-unital Abelian add-associative right_zeroed ModuleStr over GF; ( V is Subspace of X & X is Subspace of Y implies V is Subspace of Y )
assume that
A1:
V is Subspace of X
and
A2:
X is Subspace of Y
; V is Subspace of Y
( the carrier of V c= the carrier of X & the carrier of X c= the carrier of Y )
by A1, A2, Def2;
then A3:
the carrier of V c= the carrier of Y
;
A4:
the addF of V = the addF of Y || the carrier of V
set MY = the lmult of Y;
set MX = the lmult of X;
set MV = the lmult of V;
set VX = the carrier of X;
set VV = the carrier of V;
the carrier of V c= the carrier of X
by A1, Def2;
then A6:
[: the carrier of GF, the carrier of V:] c= [: the carrier of GF, the carrier of X:]
by ZFMISC_1:95;
the lmult of V = the lmult of X | [: the carrier of GF, the carrier of V:]
by A1, Def2;
then
the lmult of V = ( the lmult of Y | [: the carrier of GF, the carrier of X:]) | [: the carrier of GF, the carrier of V:]
by A2, Def2;
then A7:
the lmult of V = the lmult of Y | [: the carrier of GF, the carrier of V:]
by A6, FUNCT_1:51;
0. V = 0. X
by A1, Def2;
then
0. V = 0. Y
by A2, Def2;
hence
V is Subspace of Y
by A3, A4, A7, Def2; verum