Metamath Proof Explorer

Theorem leoppos

Description: Binary relation defining a positive operator. Definition VI.1 of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoppos ⊢ T ∈ HrmOp → 0 hop ≤ op T ↔ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x

Proof

Step Hyp Ref Expression
1 0hmop ⊢ 0 hop ∈ HrmOp
2 leop ⊢ 0 hop ∈ HrmOp ∧ T ∈ HrmOp → 0 hop ≤ op T ↔ ∀ x ∈ ℋ 0 ≤ T - op 0 hop ⁡ x ⋅ ih x
3 1 2 mpan ⊢ T ∈ HrmOp → 0 hop ≤ op T ↔ ∀ x ∈ ℋ 0 ≤ T - op 0 hop ⁡ x ⋅ ih x
4 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
5 hosubid1 ⊢ T : ℋ ⟶ ℋ → T - op 0 hop = T
6 4 5 syl ⊢ T ∈ HrmOp → T - op 0 hop = T
7 6 fveq1d ⊢ T ∈ HrmOp → T - op 0 hop ⁡ x = T ⁡ x
8 7 oveq1d ⊢ T ∈ HrmOp → T - op 0 hop ⁡ x ⋅ ih x = T ⁡ x ⋅ ih x
9 8 breq2d ⊢ T ∈ HrmOp → 0 ≤ T - op 0 hop ⁡ x ⋅ ih x ↔ 0 ≤ T ⁡ x ⋅ ih x
10 9 ralbidv ⊢ T ∈ HrmOp → ∀ x ∈ ℋ 0 ≤ T - op 0 hop ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x
11 3 10 bitrd ⊢ T ∈ HrmOp → 0 hop ≤ op T ↔ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x