let GF be non empty right_complementable well-unital distributive Abelian add-associative right_zeroed associative doubleLoopStr ; :: thesis: 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; :: thesis: ( 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 ; :: thesis: 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 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; :: thesis: verum

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; :: thesis: ( 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 ; :: thesis: 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

proof

set MY = the lmult of Y;
set AY = the addF of Y;

set VX = the carrier of X;

set AX = the addF of X;

set VV = the carrier of V;

set AV = the addF of V;

the carrier of V c= the carrier of X by A1, Def2;

then A5: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;

the addF of V = the addF of X || the carrier of V by A1, Def2;

then the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def2;

hence the addF of V = the addF of Y || the carrier of V by A5, FUNCT_1:51; :: thesis: verum

end;set VX = the carrier of X;

set AX = the addF of X;

set VV = the carrier of V;

set AV = the addF of V;

the carrier of V c= the carrier of X by A1, Def2;

then A5: [: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:] by ZFMISC_1:96;

the addF of V = the addF of X || the carrier of V by A1, Def2;

then the addF of V = ( the addF of Y || the carrier of X) || the carrier of V by A2, Def2;

hence the addF of V = the addF of Y || the carrier of V by A5, FUNCT_1:51; :: thesis: verum

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; :: thesis: verum