Definition df-leop

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.)

	Ref	Expression
Assertion	df-leop	$$⊢{\le }_{\mathrm{op}}=\left\{⟨t,u⟩|\left(u{-}_{\mathrm{op}}t\in \mathrm{HrmOp}\wedge \forall x\in \mathscr{H}0\le \left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cleo	$$class{\le }_{\mathrm{op}}$$
1		vt	$$setvart$$
2		vu	$$setvaru$$
3	2	cv	$$setvaru$$
4		chod	$$class{-}_{\mathrm{op}}$$
5	1	cv	$$setvart$$
6	3 5 4	co	$$class\left(u{-}_{\mathrm{op}}t\right)$$
7		cho	$$class\mathrm{HrmOp}$$
8	6 7	wcel	$$wffu{-}_{\mathrm{op}}t\in \mathrm{HrmOp}$$
9		vx	$$setvarx$$
10		chba	$$class\mathscr{H}$$
11		cc0	$$class0$$
12		cle	$$class\le$$
13	9	cv	$$setvarx$$
14	13 6	cfv	$$class\left(u{-}_{\mathrm{op}}t\right)\left(x\right)$$
15		csp	$$class{\cdot }_{\mathrm{ih}}$$
16	14 13 15	co	$$class\left(\left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
17	11 16 12	wbr	$$wff0\le \left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
18	17 9 10	wral	$$wff\forall x\in \mathscr{H}0\le \left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x$$
19	8 18	wa	$$wff\left(u{-}_{\mathrm{op}}t\in \mathrm{HrmOp}\wedge \forall x\in \mathscr{H}0\le \left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)$$
20	19 1 2	copab	$$class\left\{⟨t,u⟩|\left(u{-}_{\mathrm{op}}t\in \mathrm{HrmOp}\wedge \forall x\in \mathscr{H}0\le \left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)\right\}$$
21	0 20	wceq	$$wff{\le }_{\mathrm{op}}=\left\{⟨t,u⟩|\left(u{-}_{\mathrm{op}}t\in \mathrm{HrmOp}\wedge \forall x\in \mathscr{H}0\le \left(u{-}_{\mathrm{op}}t\right)\left(x\right){\cdot }_{\mathrm{ih}}x\right)\right\}$$