Theorem h2hnm

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

	Ref	Expression
Hypotheses	h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
	h2h.2	⊢ 𝑈 ∈ NrmCVec
Assertion	h2hnm	⊢ normℎ = ( normCV ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		h2h.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2		h2h.2	⊢ 𝑈 ∈ NrmCVec
3	1	fveq2i	⊢ ( normCV ‘ 𝑈 ) = ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
4		eqid	⊢ ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
5	4	nmcvfval	⊢ ( normCV ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = ( 2nd ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ )
6		opex	⊢ ⟨ +ℎ , ·ℎ ⟩ ∈ V
7	1 2	eqeltrri	⊢ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec
8		nvex	⊢ ( ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ∈ NrmCVec → ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V ) )
9	7 8	ax-mp	⊢ ( +ℎ ∈ V ∧ ·ℎ ∈ V ∧ normℎ ∈ V )
10	9	simp3i	⊢ normℎ ∈ V
11	6 10	op2nd	⊢ ( 2nd ‘ ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩ ) = normℎ
12	3 5 11	3eqtrri	⊢ normℎ = ( normCV ‘ 𝑈 )