Metamath Proof Explorer

Theorem leop3

Description: Operator ordering in terms of a positive operator. Definition of operator ordering in Retherford p. 49. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leop3 ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔0hop≤opU-opT

Proof

Step Hyp Ref Expression
1 leop ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔∀x∈ℋ0≤U-opT⁡x⋅ihx
2 0hmop ⊢0hop∈HrmOp
3 hmopd ⊢U∈HrmOp∧T∈HrmOp→U-opT∈HrmOp
4 3 ancoms ⊢T∈HrmOp∧U∈HrmOp→U-opT∈HrmOp
5 leop2 ⊢0hop∈HrmOp∧U-opT∈HrmOp→0hop≤opU-opT↔∀x∈ℋ0hop⁡x⋅ihx≤U-opT⁡x⋅ihx
6 2 4 5 sylancr ⊢T∈HrmOp∧U∈HrmOp→0hop≤opU-opT↔∀x∈ℋ0hop⁡x⋅ihx≤U-opT⁡x⋅ihx
7 ho0val ⊢x∈ℋ→0hop⁡x=0ℎ
8 7 oveq1d ⊢x∈ℋ→0hop⁡x⋅ihx=0ℎ⋅ihx
9 hi01 ⊢x∈ℋ→0ℎ⋅ihx=0
10 8 9 eqtrd ⊢x∈ℋ→0hop⁡x⋅ihx=0
11 10 breq1d ⊢x∈ℋ→0hop⁡x⋅ihx≤U-opT⁡x⋅ihx↔0≤U-opT⁡x⋅ihx
12 11 ralbiia ⊢∀x∈ℋ0hop⁡x⋅ihx≤U-opT⁡x⋅ihx↔∀x∈ℋ0≤U-opT⁡x⋅ihx
13 6 12 bitr2di ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋ0≤U-opT⁡x⋅ihx↔0hop≤opU-opT
14 1 13 bitrd ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔0hop≤opU-opT