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 𝑁 = ( normCV𝑈 )
Assertion nmcvfval 𝑁 = ( 2nd𝑈 )

Proof

Step Hyp Ref Expression
1 nmfval.6 𝑁 = ( normCV𝑈 )
2 df-nmcv normCV = 2nd
3 2 fveq1i ( normCV𝑈 ) = ( 2nd𝑈 )
4 1 3 eqtri 𝑁 = ( 2nd𝑈 )