Metamath Proof Explorer

Theorem leoptr

Description: The positive operator ordering relation is transitive. Exercise 1(iv) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoptr ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp ∧ S ≤ op T ∧ T ≤ op U → S ≤ op U

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
2 hmopre ⊢ S ∈ HrmOp ∧ x ∈ ℋ → S ⁡ x ⋅ ih x ∈ ℝ
3 hmopre ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℝ
4 hmopre ⊢ U ∈ HrmOp ∧ x ∈ ℋ → U ⁡ x ⋅ ih x ∈ ℝ
5 letr ⊢ S ⁡ x ⋅ ih x ∈ ℝ ∧ T ⁡ x ⋅ ih x ∈ ℝ ∧ U ⁡ x ⋅ ih x ∈ ℝ → S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x → S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
6 2 3 4 5 syl3an ⊢ S ∈ HrmOp ∧ x ∈ ℋ ∧ T ∈ HrmOp ∧ x ∈ ℋ ∧ U ∈ HrmOp ∧ x ∈ ℋ → S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x → S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
7 6 3anandirs ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ → S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x → S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
8 7 ralimdva ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x → ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
9 1 8 biimtrrid ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x → ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
10 leop2 ⊢ S ∈ HrmOp ∧ T ∈ HrmOp → S ≤ op T ↔ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x
11 10 3adant3 ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → S ≤ op T ↔ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x
12 leop2 ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T ≤ op U ↔ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
13 12 3adant1 ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → T ≤ op U ↔ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
14 11 13 anbi12d ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → S ≤ op T ∧ T ≤ op U ↔ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ T ⁡ x ⋅ ih x ∧ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
15 leop2 ⊢ S ∈ HrmOp ∧ U ∈ HrmOp → S ≤ op U ↔ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
16 15 3adant2 ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → S ≤ op U ↔ ∀ x ∈ ℋ S ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x
17 9 14 16 3imtr4d ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp → S ≤ op T ∧ T ≤ op U → S ≤ op U
18 17 imp ⊢ S ∈ HrmOp ∧ T ∈ HrmOp ∧ U ∈ HrmOp ∧ S ≤ op T ∧ T ≤ op U → S ≤ op U