Metamath Proof Explorer

Theorem leopadd

Description: The sum of two positive operators is positive. Exercise 1(i) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leopadd ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ 0 hop ≤ op T ∧ 0 hop ≤ op U → 0 hop ≤ op T + op U

Proof

Step Hyp Ref Expression
1 r19.26 ⊢ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x ↔ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x ∧ ∀ x ∈ ℋ 0 ≤ U ⁡ x ⋅ ih x
2 hmopre ⊢ T ∈ HrmOp ∧ x ∈ ℋ → T ⁡ x ⋅ ih x ∈ ℝ
3 hmopre ⊢ U ∈ HrmOp ∧ x ∈ ℋ → U ⁡ x ⋅ ih x ∈ ℝ
4 addge0 ⊢ T ⁡ x ⋅ ih x ∈ ℝ ∧ U ⁡ x ⋅ ih x ∈ ℝ ∧ 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x → 0 ≤ T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
5 4 ex ⊢ T ⁡ x ⋅ ih x ∈ ℝ ∧ U ⁡ x ⋅ ih x ∈ ℝ → 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x → 0 ≤ T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
6 2 3 5 syl2an ⊢ T ∈ HrmOp ∧ x ∈ ℋ ∧ U ∈ HrmOp ∧ x ∈ ℋ → 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x → 0 ≤ T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
7 6 anandirs ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ → 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x → 0 ≤ T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
8 hmopf ⊢ T ∈ HrmOp → T : ℋ ⟶ ℋ
9 hmopf ⊢ U ∈ HrmOp → U : ℋ ⟶ ℋ
10 8 9 anim12i ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ
11 hosval ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x = T ⁡ x + ℎ U ⁡ x
12 11 oveq1d ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x ⋅ ih x = T ⁡ x + ℎ U ⁡ x ⋅ ih x
13 12 3expa ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x ⋅ ih x = T ⁡ x + ℎ U ⁡ x ⋅ ih x
14 ffvelcdm ⊢ T : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
15 14 adantlr ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x ∈ ℋ
16 ffvelcdm ⊢ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → U ⁡ x ∈ ℋ
17 16 adantll ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → U ⁡ x ∈ ℋ
18 simpr ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → x ∈ ℋ
19 ax-his2 ⊢ T ⁡ x ∈ ℋ ∧ U ⁡ x ∈ ℋ ∧ x ∈ ℋ → T ⁡ x + ℎ U ⁡ x ⋅ ih x = T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
20 15 17 18 19 syl3anc ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T ⁡ x + ℎ U ⁡ x ⋅ ih x = T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
21 13 20 eqtrd ⊢ T : ℋ ⟶ ℋ ∧ U : ℋ ⟶ ℋ ∧ x ∈ ℋ → T + op U ⁡ x ⋅ ih x = T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
22 10 21 sylan ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ → T + op U ⁡ x ⋅ ih x = T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
23 22 breq2d ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ → 0 ≤ T + op U ⁡ x ⋅ ih x ↔ 0 ≤ T ⁡ x ⋅ ih x + U ⁡ x ⋅ ih x
24 7 23 sylibrd ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ x ∈ ℋ → 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x → 0 ≤ T + op U ⁡ x ⋅ ih x
25 24 ralimdva ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x ∧ 0 ≤ U ⁡ x ⋅ ih x → ∀ x ∈ ℋ 0 ≤ T + op U ⁡ x ⋅ ih x
26 1 25 biimtrrid ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x ∧ ∀ x ∈ ℋ 0 ≤ U ⁡ x ⋅ ih x → ∀ x ∈ ℋ 0 ≤ T + op U ⁡ x ⋅ ih x
27 leoppos ⊢ T ∈ HrmOp → 0 hop ≤ op T ↔ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x
28 leoppos ⊢ U ∈ HrmOp → 0 hop ≤ op U ↔ ∀ x ∈ ℋ 0 ≤ U ⁡ x ⋅ ih x
29 27 28 bi2anan9 ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → 0 hop ≤ op T ∧ 0 hop ≤ op U ↔ ∀ x ∈ ℋ 0 ≤ T ⁡ x ⋅ ih x ∧ ∀ x ∈ ℋ 0 ≤ U ⁡ x ⋅ ih x
30 hmops ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → T + op U ∈ HrmOp
31 leoppos ⊢ T + op U ∈ HrmOp → 0 hop ≤ op T + op U ↔ ∀ x ∈ ℋ 0 ≤ T + op U ⁡ x ⋅ ih x
32 30 31 syl ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → 0 hop ≤ op T + op U ↔ ∀ x ∈ ℋ 0 ≤ T + op U ⁡ x ⋅ ih x
33 26 29 32 3imtr4d ⊢ T ∈ HrmOp ∧ U ∈ HrmOp → 0 hop ≤ op T ∧ 0 hop ≤ op U → 0 hop ≤ op T + op U
34 33 imp ⊢ T ∈ HrmOp ∧ U ∈ HrmOp ∧ 0 hop ≤ op T ∧ 0 hop ≤ op U → 0 hop ≤ op T + op U