Metamath Proof Explorer

Theorem leopmuli

Description: The scalar product of a nonnegative real and a positive operator is a positive operator. Exercise 1(ii) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leopmuli ⊢A∈ℝ∧T∈HrmOp∧0≤A∧0hop≤opT→0hop≤opA·opT

Proof

Step Hyp Ref Expression
1 hmopre ⊢T∈HrmOp∧x∈ℋ→T⁡x⋅ihx∈ℝ
2 mulge0 ⊢A∈ℝ∧0≤A∧T⁡x⋅ihx∈ℝ∧0≤T⁡x⋅ihx→0≤A⁢T⁡x⋅ihx
3 1 2 sylanr1 ⊢A∈ℝ∧0≤A∧T∈HrmOp∧x∈ℋ∧0≤T⁡x⋅ihx→0≤A⁢T⁡x⋅ihx
4 3 expr ⊢A∈ℝ∧0≤A∧T∈HrmOp∧x∈ℋ→0≤T⁡x⋅ihx→0≤A⁢T⁡x⋅ihx
5 4 an4s ⊢A∈ℝ∧T∈HrmOp∧0≤A∧x∈ℋ→0≤T⁡x⋅ihx→0≤A⁢T⁡x⋅ihx
6 5 anassrs ⊢A∈ℝ∧T∈HrmOp∧0≤A∧x∈ℋ→0≤T⁡x⋅ihx→0≤A⁢T⁡x⋅ihx
7 recn ⊢A∈ℝ→A∈ℂ
8 hmopf ⊢T∈HrmOp→T:ℋ⟶ℋ
9 7 8 anim12i ⊢A∈ℝ∧T∈HrmOp→A∈ℂ∧T:ℋ⟶ℋ
10 homval ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x=A⋅ℎT⁡x
11 10 3expa ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x=A⋅ℎT⁡x
12 11 oveq1d ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x⋅ihx=A⋅ℎT⁡x⋅ihx
13 simpll ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A∈ℂ
14 ffvelcdm ⊢T:ℋ⟶ℋ∧x∈ℋ→T⁡x∈ℋ
15 14 adantll ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→T⁡x∈ℋ
16 simpr ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→x∈ℋ
17 ax-his3 ⊢A∈ℂ∧T⁡x∈ℋ∧x∈ℋ→A⋅ℎT⁡x⋅ihx=A⁢T⁡x⋅ihx
18 13 15 16 17 syl3anc ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A⋅ℎT⁡x⋅ihx=A⁢T⁡x⋅ihx
19 12 18 eqtrd ⊢A∈ℂ∧T:ℋ⟶ℋ∧x∈ℋ→A·opT⁡x⋅ihx=A⁢T⁡x⋅ihx
20 9 19 sylan ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ→A·opT⁡x⋅ihx=A⁢T⁡x⋅ihx
21 20 breq2d ⊢A∈ℝ∧T∈HrmOp∧x∈ℋ→0≤A·opT⁡x⋅ihx↔0≤A⁢T⁡x⋅ihx
22 21 adantlr ⊢A∈ℝ∧T∈HrmOp∧0≤A∧x∈ℋ→0≤A·opT⁡x⋅ihx↔0≤A⁢T⁡x⋅ihx
23 6 22 sylibrd ⊢A∈ℝ∧T∈HrmOp∧0≤A∧x∈ℋ→0≤T⁡x⋅ihx→0≤A·opT⁡x⋅ihx
24 23 ralimdva ⊢A∈ℝ∧T∈HrmOp∧0≤A→∀x∈ℋ0≤T⁡x⋅ihx→∀x∈ℋ0≤A·opT⁡x⋅ihx
25 24 expimpd ⊢A∈ℝ∧T∈HrmOp→0≤A∧∀x∈ℋ0≤T⁡x⋅ihx→∀x∈ℋ0≤A·opT⁡x⋅ihx
26 leoppos ⊢T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T⁡x⋅ihx
27 26 adantl ⊢A∈ℝ∧T∈HrmOp→0hop≤opT↔∀x∈ℋ0≤T⁡x⋅ihx
28 27 anbi2d ⊢A∈ℝ∧T∈HrmOp→0≤A∧0hop≤opT↔0≤A∧∀x∈ℋ0≤T⁡x⋅ihx
29 hmopm ⊢A∈ℝ∧T∈HrmOp→A·opT∈HrmOp
30 leoppos ⊢A·opT∈HrmOp→0hop≤opA·opT↔∀x∈ℋ0≤A·opT⁡x⋅ihx
31 29 30 syl ⊢A∈ℝ∧T∈HrmOp→0hop≤opA·opT↔∀x∈ℋ0≤A·opT⁡x⋅ihx
32 25 28 31 3imtr4d ⊢A∈ℝ∧T∈HrmOp→0≤A∧0hop≤opT→0hop≤opA·opT
33 32 imp ⊢A∈ℝ∧T∈HrmOp∧0≤A∧0hop≤opT→0hop≤opA·opT