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 ∧ 0 hop ≤ op T → 0 hop ≤ op A · op T

Proof

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