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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 3simpa | |
|
2 | 1 | adantr | |
3 | 0re | |
|
4 | ltle | |
|
5 | 4 | 3impia | |
6 | 3 5 | mp3an1 | |
7 | 6 | 3adant2 | |
8 | 7 | anim1i | |
9 | leopmuli | |
|
10 | 2 8 9 | syl2anc | |
11 | gt0ne0 | |
|
12 | rereccl | |
|
13 | 11 12 | syldan | |
14 | 13 | 3adant2 | |
15 | hmopm | |
|
16 | 15 | 3adant3 | |
17 | recgt0 | |
|
18 | ltle | |
|
19 | 3 13 18 | sylancr | |
20 | 17 19 | mpd | |
21 | 20 | 3adant2 | |
22 | 14 16 21 | jca31 | |
23 | leopmuli | |
|
24 | 23 | anassrs | |
25 | 22 24 | sylan | |
26 | recn | |
|
27 | 26 | adantr | |
28 | 27 11 | recid2d | |
29 | 28 | oveq1d | |
30 | 29 | 3adant2 | |
31 | 27 11 | reccld | |
32 | 31 | 3adant2 | |
33 | 26 | 3ad2ant1 | |
34 | hmopf | |
|
35 | 34 | 3ad2ant2 | |
36 | homulass | |
|
37 | 32 33 35 36 | syl3anc | |
38 | homulid2 | |
|
39 | 34 38 | syl | |
40 | 39 | 3ad2ant2 | |
41 | 30 37 40 | 3eqtr3d | |
42 | 41 | adantr | |
43 | 25 42 | breqtrd | |
44 | 10 43 | impbida | |