Metamath Proof Explorer

Theorem leopmuli

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

Ref Expression
Assertion leopmuli 
|- ( ( ( A e. RR /\ T e. HrmOp ) /\ ( 0 <_ A /\ 0hop <_op T ) ) -> 0hop <_op ( A .op T ) )

Proof

Step Hyp Ref Expression
1 hmopre 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
2 mulge0 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( ( T ` x ) .ih x ) e. RR /\ 0 <_ ( ( T ` x ) .ih x ) ) ) -> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) )
3 1 2 sylanr1 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( ( T e. HrmOp /\ x e. ~H ) /\ 0 <_ ( ( T ` x ) .ih x ) ) ) -> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) )
4 3 expr 
 |-  ( ( ( A e. RR /\ 0 <_ A ) /\ ( T e. HrmOp /\ x e. ~H ) ) -> ( 0 <_ ( ( T ` x ) .ih x ) -> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) ) )
5 4 an4s 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( 0 <_ A /\ x e. ~H ) ) -> ( 0 <_ ( ( T ` x ) .ih x ) -> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) ) )
6 5 anassrs 
 |-  ( ( ( ( A e. RR /\ T e. HrmOp ) /\ 0 <_ A ) /\ x e. ~H ) -> ( 0 <_ ( ( T ` x ) .ih x ) -> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) ) )
7 recn 
 |-  ( A e. RR -> A e. CC )
8 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
9 7 8 anim12i 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( A e. CC /\ T : ~H --> ~H ) )
10 homval 
 |-  ( ( A e. CC /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
11 10 3expa 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .op T ) ` x ) = ( A .h ( T ` x ) ) )
12 11 oveq1d 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) ` x ) .ih x ) = ( ( A .h ( T ` x ) ) .ih x ) )
13 simpll 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> A e. CC )
14 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
15 14 adantll 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( T ` x ) e. ~H )
16 simpr 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> x e. ~H )
17 ax-his3 
 |-  ( ( A e. CC /\ ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( A .h ( T ` x ) ) .ih x ) = ( A x. ( ( T ` x ) .ih x ) ) )
18 13 15 16 17 syl3anc 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( A .h ( T ` x ) ) .ih x ) = ( A x. ( ( T ` x ) .ih x ) ) )
19 12 18 eqtrd 
 |-  ( ( ( A e. CC /\ T : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( A .op T ) ` x ) .ih x ) = ( A x. ( ( T ` x ) .ih x ) ) )
20 9 19 sylan 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ x e. ~H ) -> ( ( ( A .op T ) ` x ) .ih x ) = ( A x. ( ( T ` x ) .ih x ) ) )
21 20 breq2d 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ x e. ~H ) -> ( 0 <_ ( ( ( A .op T ) ` x ) .ih x ) <-> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) ) )
22 21 adantlr 
 |-  ( ( ( ( A e. RR /\ T e. HrmOp ) /\ 0 <_ A ) /\ x e. ~H ) -> ( 0 <_ ( ( ( A .op T ) ` x ) .ih x ) <-> 0 <_ ( A x. ( ( T ` x ) .ih x ) ) ) )
23 6 22 sylibrd 
 |-  ( ( ( ( A e. RR /\ T e. HrmOp ) /\ 0 <_ A ) /\ x e. ~H ) -> ( 0 <_ ( ( T ` x ) .ih x ) -> 0 <_ ( ( ( A .op T ) ` x ) .ih x ) ) )
24 23 ralimdva 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ 0 <_ A ) -> ( A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) -> A. x e. ~H 0 <_ ( ( ( A .op T ) ` x ) .ih x ) ) )
25 24 expimpd 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( ( 0 <_ A /\ A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) -> A. x e. ~H 0 <_ ( ( ( A .op T ) ` x ) .ih x ) ) )
26 leoppos 
 |-  ( T e. HrmOp -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )
27 26 adantl 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( 0hop <_op T <-> A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) )
28 27 anbi2d 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( ( 0 <_ A /\ 0hop <_op T ) <-> ( 0 <_ A /\ A. x e. ~H 0 <_ ( ( T ` x ) .ih x ) ) ) )
29 hmopm 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) e. HrmOp )
30 leoppos 
 |-  ( ( A .op T ) e. HrmOp -> ( 0hop <_op ( A .op T ) <-> A. x e. ~H 0 <_ ( ( ( A .op T ) ` x ) .ih x ) ) )
31 29 30 syl 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( 0hop <_op ( A .op T ) <-> A. x e. ~H 0 <_ ( ( ( A .op T ) ` x ) .ih x ) ) )
32 25 28 31 3imtr4d 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( ( 0 <_ A /\ 0hop <_op T ) -> 0hop <_op ( A .op T ) ) )
33 32 imp 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( 0 <_ A /\ 0hop <_op T ) ) -> 0hop <_op ( A .op T ) )