Metamath Proof Explorer


Theorem leop3

Description: Operator ordering in terms of a positive operator. Definition of operator ordering in Retherford p. 49. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leop3 T HrmOp U HrmOp T op U 0 hop op U - op T

Proof

Step Hyp Ref Expression
1 leop T HrmOp U HrmOp T op U x 0 U - op T x ih x
2 0hmop 0 hop HrmOp
3 hmopd U HrmOp T HrmOp U - op T HrmOp
4 3 ancoms T HrmOp U HrmOp U - op T HrmOp
5 leop2 0 hop HrmOp U - op T HrmOp 0 hop op U - op T x 0 hop x ih x U - op T x ih x
6 2 4 5 sylancr T HrmOp U HrmOp 0 hop op U - op T x 0 hop x ih x U - op T x ih x
7 ho0val x 0 hop x = 0
8 7 oveq1d x 0 hop x ih x = 0 ih x
9 hi01 x 0 ih x = 0
10 8 9 eqtrd x 0 hop x ih x = 0
11 10 breq1d x 0 hop x ih x U - op T x ih x 0 U - op T x ih x
12 11 ralbiia x 0 hop x ih x U - op T x ih x x 0 U - op T x ih x
13 6 12 bitr2di T HrmOp U HrmOp x 0 U - op T x ih x 0 hop op U - op T
14 1 13 bitrd T HrmOp U HrmOp T op U 0 hop op U - op T