Metamath Proof Explorer

Theorem leoptri

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

Ref Expression
Assertion leoptri ⊢T∈HrmOp∧U∈HrmOp→T≤opU∧U≤opT↔T=U

Proof

Step Hyp Ref Expression
1 leop2 ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx
2 leop2 ⊢U∈HrmOp∧T∈HrmOp→U≤opT↔∀x∈ℋU⁡x⋅ihx≤T⁡x⋅ihx
3 2 ancoms ⊢T∈HrmOp∧U∈HrmOp→U≤opT↔∀x∈ℋU⁡x⋅ihx≤T⁡x⋅ihx
4 1 3 anbi12d ⊢T∈HrmOp∧U∈HrmOp→T≤opU∧U≤opT↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx∧∀x∈ℋU⁡x⋅ihx≤T⁡x⋅ihx
5 hmopre ⊢T∈HrmOp∧x∈ℋ→T⁡x⋅ihx∈ℝ
6 5 adantlr ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→T⁡x⋅ihx∈ℝ
7 hmopre ⊢U∈HrmOp∧x∈ℋ→U⁡x⋅ihx∈ℝ
8 7 adantll ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→U⁡x⋅ihx∈ℝ
9 6 8 letri3d ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→T⁡x⋅ihx=U⁡x⋅ihx↔T⁡x⋅ihx≤U⁡x⋅ihx∧U⁡x⋅ihx≤T⁡x⋅ihx
10 9 ralbidva ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx∧U⁡x⋅ihx≤T⁡x⋅ihx
11 r19.26 ⊢∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx∧U⁡x⋅ihx≤T⁡x⋅ihx↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx∧∀x∈ℋU⁡x⋅ihx≤T⁡x⋅ihx
12 10 11 bitr2di ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx∧∀x∈ℋU⁡x⋅ihx≤T⁡x⋅ihx↔∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx
13 hmoplin ⊢T∈HrmOp→T∈LinOp
14 hmoplin ⊢U∈HrmOp→U∈LinOp
15 lnopeq ⊢T∈LinOp∧U∈LinOp→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔T=U
16 13 14 15 syl2an ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋT⁡x⋅ihx=U⁡x⋅ihx↔T=U
17 4 12 16 3bitrd ⊢T∈HrmOp∧U∈HrmOp→T≤opU∧U≤opT↔T=U