# Metamath Proof Explorer

## Theorem nvi

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

Ref Expression
Hypotheses nvi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
nvi.2 ${⊢}{G}={+}_{v}\left({U}\right)$
nvi.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
nvi.5 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
nvi.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
Assertion nvi ${⊢}{U}\in \mathrm{NrmCVec}\to \left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$

### Proof

Step Hyp Ref Expression
1 nvi.1 ${⊢}{X}=\mathrm{BaseSet}\left({U}\right)$
2 nvi.2 ${⊢}{G}={+}_{v}\left({U}\right)$
3 nvi.4 ${⊢}{S}={\cdot }_{\mathrm{𝑠OLD}}\left({U}\right)$
4 nvi.5 ${⊢}{Z}={0}_{\mathrm{vec}}\left({U}\right)$
5 nvi.6 ${⊢}{N}={norm}_{CV}\left({U}\right)$
6 eqid ${⊢}{1}^{st}\left({U}\right)={1}^{st}\left({U}\right)$
7 6 5 nvop2 ${⊢}{U}\in \mathrm{NrmCVec}\to {U}=⟨{1}^{st}\left({U}\right),{N}⟩$
8 6 2 3 nvvop ${⊢}{U}\in \mathrm{NrmCVec}\to {1}^{st}\left({U}\right)=⟨{G},{S}⟩$
9 8 opeq1d ${⊢}{U}\in \mathrm{NrmCVec}\to ⟨{1}^{st}\left({U}\right),{N}⟩=⟨⟨{G},{S}⟩,{N}⟩$
10 7 9 eqtrd ${⊢}{U}\in \mathrm{NrmCVec}\to {U}=⟨⟨{G},{S}⟩,{N}⟩$
11 id ${⊢}{U}\in \mathrm{NrmCVec}\to {U}\in \mathrm{NrmCVec}$
12 10 11 eqeltrrd ${⊢}{U}\in \mathrm{NrmCVec}\to ⟨⟨{G},{S}⟩,{N}⟩\in \mathrm{NrmCVec}$
13 1 2 bafval ${⊢}{X}=\mathrm{ran}{G}$
14 eqid ${⊢}\mathrm{GId}\left({G}\right)=\mathrm{GId}\left({G}\right)$
15 13 14 isnv ${⊢}⟨⟨{G},{S}⟩,{N}⟩\in \mathrm{NrmCVec}↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}=\mathrm{GId}\left({G}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
16 12 15 sylib ${⊢}{U}\in \mathrm{NrmCVec}\to \left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}=\mathrm{GId}\left({G}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
17 2 4 0vfval ${⊢}{U}\in \mathrm{NrmCVec}\to {Z}=\mathrm{GId}\left({G}\right)$
18 17 eqeq2d ${⊢}{U}\in \mathrm{NrmCVec}\to \left({x}={Z}↔{x}=\mathrm{GId}\left({G}\right)\right)$
19 18 imbi2d ${⊢}{U}\in \mathrm{NrmCVec}\to \left(\left({N}\left({x}\right)=0\to {x}={Z}\right)↔\left({N}\left({x}\right)=0\to {x}=\mathrm{GId}\left({G}\right)\right)\right)$
20 19 3anbi1d ${⊢}{U}\in \mathrm{NrmCVec}\to \left(\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)↔\left(\left({N}\left({x}\right)=0\to {x}=\mathrm{GId}\left({G}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
21 20 ralbidv ${⊢}{U}\in \mathrm{NrmCVec}\to \left(\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)↔\forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}=\mathrm{GId}\left({G}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$
22 21 3anbi3d ${⊢}{U}\in \mathrm{NrmCVec}\to \left(\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)↔\left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}=\mathrm{GId}\left({G}\right)\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)\right)$
23 16 22 mpbird ${⊢}{U}\in \mathrm{NrmCVec}\to \left(⟨{G},{S}⟩\in {CVec}_{\mathrm{OLD}}\wedge {N}:{X}⟶ℝ\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\left(\left({N}\left({x}\right)=0\to {x}={Z}\right)\wedge \forall {y}\in ℂ\phantom{\rule{.4em}{0ex}}{N}\left({y}{S}{x}\right)=\left|{y}\right|{N}\left({x}\right)\wedge \forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{N}\left({x}{G}{y}\right)\le {N}\left({x}\right)+{N}\left({y}\right)\right)\right)$