Metamath Proof Explorer

Theorem leop

Description: Ordering relation for operators. Definition of positive operator ordering in Kreyszig p. 470. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leop ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T ≤ op U ↔ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x

Proof

Step Hyp Ref Expression
1 leopg ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T ≤ op U ↔ U - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x
2 hmopd ⊢ U ∈ HrmOp ∧ T ∈ HrmOp → U - op T ∈ HrmOp
3 2 ancoms ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → U - op T ∈ HrmOp
4 3 biantrurd ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x ↔ U - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x
5 1 4 bitr4d ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T ≤ op U ↔ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x