df-nmcv - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-nmcv		Structured version Visualization version GIF version

Definition df-nmcv 31027

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

**Assertion**
Ref	Expression
df-nmcv	⊢ norm_CV = 2^nd

**Detailed syntax breakdown of Definition df-nmcv**
Step	Hyp	Ref	Expression
1		cnmcv 31017	. 2 class norm_CV
2		c2nd 7991	. 2 class 2^nd
3	1, 2	wceq 1570	1 wff norm_CV = 2^nd

Colors of variables: wff setvar class

This definition is used by: nmcvfval 31034