Theorem sspid

Description: A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008) (New usage is discouraged.)

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

Proof

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