HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  df-leop Unicode version

Definition df-leop 22424
Description: Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that  ( ~H  X.  0H )  <_op  T means that  T is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-leop  |-  <_op  =  { <. t ,  u >.  |  ( ( u  -op  t )  e. 
HrmOp  /\  A. x  e. 
~H  0  <_  (
( ( u  -op  t ) `  x
)  .ih  x )
) }
Distinct variable group:    u, t, x

Detailed syntax breakdown of Definition df-leop
StepHypRef Expression
1 cleo 21530 . 2  class  <_op
2 vu . . . . . . 7  set  u
32cv 1627 . . . . . 6  class  u
4 vt . . . . . . 7  set  t
54cv 1627 . . . . . 6  class  t
6 chod 21512 . . . . . 6  class  -op
73, 5, 6co 5819 . . . . 5  class  ( u  -op  t )
8 cho 21522 . . . . 5  class  HrmOp
97, 8wcel 1688 . . . 4  wff  ( u  -op  t )  e. 
HrmOp
10 cc0 8732 . . . . . 6  class  0
11 vx . . . . . . . . 9  set  x
1211cv 1627 . . . . . . . 8  class  x
1312, 7cfv 5221 . . . . . . 7  class  ( ( u  -op  t ) `
 x )
14 csp 21494 . . . . . . 7  class  .ih
1513, 12, 14co 5819 . . . . . 6  class  ( ( ( u  -op  t
) `  x )  .ih  x )
16 cle 8863 . . . . . 6  class  <_
1710, 15, 16wbr 4024 . . . . 5  wff  0  <_  ( ( ( u  -op  t ) `  x )  .ih  x
)
18 chil 21491 . . . . 5  class  ~H
1917, 11, 18wral 2544 . . . 4  wff  A. x  e.  ~H  0  <_  (
( ( u  -op  t ) `  x
)  .ih  x )
209, 19wa 360 . . 3  wff  ( ( u  -op  t )  e.  HrmOp  /\  A. x  e.  ~H  0  <_  (
( ( u  -op  t ) `  x
)  .ih  x )
)
2120, 4, 2copab 4077 . 2  class  { <. t ,  u >.  |  ( ( u  -op  t
)  e.  HrmOp  /\  A. x  e.  ~H  0  <_  ( ( ( u  -op  t ) `  x )  .ih  x
) ) }
221, 21wceq 1628 1  wff  <_op  =  { <. t ,  u >.  |  ( ( u  -op  t )  e. 
HrmOp  /\  A. x  e. 
~H  0  <_  (
( ( u  -op  t ) `  x
)  .ih  x )
) }
Colors of variables: wff set class
This definition is referenced by:  leopg  22694
  Copyright terms: Public domain W3C validator