Metamath Proof Explorer


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𝑈 )