Theorem sspnv

Description: A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008) (New usage is discouraged.)

	Ref	Expression
Hypothesis	sspnv.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
Assertion	sspnv	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to W\in \mathrm{NrmCVec}$$

Proof

Step	Hyp	Ref	Expression
1		sspnv.h	$$⊢H=\mathrm{SubSp}\left(U\right)$$
2		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
3		eqid	$$⊢{+}_v\left(W\right)={+}_v\left(W\right)$$
4		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
5		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(W\right)={\cdot }_{\mathrm{𝑠OLD}}\left(W\right)$$
6		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
7		eqid	$$⊢{norm}_{CV}\left(W\right)={norm}_{CV}\left(W\right)$$
8	2 3 4 5 6 7 1	isssp	$$⊢U\in \mathrm{NrmCVec}\to \left(W\in H\leftrightarrow \left(W\in \mathrm{NrmCVec}\wedge \left({+}_v\left(W\right)\subseteq {+}_v\left(U\right)\wedge {\cdot }_{\mathrm{𝑠OLD}}\left(W\right)\subseteq {\cdot }_{\mathrm{𝑠OLD}}\left(U\right)\wedge {norm}_{CV}\left(W\right)\subseteq {norm}_{CV}\left(U\right)\right)\right)\right)$$
9	8	simprbda	$$⊢\left(U\in \mathrm{NrmCVec}\wedge W\in H\right)\to W\in \mathrm{NrmCVec}$$