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 )