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

Definition df-hmo 21329
Description: Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.)
Assertion
Ref Expression
df-hmo  |-  HmOp  =  ( u  e.  NrmCVec  |->  { t  e.  dom  ( u adj u )  |  ( ( u adj u ) `  t
)  =  t } )
Distinct variable group:    u, t

Detailed syntax breakdown of Definition df-hmo
StepHypRef Expression
1 chmo 21327 . 2  class  HmOp
2 vu . . 3  set  u
3 cnv 21140 . . 3  class  NrmCVec
4 vt . . . . . . 7  set  t
54cv 1622 . . . . . 6  class  t
62cv 1622 . . . . . . 7  class  u
7 caj 21326 . . . . . . 7  class  adj
86, 6, 7co 5858 . . . . . 6  class  ( u adj u )
95, 8cfv 5255 . . . . 5  class  ( ( u adj u ) `
 t )
109, 5wceq 1623 . . . 4  wff  ( ( u adj u ) `
 t )  =  t
118cdm 4689 . . . 4  class  dom  (
u adj u )
1210, 4, 11crab 2547 . . 3  class  { t  e.  dom  ( u adj u )  |  ( ( u adj u ) `  t
)  =  t }
132, 3, 12cmpt 4077 . 2  class  ( u  e.  NrmCVec  |->  { t  e. 
dom  ( u adj u )  |  ( ( u adj u
) `  t )  =  t } )
141, 13wceq 1623 1  wff  HmOp  =  ( u  e.  NrmCVec  |->  { t  e.  dom  ( u adj u )  |  ( ( u adj u ) `  t
)  =  t } )
Colors of variables: wff set class
This definition is referenced by:  hmoval  21388
  Copyright terms: Public domain W3C validator