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

Definition df-leop 22432
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 21538 . 2  class  <_op
2 vu . . . . . . 7  set  u
32cv 1622 . . . . . 6  class  u
4 vt . . . . . . 7  set  t
54cv 1622 . . . . . 6  class  t
6 chod 21520 . . . . . 6  class  -op
73, 5, 6co 5858 . . . . 5  class  ( u  -op  t )
8 cho 21530 . . . . 5  class  HrmOp
97, 8wcel 1684 . . . 4  wff  ( u  -op  t )  e. 
HrmOp
10 cc0 8737 . . . . . 6  class  0
11 vx . . . . . . . . 9  set  x
1211cv 1622 . . . . . . . 8  class  x
1312, 7cfv 5255 . . . . . . 7  class  ( ( u  -op  t ) `
 x )
14 csp 21502 . . . . . . 7  class  .ih
1513, 12, 14co 5858 . . . . . 6  class  ( ( ( u  -op  t
) `  x )  .ih  x )
16 cle 8868 . . . . . 6  class  <_
1710, 15, 16wbr 4023 . . . . 5  wff  0  <_  ( ( ( u  -op  t ) `  x )  .ih  x
)
18 chil 21499 . . . . 5  class  ~H
1917, 11, 18wral 2543 . . . 4  wff  A. x  e.  ~H  0  <_  (
( ( u  -op  t ) `  x
)  .ih  x )
209, 19wa 358 . . 3  wff  ( ( u  -op  t )  e.  HrmOp  /\  A. x  e.  ~H  0  <_  (
( ( u  -op  t ) `  x
)  .ih  x )
)
2120, 4, 2copab 4076 . 2  class  { <. t ,  u >.  |  ( ( u  -op  t
)  e.  HrmOp  /\  A. x  e.  ~H  0  <_  ( ( ( u  -op  t ) `  x )  .ih  x
) ) }
221, 21wceq 1623 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  22702
  Copyright terms: Public domain W3C validator