This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ‘ 𝑈 )