Metamath Proof Explorer

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 
|- normCV = 2nd

Detailed syntax breakdown

Step Hyp Ref Expression
0 cnmcv 
 |-  normCV
1 c2nd 
 |-  2nd
2 0 1 wceq 
 |-  normCV = 2nd