Definition df-leop 31092

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

Step	Hyp	Ref	Expression
1		cleo 30198	. 2 class ≤op
2		vu	. . . . . . 7 setvar 𝑢
3	2	cv 1540	. . . . . 6 class 𝑢
4		vt	. . . . . . 7 setvar 𝑡
5	4	cv 1540	. . . . . 6 class 𝑡
6		chod 30180	. . . . . 6 class −op
7	3, 5, 6	co 7405	. . . . 5 class (𝑢 −op 𝑡)
8		cho 30190	. . . . 5 class HrmOp
9	7, 8	wcel 2106	. . . 4 wff (𝑢 −op 𝑡) ∈ HrmOp
10		cc0 11106	. . . . . 6 class 0
11		vx	. . . . . . . . 9 setvar 𝑥
12	11	cv 1540	. . . . . . . 8 class 𝑥
13	12, 7	cfv 6540	. . . . . . 7 class ((𝑢 −op 𝑡)‘𝑥)
14		csp 30162	. . . . . . 7 class ·ih
15	13, 12, 14	co 7405	. . . . . 6 class (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥)
16		cle 11245	. . . . . 6 class ≤
17	10, 15, 16	wbr 5147	. . . . 5 wff 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥)
18		chba 30159	. . . . 5 class ℋ
19	17, 11, 18	wral 3061	. . . 4 wff ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥)
20	9, 19	wa 396	. . 3 wff ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))
21	20, 4, 2	copab 5209	. 2 class {⟨𝑡, 𝑢⟩ ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))}
22	1, 21	wceq 1541	1 wff ≤op = {⟨𝑡, 𝑢⟩ ∣ ((𝑢 −op 𝑡) ∈ HrmOp ∧ ∀𝑥 ∈ ℋ 0 ≤ (((𝑢 −op 𝑡)‘𝑥) ·ih 𝑥))}

This definition is referenced by:  leopg  31362