Definition df-leop 9718

Description: Define positive operator ordering. Definition VI.1 of [Retherford] p. 49. Note that ( ℋ × 0_ℋ) ≤_op T means that T is a positive operator.

Assertion

Ref	Expression
df-leop	⊢ ≤op = {⟨t, u⟩∣((u −op t) ∈ HrmOp ⋀ ∀x ∈ ℋ 0 ≤ (((u −op t) ‘x) ·ih x))}

Distinct variable group:   u,t,x

Detailed syntax breakdown of Definition df-leop

Step	Hyp	Ref	Expression
1		cleo 8766	. 2 class ≤op
2		vu	. . . . . . 7 set u
3	2	cv 953	. . . . . 6 class u
4		vt	. . . . . . 7 set t
5	4	cv 953	. . . . . 6 class t
6		chod 8748	. . . . . 6 class −op
7	3, 5, 6	co 3954	. . . . 5 class (u −op t)
8		cho 8758	. . . . 5 class HrmOp
9	7, 8	wcel 956	. . . 4 wff (u −op t) ∈ HrmOp
10		cc0 5214	. . . . . 6 class 0
11		vx	. . . . . . . . 9 set x
12	11	cv 953	. . . . . . . 8 class x
13	12, 7	cfv 3177	. . . . . . 7 class ((u −op t) ‘x)
14		csp 8732	. . . . . . 7 class ·ih
15	13, 12, 14	co 3954	. . . . . 6 class (((u −op t) ‘x) ·ih x)
16		cle 5275	. . . . . 6 class ≤
17	10, 15, 16	wbr 2614	. . . . 5 wff 0 ≤ (((u −op t) ‘x) ·ih x)
18		chil 8727	. . . . 5 class ℋ
19	17, 11, 18	wral 1642	. . . 4 wff ∀x ∈ ℋ 0 ≤ (((u −op t) ‘x) ·ih x)
20	9, 19	wa 223	. . 3 wff ((u −op t) ∈ HrmOp ⋀ ∀x ∈ ℋ 0 ≤ (((u −op t) ‘x) ·ih x))
21	20, 4, 2	copab 2661	. 2 class {⟨t, u⟩∣((u −op t) ∈ HrmOp ⋀ ∀x ∈ ℋ 0 ≤ (((u −op t) ‘x) ·ih x))}
22	1, 21	wceq 954	1 wff ≤op = {⟨t, u⟩∣((u −op t) ∈ HrmOp ⋀ ∀x ∈ ℋ 0 ≤ (((u −op t) ‘x) ·ih x))}

This definition is referenced by:  leopg 9993

Copyright terms: Public domain