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∧0hop≤opT∧0hop≤opU→0hop≤opT+opU

Proof

Step Hyp Ref Expression
1 r19.26 ⊢∀x∈ℋ0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx↔∀x∈ℋ0≤T⁡x⋅ihx∧∀x∈ℋ0≤U⁡x⋅ihx
2 hmopre ⊢T∈HrmOp∧x∈ℋ→T⁡x⋅ihx∈ℝ
3 hmopre ⊢U∈HrmOp∧x∈ℋ→U⁡x⋅ihx∈ℝ
4 addge0 ⊢T⁡x⋅ihx∈ℝ∧U⁡x⋅ihx∈ℝ∧0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx→0≤T⁡x⋅ihx+U⁡x⋅ihx
5 4 ex ⊢T⁡x⋅ihx∈ℝ∧U⁡x⋅ihx∈ℝ→0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx→0≤T⁡x⋅ihx+U⁡x⋅ihx
6 2 3 5 syl2an ⊢T∈HrmOp∧x∈ℋ∧U∈HrmOp∧x∈ℋ→0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx→0≤T⁡x⋅ihx+U⁡x⋅ihx
7 6 anandirs ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx→0≤T⁡x⋅ihx+U⁡x⋅ihx
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+opU⁡x=T⁡x+ℎU⁡x
12 11 oveq1d ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→T+opU⁡x⋅ihx=T⁡x+ℎU⁡x⋅ihx
13 12 3expa ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→T+opU⁡x⋅ihx=T⁡x+ℎU⁡x⋅ihx
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⋅ihx=T⁡x⋅ihx+U⁡x⋅ihx
20 15 17 18 19 syl3anc ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→T⁡x+ℎU⁡x⋅ihx=T⁡x⋅ihx+U⁡x⋅ihx
21 13 20 eqtrd ⊢T:ℋ⟶ℋ∧U:ℋ⟶ℋ∧x∈ℋ→T+opU⁡x⋅ihx=T⁡x⋅ihx+U⁡x⋅ihx
22 10 21 sylan ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→T+opU⁡x⋅ihx=T⁡x⋅ihx+U⁡x⋅ihx
23 22 breq2d ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→0≤T+opU⁡x⋅ihx↔0≤T⁡x⋅ihx+U⁡x⋅ihx
24 7 23 sylibrd ⊢T∈HrmOp∧U∈HrmOp∧x∈ℋ→0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx→0≤T+opU⁡x⋅ihx
25 24 ralimdva ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋ0≤T⁡x⋅ihx∧0≤U⁡x⋅ihx→∀x∈ℋ0≤T+opU⁡x⋅ihx
26 1 25 biimtrrid ⊢T∈HrmOp∧U∈HrmOp→∀x∈ℋ0≤T⁡x⋅ihx∧∀x∈ℋ0≤U⁡x⋅ihx→∀x∈ℋ0≤T+opU⁡x⋅ihx
27 leoppos ⊢T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T⁡x⋅ihx
28 leoppos ⊢U∈HrmOp→0hop≤opU↔∀x∈ℋ0≤U⁡x⋅ihx
29 27 28 bi2anan9 ⊢T∈HrmOp∧U∈HrmOp→0hop≤opT∧0hop≤opU↔∀x∈ℋ0≤T⁡x⋅ihx∧∀x∈ℋ0≤U⁡x⋅ihx
30 hmops ⊢T∈HrmOp∧U∈HrmOp→T+opU∈HrmOp
31 leoppos ⊢T+opU∈HrmOp→0hop≤opT+opU↔∀x∈ℋ0≤T+opU⁡x⋅ihx
32 30 31 syl ⊢T∈HrmOp∧U∈HrmOp→0hop≤opT+opU↔∀x∈ℋ0≤T+opU⁡x⋅ihx
33 26 29 32 3imtr4d ⊢T∈HrmOp∧U∈HrmOp→0hop≤opT∧0hop≤opU→0hop≤opT+opU
34 33 imp ⊢T∈HrmOp∧U∈HrmOp∧0hop≤opT∧0hop≤opU→0hop≤opT+opU