# Metamath Proof Explorer

## 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)\phantom{\rule{.4em}{0ex}}\left(\left({norm}_{CV}\left({U}\right)\left({x}\right)=0\to {x}={0}_{\mathrm{vec}}\left({U}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{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)\phantom{\rule{.4em}{0ex}}{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}}$