Theorem leop2

Description: Ordering relation for operators. Definition of operator ordering in Young p. 141. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	leop2	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		leop	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
2		hmopf	⊢ ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
3		hmopf	⊢ ( 𝑈 ∈ HrmOp → 𝑈 : ℋ ⟶ ℋ )
4	2 3	anim12i	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) )
5		hodval	⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
6	5	3com12	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
7	6	3expa	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑈 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) )
8	7	oveq1d	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑈 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑥 ) )
9		ffvelrn	⊢ ( ( 𝑈 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑈 ‘ 𝑥 ) ∈ ℋ )
10	9	adantll	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑈 ‘ 𝑥 ) ∈ ℋ )
11		ffvelrn	⊢ ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
12	11	adantlr	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( 𝑇 ‘ 𝑥 ) ∈ ℋ )
13		simpr	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → 𝑥 ∈ ℋ )
14		his2sub	⊢ ( ( ( 𝑈 ‘ 𝑥 ) ∈ ℋ ∧ ( 𝑇 ‘ 𝑥 ) ∈ ℋ ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑈 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
15	10 12 13 14	syl3anc	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑈 ‘ 𝑥 ) −ℎ ( 𝑇 ‘ 𝑥 ) ) ·ih 𝑥 ) = ( ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
16	8 15	eqtrd	⊢ ( ( ( 𝑇 : ℋ ⟶ ℋ ∧ 𝑈 : ℋ ⟶ ℋ ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
17	4 16	sylan	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )
18	17	breq2d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
19		hmopre	⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
20	19	adantll	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
21		hmopre	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
22	21	adantlr	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ∈ ℝ )
23	20 22	subge0d	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( 0 ≤ ( ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) − ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
24	18 23	bitrd	⊢ ( ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) ∧ 𝑥 ∈ ℋ ) → ( 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
25	24	ralbidva	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )
26	1 25	bitrd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( 𝑈 ‘ 𝑥 ) ·ih 𝑥 ) ) )