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