Metamath Proof Explorer

Theorem leop

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

Ref Expression
Assertion leop ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔∀x∈ℋ0≤U-opT⁡x⋅ihx

Proof

Step Hyp Ref Expression
1 leopg ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔U-opT∈HrmOp∧∀x∈ℋ0≤U-opT⁡x⋅ihx
2 hmopd ⊢U∈HrmOp∧T∈HrmOp→U-opT∈HrmOp
3 2 ancoms ⊢T∈HrmOp∧U∈HrmOp→U-opT∈HrmOp
4 3 biantrurd ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋ0≤U-opT⁡x⋅ihx↔U-opT∈HrmOp∧∀x∈ℋ0≤U-opT⁡x⋅ihx
5 1 4 bitr4d ⊢T∈HrmOp∧U∈HrmOp→T≤opU↔∀x∈ℋ0≤U-opT⁡x⋅ihx