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