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 ( 𝑇 ∈ HrmOp → ( 0hopop 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇𝑥 ) ·ih 𝑥 ) ) )

Proof

Step Hyp Ref Expression
1 0hmop 0hop ∈ HrmOp
2 leop ( ( 0hop ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 0hopop 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
3 1 2 mpan ( 𝑇 ∈ HrmOp → ( 0hopop 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
4 hmopf ( 𝑇 ∈ HrmOp → 𝑇 : ℋ ⟶ ℋ )
5 hosubid1 ( 𝑇 : ℋ ⟶ ℋ → ( 𝑇op 0hop ) = 𝑇 )
6 4 5 syl ( 𝑇 ∈ HrmOp → ( 𝑇op 0hop ) = 𝑇 )
7 6 fveq1d ( 𝑇 ∈ HrmOp → ( ( 𝑇op 0hop ) ‘ 𝑥 ) = ( 𝑇𝑥 ) )
8 7 oveq1d ( 𝑇 ∈ HrmOp → ( ( ( 𝑇op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( 𝑇𝑥 ) ·ih 𝑥 ) )
9 8 breq2d ( 𝑇 ∈ HrmOp → ( 0 ≤ ( ( ( 𝑇op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( 𝑇𝑥 ) ·ih 𝑥 ) ) )
10 9 ralbidv ( 𝑇 ∈ HrmOp → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇𝑥 ) ·ih 𝑥 ) ) )
11 3 10 bitrd ( 𝑇 ∈ HrmOp → ( 0hopop 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇𝑥 ) ·ih 𝑥 ) ) )