Metamath Proof Explorer

Theorem leop2

Description: Ordering relation for operators. Definition of operator ordering in Young p. 141. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leop2 
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )

Proof

Step Hyp Ref Expression
1 leop 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
2 hmopf 
 |-  ( T e. HrmOp -> T : ~H --> ~H )
3 hmopf 
 |-  ( U e. HrmOp -> U : ~H --> ~H )
4 2 3 anim12i 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T : ~H --> ~H /\ U : ~H --> ~H ) )
5 hodval 
 |-  ( ( U : ~H --> ~H /\ T : ~H --> ~H /\ x e. ~H ) -> ( ( U -op T ) ` x ) = ( ( U ` x ) -h ( T ` x ) ) )
6 5 3com12 
 |-  ( ( T : ~H --> ~H /\ U : ~H --> ~H /\ x e. ~H ) -> ( ( U -op T ) ` x ) = ( ( U ` x ) -h ( T ` x ) ) )
7 6 3expa 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( U -op T ) ` x ) = ( ( U ` x ) -h ( T ` x ) ) )
8 7 oveq1d 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( U -op T ) ` x ) .ih x ) = ( ( ( U ` x ) -h ( T ` x ) ) .ih x ) )
9 ffvelrn 
 |-  ( ( U : ~H --> ~H /\ x e. ~H ) -> ( U ` x ) e. ~H )
10 9 adantll 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( U ` x ) e. ~H )
11 ffvelrn 
 |-  ( ( T : ~H --> ~H /\ x e. ~H ) -> ( T ` x ) e. ~H )
12 11 adantlr 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( T ` x ) e. ~H )
13 simpr 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> x e. ~H )
14 his2sub 
 |-  ( ( ( U ` x ) e. ~H /\ ( T ` x ) e. ~H /\ x e. ~H ) -> ( ( ( U ` x ) -h ( T ` x ) ) .ih x ) = ( ( ( U ` x ) .ih x ) - ( ( T ` x ) .ih x ) ) )
15 10 12 13 14 syl3anc 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( U ` x ) -h ( T ` x ) ) .ih x ) = ( ( ( U ` x ) .ih x ) - ( ( T ` x ) .ih x ) ) )
16 8 15 eqtrd 
 |-  ( ( ( T : ~H --> ~H /\ U : ~H --> ~H ) /\ x e. ~H ) -> ( ( ( U -op T ) ` x ) .ih x ) = ( ( ( U ` x ) .ih x ) - ( ( T ` x ) .ih x ) ) )
17 4 16 sylan 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( ( U -op T ) ` x ) .ih x ) = ( ( ( U ` x ) .ih x ) - ( ( T ` x ) .ih x ) ) )
18 17 breq2d 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( 0 <_ ( ( ( U -op T ) ` x ) .ih x ) <-> 0 <_ ( ( ( U ` x ) .ih x ) - ( ( T ` x ) .ih x ) ) ) )
19 hmopre 
 |-  ( ( U e. HrmOp /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. RR )
20 19 adantll 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. RR )
21 hmopre 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
22 21 adantlr 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
23 20 22 subge0d 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( 0 <_ ( ( ( U ` x ) .ih x ) - ( ( T ` x ) .ih x ) ) <-> ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
24 18 23 bitrd 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( 0 <_ ( ( ( U -op T ) ` x ) .ih x ) <-> ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
25 24 ralbidva 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
26 1 25 bitrd 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )