# Metamath Proof Explorer

## Theorem leopmul

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

Ref Expression
Assertion leopmul ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left({0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}↔{0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)$

### Proof

Step Hyp Ref Expression
1 3simpa ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)$
2 1 adantr ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}\right)\to \left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)$
3 0re ${⊢}0\in ℝ$
4 ltle ${⊢}\left(0\in ℝ\wedge {A}\in ℝ\right)\to \left(0<{A}\to 0\le {A}\right)$
5 4 3impia ${⊢}\left(0\in ℝ\wedge {A}\in ℝ\wedge 0<{A}\right)\to 0\le {A}$
6 3 5 mp3an1 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0\le {A}$
7 6 3adant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to 0\le {A}$
8 7 anim1i ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}\right)\to \left(0\le {A}\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}\right)$
9 leopmuli ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\wedge \left(0\le {A}\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}\right)\right)\to {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
10 2 8 9 syl2anc ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}\right)\to {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
11 gt0ne0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\ne 0$
12 rereccl ${⊢}\left({A}\in ℝ\wedge {A}\ne 0\right)\to \frac{1}{{A}}\in ℝ$
13 11 12 syldan ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \frac{1}{{A}}\in ℝ$
14 13 3adant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \frac{1}{{A}}\in ℝ$
15 hmopm ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\right)\to {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}$
16 15 3adant3 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}$
17 recgt0 ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0<\frac{1}{{A}}$
18 ltle ${⊢}\left(0\in ℝ\wedge \frac{1}{{A}}\in ℝ\right)\to \left(0<\frac{1}{{A}}\to 0\le \frac{1}{{A}}\right)$
19 3 13 18 sylancr ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(0<\frac{1}{{A}}\to 0\le \frac{1}{{A}}\right)$
20 17 19 mpd ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to 0\le \frac{1}{{A}}$
21 20 3adant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to 0\le \frac{1}{{A}}$
22 14 16 21 jca31 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left(\left(\frac{1}{{A}}\in ℝ\wedge {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}\right)\wedge 0\le \frac{1}{{A}}\right)$
23 leopmuli ${⊢}\left(\left(\frac{1}{{A}}\in ℝ\wedge {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}\right)\wedge \left(0\le \frac{1}{{A}}\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)\right)\to {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)$
24 23 anassrs ${⊢}\left(\left(\left(\frac{1}{{A}}\in ℝ\wedge {A}{·}_{\mathrm{op}}{T}\in \mathrm{HrmOp}\right)\wedge 0\le \frac{1}{{A}}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)\to {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)$
25 22 24 sylan ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)\to {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left(\left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)$
26 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
27 26 adantr ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to {A}\in ℂ$
28 27 11 recid2d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\frac{1}{{A}}\right){A}=1$
29 28 oveq1d ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \left(\frac{1}{{A}}\right){A}{·}_{\mathrm{op}}{T}=1{·}_{\mathrm{op}}{T}$
30 29 3adant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left(\frac{1}{{A}}\right){A}{·}_{\mathrm{op}}{T}=1{·}_{\mathrm{op}}{T}$
31 27 11 reccld ${⊢}\left({A}\in ℝ\wedge 0<{A}\right)\to \frac{1}{{A}}\in ℂ$
32 31 3adant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \frac{1}{{A}}\in ℂ$
33 26 3ad2ant1 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to {A}\in ℂ$
34 hmopf ${⊢}{T}\in \mathrm{HrmOp}\to {T}:ℋ⟶ℋ$
35 34 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to {T}:ℋ⟶ℋ$
36 homulass ${⊢}\left(\frac{1}{{A}}\in ℂ\wedge {A}\in ℂ\wedge {T}:ℋ⟶ℋ\right)\to \left(\frac{1}{{A}}\right){A}{·}_{\mathrm{op}}{T}=\left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
37 32 33 35 36 syl3anc ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left(\frac{1}{{A}}\right){A}{·}_{\mathrm{op}}{T}=\left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)$
38 homulid2 ${⊢}{T}:ℋ⟶ℋ\to 1{·}_{\mathrm{op}}{T}={T}$
39 34 38 syl ${⊢}{T}\in \mathrm{HrmOp}\to 1{·}_{\mathrm{op}}{T}={T}$
40 39 3ad2ant2 ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to 1{·}_{\mathrm{op}}{T}={T}$
41 30 37 40 3eqtr3d ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)={T}$
42 41 adantr ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)\to \left(\frac{1}{{A}}\right){·}_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)={T}$
43 25 42 breqtrd ${⊢}\left(\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\wedge {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)\to {0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}$
44 10 43 impbida ${⊢}\left({A}\in ℝ\wedge {T}\in \mathrm{HrmOp}\wedge 0<{A}\right)\to \left({0}_{\mathrm{hop}}{\le }_{\mathrm{op}}{T}↔{0}_{\mathrm{hop}}{\le }_{\mathrm{op}}\left({A}{·}_{\mathrm{op}}{T}\right)\right)$