Definition df-nmcv

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

	Ref	Expression
Assertion	df-nmcv	$$⊢{norm}_{CV}=2^{nd}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cnmcv	$$class{norm}_{CV}$$
1		c2nd	$$class{2}^{nd}$$
2	0 1	wceq	$$wff{norm}_{CV}=2^{nd}$$