Metamath Proof Explorer

Theorem leoptri

Description: The positive operator ordering relation satisfies trichotomy. Exercise 1(iii) of Retherford p. 49. (Contributed by NM, 25-Jul-2006) (New usage is discouraged.)

Ref Expression
Assertion leoptri 
|- ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( T <_op U /\ U <_op T ) <-> T = U ) )

Proof

Step Hyp Ref Expression
1 leop2 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
2 leop2 
 |-  ( ( U e. HrmOp /\ T e. HrmOp ) -> ( U <_op T <-> A. x e. ~H ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) )
3 2 ancoms 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( U <_op T <-> A. x e. ~H ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) )
4 1 3 anbi12d 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( T <_op U /\ U <_op T ) <-> ( A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) /\ A. x e. ~H ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) ) )
5 hmopre 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
6 5 adantlr 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
7 hmopre 
 |-  ( ( U e. HrmOp /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. RR )
8 7 adantll 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. RR )
9 6 8 letri3d 
 |-  ( ( ( T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> ( ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) /\ ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) ) )
10 9 ralbidva 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> A. x e. ~H ( ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) /\ ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) ) )
11 r19.26 
 |-  ( A. x e. ~H ( ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) /\ ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) <-> ( A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) /\ A. x e. ~H ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) )
12 10 11 bitr2di 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) /\ A. x e. ~H ( ( U ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) <-> A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) ) )
13 hmoplin 
 |-  ( T e. HrmOp -> T e. LinOp )
14 hmoplin 
 |-  ( U e. HrmOp -> U e. LinOp )
15 lnopeq 
 |-  ( ( T e. LinOp /\ U e. LinOp ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U ) )
16 13 14 15 syl2an 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H ( ( T ` x ) .ih x ) = ( ( U ` x ) .ih x ) <-> T = U ) )
17 4 12 16 3bitrd 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( ( T <_op U /\ U <_op T ) <-> T = U ) )