Metamath Proof Explorer

Theorem nmcvfval

Description: Value of the norm function in a normed complex vector space. (Contributed by NM, 25-Apr-2007) (New usage is discouraged.)

Ref Expression
Hypothesis nmfval.6 
|- N = ( normCV ` U )
Assertion nmcvfval 
|- N = ( 2nd ` U )

Proof

Step Hyp Ref Expression
1 nmfval.6 
 |-  N = ( normCV ` U )
2 df-nmcv 
 |-  normCV = 2nd
3 2 fveq1i 
 |-  ( normCV ` U ) = ( 2nd ` U )
4 1 3 eqtri 
 |-  N = ( 2nd ` U )