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

Definition df-hmo 22100
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 22098 . 2  class  HmOp
2 vu . . 3  set  u
3 cnv 21911 . . 3  class  NrmCVec
4 vt . . . . . . 7  set  t
54cv 1648 . . . . . 6  class  t
62cv 1648 . . . . . . 7  class  u
7 caj 22097 . . . . . . 7  class  adj
86, 6, 7co 6020 . . . . . 6  class  ( u adj u )
95, 8cfv 5394 . . . . 5  class  ( ( u adj u ) `
 t )
109, 5wceq 1649 . . . 4  wff  ( ( u adj u ) `
 t )  =  t
118cdm 4818 . . . 4  class  dom  (
u adj u )
1210, 4, 11crab 2653 . . 3  class  { t  e.  dom  ( u adj u )  |  ( ( u adj u ) `  t
)  =  t }
132, 3, 12cmpt 4207 . 2  class  ( u  e.  NrmCVec  |->  { t  e. 
dom  ( u adj u )  |  ( ( u adj u
) `  t )  =  t } )
141, 13wceq 1649 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  22159
  Copyright terms: Public domain W3C validator