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	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )

Proof

Step	Hyp	Ref	Expression
1		leopg	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ( ( 𝑈 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
2		hmopd	⊢ ( ( 𝑈 ∈ HrmOp ∧ 𝑇 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
3	2	ancoms	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑈 −op 𝑇 ) ∈ HrmOp )
4	3	biantrurd	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ( ( 𝑈 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
5	1 4	bitr4d	⊢ ( ( 𝑇 ∈ HrmOp ∧ 𝑈 ∈ HrmOp ) → ( 𝑇 ≤op 𝑈 ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )