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={norm}_{CV}\left(U\right)$$
Assertion	nmcvfval	$$⊢N=2^{nd}\left(U\right)$$

Proof

Step	Hyp	Ref	Expression
1		nmfval.6	$$⊢N={norm}_{CV}\left(U\right)$$
2		df-nmcv	$$⊢{norm}_{CV}=2^{nd}$$
3	2	fveq1i	$$⊢{norm}_{CV}\left(U\right)=2^{nd}\left(U\right)$$
4	1 3	eqtri	$$⊢N=2^{nd}\left(U\right)$$