Theorem nvvc

Description: The vector space component of a normed complex vector space. (Contributed by NM, 28-Nov-2006) (Revised by Mario Carneiro, 21-Dec-2013) (New usage is discouraged.)

	Ref	Expression
Hypothesis	nvvc.1	$$⊢W=1^{st}\left(U\right)$$
Assertion	nvvc	$$⊢U\in \mathrm{NrmCVec}\to W\in {CVec}_{\mathrm{OLD}}$$

Proof

Step	Hyp	Ref	Expression
1		nvvc.1	$$⊢W=1^{st}\left(U\right)$$
2		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
3		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4	1 2 3	nvvop	$$⊢U\in \mathrm{NrmCVec}\to W=⟨{+}_v\left(U\right),{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)⟩$$
5		eqid	$$⊢\mathrm{BaseSet}\left(U\right)=\mathrm{BaseSet}\left(U\right)$$
6		eqid	$$⊢0_{\mathrm{vec}}\left(U\right)=0_{\mathrm{vec}}\left(U\right)$$
7		eqid	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(U\right)$$
8	5 2 3 6 7	nvi	$$⊢U\in \mathrm{NrmCVec}\to \left(⟨{+}_v\left(U\right),{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)⟩\in {CVec}_{\mathrm{OLD}}\wedge {norm}_{CV}\left(U\right):\mathrm{BaseSet}\left(U\right)⟶ℝ\wedge \forall x\in \mathrm{BaseSet}\left(U\right)\left(\left({norm}_{CV}\left(U\right)\left(x\right)=0\to x=0_{\mathrm{vec}}\left(U\right)\right)\wedge \forall y\in ℂ{norm}_{CV}\left(U\right)\left(y{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)x\right)=\left|y\right|{norm}_{CV}\left(U\right)\left(x\right)\wedge \forall y\in \mathrm{BaseSet}\left(U\right){norm}_{CV}\left(U\right)\left(x{+}_v\left(U\right)y\right)\le {norm}_{CV}\left(U\right)\left(x\right)+{norm}_{CV}\left(U\right)\left(y\right)\right)\right)$$
9	8	simp1d	$$⊢U\in \mathrm{NrmCVec}\to ⟨{+}_v\left(U\right),{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)⟩\in {CVec}_{\mathrm{OLD}}$$
10	4 9	eqeltrd	$$⊢U\in \mathrm{NrmCVec}\to W\in {CVec}_{\mathrm{OLD}}$$