This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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