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 ⊢ U = + ℎ ⋅ ℎ norm ℎ
h2h.2 ⊢ U ∈ NrmCVec
Assertion h2hnm ⊢ norm ℎ = norm CV ⁡ U

Proof

Step Hyp Ref Expression
1 h2h.1 ⊢ U = + ℎ ⋅ ℎ norm ℎ
2 h2h.2 ⊢ U ∈ NrmCVec
3 1 fveq2i ⊢ norm CV ⁡ U = norm CV ⁡ + ℎ ⋅ ℎ norm ℎ
4 eqid ⊢ norm CV ⁡ + ℎ ⋅ ℎ norm ℎ = norm CV ⁡ + ℎ ⋅ ℎ norm ℎ
5 4 nmcvfval ⊢ norm CV ⁡ + ℎ ⋅ ℎ norm ℎ = 2 nd ⁡ + ℎ ⋅ ℎ 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 ⊢ 2 nd ⁡ + ℎ ⋅ ℎ norm ℎ = norm ℎ
12 3 5 11 3eqtrri ⊢ norm ℎ = norm CV ⁡ U