Theorem leopg

Description: Ordering relation for positive operators. Definition of positive operator ordering in Kreyszig p. 470. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

	Ref	Expression
Assertion	leopg	⊢ ( ( 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐵 ) → ( 𝑇 ≤op 𝑈 ↔ ( ( 𝑈 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		oveq2	⊢ ( 𝑡 = 𝑇 → ( 𝑢 −op 𝑡 ) = ( 𝑢 −op 𝑇 ) )
2	1	eleq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ↔ ( 𝑢 −op 𝑇 ) ∈ HrmOp ) )
3	1	fveq1d	⊢ ( 𝑡 = 𝑇 → ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) = ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) )
4	3	oveq1d	⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) )
5	4	breq2d	⊢ ( 𝑡 = 𝑇 → ( 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
6	5	ralbidv	⊢ ( 𝑡 = 𝑇 → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
7	2 6	anbi12d	⊢ ( 𝑡 = 𝑇 → ( ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ↔ ( ( 𝑢 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
8		oveq1	⊢ ( 𝑢 = 𝑈 → ( 𝑢 −op 𝑇 ) = ( 𝑈 −op 𝑇 ) )
9	8	eleq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 −op 𝑇 ) ∈ HrmOp ↔ ( 𝑈 −op 𝑇 ) ∈ HrmOp ) )
10	8	fveq1d	⊢ ( 𝑢 = 𝑈 → ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) = ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) )
11	10	oveq1d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) = ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) )
12	11	breq2d	⊢ ( 𝑢 = 𝑈 → ( 0 ≤ ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
13	12	ralbidv	⊢ ( 𝑢 = 𝑈 → ( ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ↔ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) )
14	9 13	anbi12d	⊢ ( 𝑢 = 𝑈 → ( ( ( 𝑢 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ↔ ( ( 𝑈 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) )
15		df-leop	⊢ ≤op = { ⟨ 𝑡 , 𝑢 ⟩ ∣ ( ( 𝑢 −op 𝑡 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑢 −op 𝑡 ) ‘ 𝑥 ) ·ih 𝑥 ) ) }
16	7 14 15	brabg	⊢ ( ( 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐵 ) → ( 𝑇 ≤op 𝑈 ↔ ( ( 𝑈 −op 𝑇 ) ∈ HrmOp ∧ ∀ 𝑥 ∈ ℋ 0 ≤ ( ( ( 𝑈 −op 𝑇 ) ‘ 𝑥 ) ·ih 𝑥 ) ) ) )