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	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( 0hop <_op T <-> 0hop <_op ( A .op T ) ) )

Proof

Step	Hyp	Ref	Expression
1		3simpa	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( A e. RR /\ T e. HrmOp ) )
2	1	adantr	|- ( ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) /\ 0hop <_op T ) -> ( A e. RR /\ T e. HrmOp ) )
3		0re	|- 0 e. RR
4		ltle	|- ( ( 0 e. RR /\ A e. RR ) -> ( 0 < A -> 0 <_ A ) )
5	4	3impia	|- ( ( 0 e. RR /\ A e. RR /\ 0 < A ) -> 0 <_ A )
6	3 5	mp3an1	|- ( ( A e. RR /\ 0 < A ) -> 0 <_ A )
7	6	3adant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> 0 <_ A )
8	7	anim1i	|- ( ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) /\ 0hop <_op T ) -> ( 0 <_ A /\ 0hop <_op T ) )
9		leopmuli	|- ( ( ( A e. RR /\ T e. HrmOp ) /\ ( 0 <_ A /\ 0hop <_op T ) ) -> 0hop <_op ( A .op T ) )
10	2 8 9	syl2anc	|- ( ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) /\ 0hop <_op T ) -> 0hop <_op ( A .op T ) )
11		gt0ne0	|- ( ( A e. RR /\ 0 < A ) -> A =/= 0 )
12		rereccl	|- ( ( A e. RR /\ A =/= 0 ) -> ( 1 / A ) e. RR )
13	11 12	syldan	|- ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. RR )
14	13	3adant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( 1 / A ) e. RR )
15		hmopm	|- ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) e. HrmOp )
16	15	3adant3	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( A .op T ) e. HrmOp )
17		recgt0	|- ( ( A e. RR /\ 0 < A ) -> 0 < ( 1 / A ) )
18		ltle	|- ( ( 0 e. RR /\ ( 1 / A ) e. RR ) -> ( 0 < ( 1 / A ) -> 0 <_ ( 1 / A ) ) )
19	3 13 18	sylancr	|- ( ( A e. RR /\ 0 < A ) -> ( 0 < ( 1 / A ) -> 0 <_ ( 1 / A ) ) )
20	17 19	mpd	|- ( ( A e. RR /\ 0 < A ) -> 0 <_ ( 1 / A ) )
21	20	3adant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> 0 <_ ( 1 / A ) )
22	14 16 21	jca31	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( ( ( 1 / A ) e. RR /\ ( A .op T ) e. HrmOp ) /\ 0 <_ ( 1 / A ) ) )
23		leopmuli	|- ( ( ( ( 1 / A ) e. RR /\ ( A .op T ) e. HrmOp ) /\ ( 0 <_ ( 1 / A ) /\ 0hop <_op ( A .op T ) ) ) -> 0hop <_op ( ( 1 / A ) .op ( A .op T ) ) )
24	23	anassrs	|- ( ( ( ( ( 1 / A ) e. RR /\ ( A .op T ) e. HrmOp ) /\ 0 <_ ( 1 / A ) ) /\ 0hop <_op ( A .op T ) ) -> 0hop <_op ( ( 1 / A ) .op ( A .op T ) ) )
25	22 24	sylan	|- ( ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) /\ 0hop <_op ( A .op T ) ) -> 0hop <_op ( ( 1 / A ) .op ( A .op T ) ) )
26		recn	|- ( A e. RR -> A e. CC )
27	26	adantr	|- ( ( A e. RR /\ 0 < A ) -> A e. CC )
28	27 11	recid2d	|- ( ( A e. RR /\ 0 < A ) -> ( ( 1 / A ) x. A ) = 1 )
29	28	oveq1d	|- ( ( A e. RR /\ 0 < A ) -> ( ( ( 1 / A ) x. A ) .op T ) = ( 1 .op T ) )
30	29	3adant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( ( ( 1 / A ) x. A ) .op T ) = ( 1 .op T ) )
31	27 11	reccld	|- ( ( A e. RR /\ 0 < A ) -> ( 1 / A ) e. CC )
32	31	3adant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( 1 / A ) e. CC )
33	26	3ad2ant1	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> A e. CC )
34		hmopf	|- ( T e. HrmOp -> T : ~H --> ~H )
35	34	3ad2ant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> T : ~H --> ~H )
36		homulass	|- ( ( ( 1 / A ) e. CC /\ A e. CC /\ T : ~H --> ~H ) -> ( ( ( 1 / A ) x. A ) .op T ) = ( ( 1 / A ) .op ( A .op T ) ) )
37	32 33 35 36	syl3anc	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( ( ( 1 / A ) x. A ) .op T ) = ( ( 1 / A ) .op ( A .op T ) ) )
38		homullid	|- ( T : ~H --> ~H -> ( 1 .op T ) = T )
39	34 38	syl	|- ( T e. HrmOp -> ( 1 .op T ) = T )
40	39	3ad2ant2	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( 1 .op T ) = T )
41	30 37 40	3eqtr3d	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( ( 1 / A ) .op ( A .op T ) ) = T )
42	41	adantr	|- ( ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) /\ 0hop <_op ( A .op T ) ) -> ( ( 1 / A ) .op ( A .op T ) ) = T )
43	25 42	breqtrd	|- ( ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) /\ 0hop <_op ( A .op T ) ) -> 0hop <_op T )
44	10 43	impbida	|- ( ( A e. RR /\ T e. HrmOp /\ 0 < A ) -> ( 0hop <_op T <-> 0hop <_op ( A .op T ) ) )