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≤opT∧T≤opU→S≤opU

Proof

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