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 = <. <. +h , .h >. , normh >.
h2h.2
|- U e. NrmCVec
Assertion h2hnm
|- normh = ( normCV ` U )

Proof

Step Hyp Ref Expression
1 h2h.1
 |-  U = <. <. +h , .h >. , normh >.
2 h2h.2
 |-  U e. NrmCVec
3 1 fveq2i
 |-  ( normCV ` U ) = ( normCV ` <. <. +h , .h >. , normh >. )
4 eqid
 |-  ( normCV ` <. <. +h , .h >. , normh >. ) = ( normCV ` <. <. +h , .h >. , normh >. )
5 4 nmcvfval
 |-  ( normCV ` <. <. +h , .h >. , normh >. ) = ( 2nd ` <. <. +h , .h >. , normh >. )
6 opex
 |-  <. +h , .h >. e. _V
7 1 2 eqeltrri
 |-  <. <. +h , .h >. , normh >. e. NrmCVec
8 nvex
 |-  ( <. <. +h , .h >. , normh >. e. NrmCVec -> ( +h e. _V /\ .h e. _V /\ normh e. _V ) )
9 7 8 ax-mp
 |-  ( +h e. _V /\ .h e. _V /\ normh e. _V )
10 9 simp3i
 |-  normh e. _V
11 6 10 op2nd
 |-  ( 2nd ` <. <. +h , .h >. , normh >. ) = normh
12 3 5 11 3eqtrri
 |-  normh = ( normCV ` U )