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 ( ( ( 𝐴 ∈ ℝ ∧ 𝑇 ∈ HrmOp ) ∧ ( 0 ≤ 𝐴 ∧ 0hop ≤op 𝑇 ) ) → 0hop ≤op ( 𝐴 ·op 𝑇 ) )

Proof

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