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

Proof

Step	Hyp	Ref	Expression
1		0hmop	⊢ 0hop ∈ HrmOp
2		leop	⊢ ( ( 0hop ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑇 −op 0hop ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
3	1 2	mpan	⊢ ( 𝑇 ∈ HrmOp → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 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 → ( 0hop ≤op 𝑇 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( 𝑇 ‘ 𝑥 ) ·ih 𝑥 ) ) )