Metamath Proof Explorer

Theorem leoppos

Description: Binary relation defining a positive operator. Definition VI.1 of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoppos ⊢T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T⁡x⋅ihx

Proof

Step Hyp Ref Expression
1 0hmop ⊢0hop∈HrmOp
2 leop ⊢0hop∈HrmOp∧T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T-op0hop⁡x⋅ihx
3 1 2 mpan ⊢T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T-op0hop⁡x⋅ihx
4 hmopf ⊢T∈HrmOp→T:ℋ⟶ℋ
5 hosubid1 ⊢T:ℋ⟶ℋ→T-op0hop=T
6 4 5 syl ⊢T∈HrmOp→T-op0hop=T
7 6 fveq1d ⊢T∈HrmOp→T-op0hop⁡x=T⁡x
8 7 oveq1d ⊢T∈HrmOp→T-op0hop⁡x⋅ihx=T⁡x⋅ihx
9 8 breq2d ⊢T∈HrmOp→0≤T-op0hop⁡x⋅ihx↔0≤T⁡x⋅ihx
10 9 ralbidv ⊢T∈HrmOp→∀x∈ℋ0≤T-op0hop⁡x⋅ihx↔∀x∈ℋ0≤T⁡x⋅ihx
11 3 10 bitrd ⊢T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T⁡x⋅ihx