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

Proof

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