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

Definition df-nmcv 21156
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 21146 . 2  class  normCV
2 c2nd 6121 . 2  class  2nd
31, 2wceq 1623 1  wff  normCV  =  2nd
Colors of variables: wff set class
This definition is referenced by:  nmcvfval  21163
  Copyright terms: Public domain W3C validator