Theorem h2hnm

Description: The norm function of Hilbert space. (Contributed by NM, 5-Jun-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2h.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	h2h.2	$$⊢U\in \mathrm{NrmCVec}$$
Assertion	h2hnm	$$⊢{norm}_{ℎ}={norm}_{CV}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		h2h.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		h2h.2	$$⊢U\in \mathrm{NrmCVec}$$
3	1	fveq2i	$$⊢{norm}_{CV}\left(U\right)={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
4		eqid	$$⊢{norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)={norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
5	4	nmcvfval	$$⊢{norm}_{CV}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)=2^{nd}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)$$
6		opex	$$⊢⟨{+}_{ℎ},{\cdot }_{ℎ}⟩\in \mathrm{V}$$
7	1 2	eqeltrri	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}$$
8		nvex	$$⊢⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\in \mathrm{NrmCVec}\to \left({+}_{ℎ}\in \mathrm{V}\wedge {\cdot }_{ℎ}\in \mathrm{V}\wedge {norm}_{ℎ}\in \mathrm{V}\right)$$
9	7 8	ax-mp	$$⊢\left({+}_{ℎ}\in \mathrm{V}\wedge {\cdot }_{ℎ}\in \mathrm{V}\wedge {norm}_{ℎ}\in \mathrm{V}\right)$$
10	9	simp3i	$$⊢{norm}_{ℎ}\in \mathrm{V}$$
11	6 10	op2nd	$$⊢2^{nd}\left(⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩\right)={norm}_{ℎ}$$
12	3 5 11	3eqtrri	$$⊢{norm}_{ℎ}={norm}_{CV}\left(U\right)$$