Metamath Proof Explorer

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 ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T ≤ op U ↔ ∀ x ∈ ℋ T ⁡ x ⋅ ih x ≤ U ⁡ x ⋅ ih x

Proof

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