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	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ 0hop ≤op ( 𝑈 −op 𝑇 ) ) )

Proof

Step	Hyp	Ref	Expression
1		leop	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
2		0hmop	⊢ 0hop ∈ HrmOp
3		hmopd	⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
4	3	ancoms	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
5		leop2	⊢ ( ( 0hop ∈ HrmOp ∧ ( 𝑈 −op 𝑇 ) ∈ HrmOp ) → ( 0hop ≤op ( 𝑈 −op 𝑇 ) ↔ ∀ 𝑥 ∈ ℋ ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
6	2 4 5	sylancr	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 0hop ≤op ( 𝑈 −op 𝑇 ) ↔ ∀ 𝑥 ∈ ℋ ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
7		ho0val	⊢ ( 𝑥 ∈ ℋ → ( 0hop ‘ 𝑥 ) = 0ℎ )
8	7	oveq1d	⊢ ( 𝑥 ∈ ℋ → ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) = ( 0ℎ ·ih 𝑥 ) )
9		hi01	⊢ ( 𝑥 ∈ ℋ → ( 0ℎ ·ih 𝑥 ) = 0 )
10	8 9	eqtrd	⊢ ( 𝑥 ∈ ℋ → ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) = 0 )
11	10	breq1d	⊢ ( 𝑥 ∈ ℋ → ( ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
12	11	ralbiia	⊢ ( ∀ 𝑥 ∈ ℋ ( ( 0hop ‘ 𝑥 ) ·ih 𝑥 ) ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) )
13	6 12	bitr2di	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0hop ≤op ( 𝑈 −op 𝑇 ) ) )
14	1 13	bitrd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ 0hop ≤op ( 𝑈 −op 𝑇 ) ) )