Metamath Proof Explorer

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 ⊢ T ∈ A ∧ U ∈ B → T ≤ op U ↔ U - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ t = T → u - op t = u - op T
2 1 eleq1d ⊢ t = T → u - op t ∈ HrmOp ↔ u - op T ∈ HrmOp
3 1 fveq1d ⊢ t = T → u - op t ⁡ x = u - op T ⁡ x
4 3 oveq1d ⊢ t = T → u - op t ⁡ x ⋅ ih x = u - op T ⁡ x ⋅ ih x
5 4 breq2d ⊢ t = T → 0 ≤ u - op t ⁡ x ⋅ ih x ↔ 0 ≤ u - op T ⁡ x ⋅ ih x
6 5 ralbidv ⊢ t = T → ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ 0 ≤ u - op T ⁡ x ⋅ ih x
7 2 6 anbi12d ⊢ t = T → u - op t ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x ↔ u - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op T ⁡ x ⋅ ih x
8 oveq1 ⊢ u = U → u - op T = U - op T
9 8 eleq1d ⊢ u = U → u - op T ∈ HrmOp ↔ U - op T ∈ HrmOp
10 8 fveq1d ⊢ u = U → u - op T ⁡ x = U - op T ⁡ x
11 10 oveq1d ⊢ u = U → u - op T ⁡ x ⋅ ih x = U - op T ⁡ x ⋅ ih x
12 11 breq2d ⊢ u = U → 0 ≤ u - op T ⁡ x ⋅ ih x ↔ 0 ≤ U - op T ⁡ x ⋅ ih x
13 12 ralbidv ⊢ u = U → ∀ x ∈ ℋ 0 ≤ u - op T ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x
14 9 13 anbi12d ⊢ u = U → u - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op T ⁡ x ⋅ ih x ↔ U - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x
15 df-leop ⊢ ≤ op = t u | u - op t ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ u - op t ⁡ x ⋅ ih x
16 7 14 15 brabg ⊢ T ∈ A ∧ U ∈ B → T ≤ op U ↔ U - op T ∈ HrmOp ∧ ∀ x ∈ ℋ 0 ≤ U - op T ⁡ x ⋅ ih x