Metamath Proof Explorer

Theorem leopmul2i

Description: Scalar product applied to operator ordering. (Contributed by NM, 12-Aug-2006) (New usage is discouraged.)

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

Proof

Step Hyp Ref Expression
1 simp1 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> A e. RR )
2 hmopd 
 |-  ( ( U e. HrmOp /\ T e. HrmOp ) -> ( U -op T ) e. HrmOp )
3 2 ancoms 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( U -op T ) e. HrmOp )
4 3 3adant1 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( U -op T ) e. HrmOp )
5 leopmuli 
 |-  ( ( ( A e. RR /\ ( U -op T ) e. HrmOp ) /\ ( 0 <_ A /\ 0hop <_op ( U -op T ) ) ) -> 0hop <_op ( A .op ( U -op T ) ) )
6 5 exp32 
 |-  ( ( A e. RR /\ ( U -op T ) e. HrmOp ) -> ( 0 <_ A -> ( 0hop <_op ( U -op T ) -> 0hop <_op ( A .op ( U -op T ) ) ) ) )
7 1 4 6 syl2anc 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( 0 <_ A -> ( 0hop <_op ( U -op T ) -> 0hop <_op ( A .op ( U -op T ) ) ) ) )
8 7 imp 
 |-  ( ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) /\ 0 <_ A ) -> ( 0hop <_op ( U -op T ) -> 0hop <_op ( A .op ( U -op T ) ) ) )
9 leop3 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> 0hop <_op ( U -op T ) ) )
10 9 3adant1 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> 0hop <_op ( U -op T ) ) )
11 10 adantr 
 |-  ( ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) /\ 0 <_ A ) -> ( T <_op U <-> 0hop <_op ( U -op T ) ) )
12 hmopm 
 |-  ( ( A e. RR /\ T e. HrmOp ) -> ( A .op T ) e. HrmOp )
13 hmopm 
 |-  ( ( A e. RR /\ U e. HrmOp ) -> ( A .op U ) e. HrmOp )
14 leop3 
 |-  ( ( ( A .op T ) e. HrmOp /\ ( A .op U ) e. HrmOp ) -> ( ( A .op T ) <_op ( A .op U ) <-> 0hop <_op ( ( A .op U ) -op ( A .op T ) ) ) )
15 12 13 14 syl2an 
 |-  ( ( ( A e. RR /\ T e. HrmOp ) /\ ( A e. RR /\ U e. HrmOp ) ) -> ( ( A .op T ) <_op ( A .op U ) <-> 0hop <_op ( ( A .op U ) -op ( A .op T ) ) ) )
16 15 3impdi 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( ( A .op T ) <_op ( A .op U ) <-> 0hop <_op ( ( A .op U ) -op ( A .op T ) ) ) )
17 recn 
 |-  ( A e. RR -> A e. CC )
18 hmopf 
 |-  ( U e. HrmOp -> U : ~H --> ~H )
19 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
20 hosubdi 
 |-  ( ( A e. CC /\ U : ~H --> ~H /\ T : ~H --> ~H ) -> ( A .op ( U -op T ) ) = ( ( A .op U ) -op ( A .op T ) ) )
21 17 18 19 20 syl3an 
 |-  ( ( A e. RR /\ U e. HrmOp /\ T e. HrmOp ) -> ( A .op ( U -op T ) ) = ( ( A .op U ) -op ( A .op T ) ) )
22 21 3com23 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( A .op ( U -op T ) ) = ( ( A .op U ) -op ( A .op T ) ) )
23 22 breq2d 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( 0hop <_op ( A .op ( U -op T ) ) <-> 0hop <_op ( ( A .op U ) -op ( A .op T ) ) ) )
24 16 23 bitr4d 
 |-  ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) -> ( ( A .op T ) <_op ( A .op U ) <-> 0hop <_op ( A .op ( U -op T ) ) ) )
25 24 adantr 
 |-  ( ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) /\ 0 <_ A ) -> ( ( A .op T ) <_op ( A .op U ) <-> 0hop <_op ( A .op ( U -op T ) ) ) )
26 8 11 25 3imtr4d 
 |-  ( ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) /\ 0 <_ A ) -> ( T <_op U -> ( A .op T ) <_op ( A .op U ) ) )
27 26 impr 
 |-  ( ( ( A e. RR /\ T e. HrmOp /\ U e. HrmOp ) /\ ( 0 <_ A /\ T <_op U ) ) -> ( A .op T ) <_op ( A .op U ) )