Theorem nvf

Description: Mapping for the norm function. (Contributed by NM, 11-Nov-2006) (New usage is discouraged.)

	Ref	Expression
Hypotheses	nvf.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
	nvf.6	$$⊢N={norm}_{CV}\left(U\right)$$
Assertion	nvf	$$⊢U\in \mathrm{NrmCVec}\to N:X⟶ℝ$$

Proof

Step	Hyp	Ref	Expression
1		nvf.1	$$⊢X=\mathrm{BaseSet}\left(U\right)$$
2		nvf.6	$$⊢N={norm}_{CV}\left(U\right)$$
3		eqid	$$⊢{+}_v\left(U\right)={+}_v\left(U\right)$$
4		eqid	$$⊢{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
5		eqid	$$⊢0_{\mathrm{vec}}\left(U\right)=0_{\mathrm{vec}}\left(U\right)$$
6	1 3 4 5 2	nvi	$$⊢U\in \mathrm{NrmCVec}\to \left(⟨{+}_v\left(U\right),{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)⟩\in {CVec}_{\mathrm{OLD}}\wedge N:X⟶ℝ\wedge \forall x\in X\left(\left(N\left(x\right)=0\to x=0_{\mathrm{vec}}\left(U\right)\right)\wedge \forall y\in ℂN\left(y{\cdot }_{\mathrm{𝑠OLD}}\left(U\right)x\right)=\left|y\right|N\left(x\right)\wedge \forall y\in XN\left(x{+}_v\left(U\right)y\right)\le N\left(x\right)+N\left(y\right)\right)\right)$$
7	6	simp2d	$$⊢U\in \mathrm{NrmCVec}\to N:X⟶ℝ$$