Metamath Proof Explorer

Theorem leop3

Description: Operator ordering in terms of a positive operator. Definition of operator ordering in Retherford p. 49. (Contributed by NM, 23-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leop3 
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> 0hop <_op ( U -op T ) ) )

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 0hmop 
 |-  0hop e. HrmOp
3 hmopd 
 |-  ( ( U e. HrmOp /\ T e. HrmOp ) -> ( U -op T ) e. HrmOp )
4 3 ancoms 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( U -op T ) e. HrmOp )
5 leop2 
 |-  ( ( 0hop e. HrmOp /\ ( U -op T ) e. HrmOp ) -> ( 0hop <_op ( U -op T ) <-> A. x e. ~H ( ( 0hop ` x ) .ih x ) <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
6 2 4 5 sylancr 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( 0hop <_op ( U -op T ) <-> A. x e. ~H ( ( 0hop ` x ) .ih x ) <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
7 ho0val 
 |-  ( x e. ~H -> ( 0hop ` x ) = 0h )
8 7 oveq1d 
 |-  ( x e. ~H -> ( ( 0hop ` x ) .ih x ) = ( 0h .ih x ) )
9 hi01 
 |-  ( x e. ~H -> ( 0h .ih x ) = 0 )
10 8 9 eqtrd 
 |-  ( x e. ~H -> ( ( 0hop ` x ) .ih x ) = 0 )
11 10 breq1d 
 |-  ( x e. ~H -> ( ( ( 0hop ` x ) .ih x ) <_ ( ( ( U -op T ) ` x ) .ih x ) <-> 0 <_ ( ( ( U -op T ) ` x ) .ih x ) ) )
12 11 ralbiia 
 |-  ( A. x e. ~H ( ( 0hop ` x ) .ih x ) <_ ( ( ( U -op T ) ` x ) .ih x ) <-> A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) )
13 6 12 bitr2di 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H 0 <_ ( ( ( U -op T ) ` x ) .ih x ) <-> 0hop <_op ( U -op T ) ) )
14 1 13 bitrd 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> 0hop <_op ( U -op T ) ) )