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

Definition df-nmcv 21172
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  |-  normCV  =  2nd

Detailed syntax breakdown of Definition df-nmcv
StepHypRef Expression
1 cnmcv 21162 . 2  class  normCV
2 c2nd 6137 . 2  class  2nd
31, 2wceq 1632 1  wff  normCV  =  2nd
Colors of variables: wff set class
This definition is referenced by:  nmcvfval  21179
  Copyright terms: Public domain W3C validator