let V, X, Y be RealUnitarySpace; ( 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, Def1;
hence
the carrier of V c= the carrier of Y
; RUSUB_1:def 1 ( 0. V = 0. Y & the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
0. V = 0. X
by A1, Def1;
hence
0. V = 0. Y
by A2, Def1; ( the addF of V = the addF of Y || the carrier of V & the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
thus
the addF of V = the addF of Y || the carrier of V
( the Mult of V = the Mult of Y | [:REAL, the carrier of V:] & the scalar of V = the scalar of Y || the carrier of V )
thus
the Mult of V = the Mult of Y | [:REAL, the carrier of V:]
the scalar of V = the scalar of Y || the carrier of Vproof
set MY = the
Mult of
Y;
set VX = the
carrier of
X;
set MX = the
Mult of
X;
set VV = the
carrier of
V;
set MV = the
Mult of
V;
the
carrier of
V c= the
carrier of
X
by A1, Def1;
then A4:
[:REAL, the carrier of V:] c= [:REAL, the carrier of X:]
by ZFMISC_1:95;
the
Mult of
V = the
Mult of
X | [:REAL, the carrier of V:]
by A1, Def1;
then
the
Mult of
V = ( the Mult of Y | [:REAL, the carrier of X:]) | [:REAL, the carrier of V:]
by A2, Def1;
hence
the
Mult of
V = the
Mult of
Y | [:REAL, the carrier of V:]
by A4, FUNCT_1:51;
verum
end;
set SY = the scalar of Y;
set SX = the scalar of X;
set SV = the scalar 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, Def1;
then A5:
[: the carrier of V, the carrier of V:] c= [: the carrier of X, the carrier of X:]
by ZFMISC_1:96;
the scalar of V = the scalar of X || the carrier of V
by A1, Def1;
then
the scalar of V = ( the scalar of Y || the carrier of X) || the carrier of V
by A2, Def1;
hence
the scalar of V = the scalar of Y || the carrier of V
by A5, FUNCT_1:51; verum