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

Definition df-leop 30836
Description: Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( โ„‹ ร— 0โ„‹) โ‰คop ๐‘‡ means that ๐‘‡ is a positive operator. (Contributed by NM, 23-Jul-2006.) (New usage is discouraged.)
Assertion
Ref Expression
df-leop โ‰คop = {โŸจ๐‘ก, ๐‘ขโŸฉ โˆฃ ((๐‘ข โˆ’op ๐‘ก) โˆˆ HrmOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ 0 โ‰ค (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ))}
Distinct variable group:   ๐‘ข,๐‘ก,๐‘ฅ

Detailed syntax breakdown of Definition df-leop
StepHypRef Expression
1 cleo 29942 . 2 class โ‰คop
2 vu . . . . . . 7 setvar ๐‘ข
32cv 1541 . . . . . 6 class ๐‘ข
4 vt . . . . . . 7 setvar ๐‘ก
54cv 1541 . . . . . 6 class ๐‘ก
6 chod 29924 . . . . . 6 class โˆ’op
73, 5, 6co 7358 . . . . 5 class (๐‘ข โˆ’op ๐‘ก)
8 cho 29934 . . . . 5 class HrmOp
97, 8wcel 2107 . . . 4 wff (๐‘ข โˆ’op ๐‘ก) โˆˆ HrmOp
10 cc0 11056 . . . . . 6 class 0
11 vx . . . . . . . . 9 setvar ๐‘ฅ
1211cv 1541 . . . . . . . 8 class ๐‘ฅ
1312, 7cfv 6497 . . . . . . 7 class ((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ)
14 csp 29906 . . . . . . 7 class ยทih
1513, 12, 14co 7358 . . . . . 6 class (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ)
16 cle 11195 . . . . . 6 class โ‰ค
1710, 15, 16wbr 5106 . . . . 5 wff 0 โ‰ค (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ)
18 chba 29903 . . . . 5 class โ„‹
1917, 11, 18wral 3061 . . . 4 wff โˆ€๐‘ฅ โˆˆ โ„‹ 0 โ‰ค (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ)
209, 19wa 397 . . 3 wff ((๐‘ข โˆ’op ๐‘ก) โˆˆ HrmOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ 0 โ‰ค (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ))
2120, 4, 2copab 5168 . 2 class {โŸจ๐‘ก, ๐‘ขโŸฉ โˆฃ ((๐‘ข โˆ’op ๐‘ก) โˆˆ HrmOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ 0 โ‰ค (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ))}
221, 21wceq 1542 1 wff โ‰คop = {โŸจ๐‘ก, ๐‘ขโŸฉ โˆฃ ((๐‘ข โˆ’op ๐‘ก) โˆˆ HrmOp โˆง โˆ€๐‘ฅ โˆˆ โ„‹ 0 โ‰ค (((๐‘ข โˆ’op ๐‘ก)โ€˜๐‘ฅ) ยทih ๐‘ฅ))}
Colors of variables: wff setvar class
This definition is referenced by:  leopg  31106
  Copyright terms: Public domain W3C validator