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≤opU↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx

Proof

Step Hyp Ref Expression
1 leop ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔∀x∈ℋ0≤U-opT⁡x⋅ihx
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-opT⁡x=U⁡x-ℎT⁡x
6 5 3com12 ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→U-opT⁡x=U⁡x-ℎT⁡x
7 6 3expa ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→U-opT⁡x=U⁡x-ℎT⁡x
8 7 oveq1d ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→U-opT⁡x⋅ihx=U⁡x-ℎT⁡x⋅ihx
9 ffvelrn ⊢U:ℋ⟶ℋ∧x∈ℋ→U⁡x∈ℋ
10 9 adantll ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→U⁡x∈ℋ
11 ffvelrn ⊢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⋅ihx=U⁡x⋅ihx−T⁡x⋅ihx
15 10 12 13 14 syl3anc ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→U⁡x-ℎT⁡x⋅ihx=U⁡x⋅ihx−T⁡x⋅ihx
16 8 15 eqtrd ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→U-opT⁡x⋅ihx=U⁡x⋅ihx−T⁡x⋅ihx
17 4 16 sylan ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→U-opT⁡x⋅ihx=U⁡x⋅ihx−T⁡x⋅ihx
18 17 breq2d ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→0≤U-opT⁡x⋅ihx↔0≤U⁡x⋅ihx−T⁡x⋅ihx
19 hmopre ⊢U∈HrmOp∧x∈ℋ→U⁡x⋅ihx∈ℝ
20 19 adantll ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→U⁡x⋅ihx∈ℝ
21 hmopre ⊢T∈HrmOp∧x∈ℋ→T⁡x⋅ihx∈ℝ
22 21 adantlr ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→T⁡x⋅ihx∈ℝ
23 20 22 subge0d ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→0≤U⁡x⋅ihx−T⁡x⋅ihx↔T⁡x⋅ihx≤U⁡x⋅ihx
24 18 23 bitrd ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→0≤U-opT⁡x⋅ihx↔T⁡x⋅ihx≤U⁡x⋅ihx
25 24 ralbidva ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋ0≤U-opT⁡x⋅ihx↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx
26 1 25 bitrd ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔∀x∈ℋT⁡x⋅ihx≤U⁡x⋅ihx