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