Theorem hhnm

Description: The norm function of Hilbert space. (Contributed by NM, 17-Nov-2007) (New usage is discouraged.)

	Ref	Expression
Hypothesis	hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
Assertion	hhnm	⊢ normℎ = ( normCV ‘ 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		hhnv.1	⊢ 𝑈 = ⟨ ⟨ +ℎ , ·ℎ ⟩ , normℎ ⟩
2	1	hhnv	⊢ 𝑈 ∈ NrmCVec
3	1 2	h2hnm	⊢ normℎ = ( normCV ‘ 𝑈 )