Hilbert Space Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  HSE Home  >  Th. List  >  leopmul Unicode version

Theorem leopmul 23625
 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.)
Assertion
Ref Expression
leopmul

Proof of Theorem leopmul
StepHypRef Expression
1 3simpa 954 . . . 4
3 0re 9080 . . . . . 6
4 ltle 9152 . . . . . . 7
543impia 1150 . . . . . 6
63, 5mp3an1 1266 . . . . 5
763adant2 976 . . . 4
87anim1i 552 . . 3
9 leopmuli 23624 . . 3
102, 8, 9syl2anc 643 . 2
11 gt0ne0 9482 . . . . . . 7
12 rereccl 9721 . . . . . . 7
1311, 12syldan 457 . . . . . 6
14133adant2 976 . . . . 5
15 hmopm 23512 . . . . . 6
16153adant3 977 . . . . 5
17 recgt0 9843 . . . . . . 7
18 ltle 9152 . . . . . . . 8
193, 13, 18sylancr 645 . . . . . . 7
2017, 19mpd 15 . . . . . 6
21203adant2 976 . . . . 5
2214, 16, 21jca31 521 . . . 4
23 leopmuli 23624 . . . . 5
2423anassrs 630 . . . 4
2522, 24sylan 458 . . 3
26 recn 9069 . . . . . . . . 9
2726adantr 452 . . . . . . . 8
2827, 11recid2d 9775 . . . . . . 7
2928oveq1d 6087 . . . . . 6
30293adant2 976 . . . . 5
3127, 11reccld 9772 . . . . . . 7
32313adant2 976 . . . . . 6
33263ad2ant1 978 . . . . . 6
34 hmopf 23365 . . . . . . 7
35343ad2ant2 979 . . . . . 6
36 homulass 23293 . . . . . 6
3732, 33, 35, 36syl3anc 1184 . . . . 5
38 homulid2 23291 . . . . . . 7
3934, 38syl 16 . . . . . 6
40393ad2ant2 979 . . . . 5
4130, 37, 403eqtr3d 2475 . . . 4