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	⊢ ( ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈 ) ) → 𝑆 ≤op 𝑈 )

Proof

Step	Hyp	Ref	Expression
1		r19.26	⊢ ( ∀ 𝑥 ∈ ℋ ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ↔ ( ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
2		hmopre	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
3		hmopre	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
4		hmopre	⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
5		letr	⊢ ( ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ∧ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ∧ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ ) → ( ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
6	2 3 4 5	syl3an	⊢ ( ( ( 𝑆 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) ∧ ( 𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) ) → ( ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
7	6	3anandirs	⊢ ( ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
8	7	ralimdva	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ∀ 𝑥 ∈ ℋ ( ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
9	1 8	syl5bir	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) → ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
10		leop2	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 𝑆 ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
11	10	3adant3	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑆 ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
12		leop2	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
13	12	3adant1	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
14	11 13	anbi12d	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( 𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈 ) ↔ ( ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∧ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
15		leop2	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑆 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
16	15	3adant2	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑆 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑆 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
17	9 14 16	3imtr4d	⊢ ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ( 𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈 ) → 𝑆 ≤op 𝑈 ) )
18	17	imp	⊢ ( ( ( 𝑆 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ ( 𝑆 ≤op 𝑇 ∧ 𝑇 ≤op 𝑈 ) ) → 𝑆 ≤op 𝑈 )