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 ATHrmOp0<A0hopopT0hopopA·opT

Proof

Step Hyp Ref Expression
1 3simpa ATHrmOp0<AATHrmOp
2 1 adantr ATHrmOp0<A0hopopTATHrmOp
3 0re 0
4 ltle 0A0<A0A
5 4 3impia 0A0<A0A
6 3 5 mp3an1 A0<A0A
7 6 3adant2 ATHrmOp0<A0A
8 7 anim1i ATHrmOp0<A0hopopT0A0hopopT
9 leopmuli ATHrmOp0A0hopopT0hopopA·opT
10 2 8 9 syl2anc ATHrmOp0<A0hopopT0hopopA·opT
11 gt0ne0 A0<AA0
12 rereccl AA01A
13 11 12 syldan A0<A1A
14 13 3adant2 ATHrmOp0<A1A
15 hmopm ATHrmOpA·opTHrmOp
16 15 3adant3 ATHrmOp0<AA·opTHrmOp
17 recgt0 A0<A0<1A
18 ltle 01A0<1A01A
19 3 13 18 sylancr A0<A0<1A01A
20 17 19 mpd A0<A01A
21 20 3adant2 ATHrmOp0<A01A
22 14 16 21 jca31 ATHrmOp0<A1AA·opTHrmOp01A
23 leopmuli 1AA·opTHrmOp01A0hopopA·opT0hopop1A·opA·opT
24 23 anassrs 1AA·opTHrmOp01A0hopopA·opT0hopop1A·opA·opT
25 22 24 sylan ATHrmOp0<A0hopopA·opT0hopop1A·opA·opT
26 recn AA
27 26 adantr A0<AA
28 27 11 recid2d A0<A1AA=1
29 28 oveq1d A0<A1AA·opT=1·opT
30 29 3adant2 ATHrmOp0<A1AA·opT=1·opT
31 27 11 reccld A0<A1A
32 31 3adant2 ATHrmOp0<A1A
33 26 3ad2ant1 ATHrmOp0<AA
34 hmopf THrmOpT:
35 34 3ad2ant2 ATHrmOp0<AT:
36 homulass 1AAT:1AA·opT=1A·opA·opT
37 32 33 35 36 syl3anc ATHrmOp0<A1AA·opT=1A·opA·opT
38 homulid2 T:1·opT=T
39 34 38 syl THrmOp1·opT=T
40 39 3ad2ant2 ATHrmOp0<A1·opT=T
41 30 37 40 3eqtr3d ATHrmOp0<A1A·opA·opT=T
42 41 adantr ATHrmOp0<A0hopopA·opT1A·opA·opT=T
43 25 42 breqtrd ATHrmOp0<A0hopopA·opT0hopopT
44 10 43 impbida ATHrmOp0<A0hopopT0hopopA·opT