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

Definition df-ims 21157
Description: Define the induced metric on a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.)
Assertion
Ref Expression
df-ims  |-  IndMet  =  ( u  e.  NrmCVec  |->  ( (
normCV
`  u )  o.  ( -v `  u
) ) )

Detailed syntax breakdown of Definition df-ims
StepHypRef Expression
1 cims 21147 . 2  class  IndMet
2 vu . . 3  set  u
3 cnv 21140 . . 3  class  NrmCVec
42cv 1622 . . . . 5  class  u
5 cnmcv 21146 . . . . 5  class  normCV
64, 5cfv 5255 . . . 4  class  ( normCV `  u )
7 cnsb 21145 . . . . 5  class  -v
84, 7cfv 5255 . . . 4  class  ( -v
`  u )
96, 8ccom 4693 . . 3  class  ( (
normCV
`  u )  o.  ( -v `  u
) )
102, 3, 9cmpt 4077 . 2  class  ( u  e.  NrmCVec  |->  ( ( normCV `  u )  o.  ( -v `  u ) ) )
111, 10wceq 1623 1  wff  IndMet  =  ( u  e.  NrmCVec  |->  ( (
normCV
`  u )  o.  ( -v `  u
) ) )
Colors of variables: wff set class
This definition is referenced by:  imsval  21254
  Copyright terms: Public domain W3C validator