Metamath Proof Explorer


Theorem hhnm

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

Ref Expression
Hypothesis hhnv.1
|- U = <. <. +h , .h >. , normh >.
Assertion hhnm
|- normh = ( normCV ` U )

Proof

Step Hyp Ref Expression
1 hhnv.1
 |-  U = <. <. +h , .h >. , normh >.
2 1 hhnv
 |-  U e. NrmCVec
3 1 2 h2hnm
 |-  normh = ( normCV ` U )