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 ≤ op U ∧ U ≤ op T ↔ T = U

Proof

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