Metamath Proof Explorer

Theorem leoptr

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

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

Proof

Step Hyp Ref Expression
1 r19.26 
 |-  ( A. x e. ~H ( ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) <-> ( A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
2 hmopre 
 |-  ( ( S e. HrmOp /\ x e. ~H ) -> ( ( S ` x ) .ih x ) e. RR )
3 hmopre 
 |-  ( ( T e. HrmOp /\ x e. ~H ) -> ( ( T ` x ) .ih x ) e. RR )
4 hmopre 
 |-  ( ( U e. HrmOp /\ x e. ~H ) -> ( ( U ` x ) .ih x ) e. RR )
5 letr 
 |-  ( ( ( ( S ` x ) .ih x ) e. RR /\ ( ( T ` x ) .ih x ) e. RR /\ ( ( U ` x ) .ih x ) e. RR ) -> ( ( ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) -> ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
6 2 3 4 5 syl3an 
 |-  ( ( ( S e. HrmOp /\ x e. ~H ) /\ ( T e. HrmOp /\ x e. ~H ) /\ ( U e. HrmOp /\ x e. ~H ) ) -> ( ( ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) -> ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
7 6 3anandirs 
 |-  ( ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) /\ x e. ~H ) -> ( ( ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) -> ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
8 7 ralimdva 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( A. x e. ~H ( ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) -> A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
9 1 8 syl5bir 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( ( A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) -> A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
10 leop2 
 |-  ( ( S e. HrmOp /\ T e. HrmOp ) -> ( S <_op T <-> A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) )
11 10 3adant3 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( S <_op T <-> A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) ) )
12 leop2 
 |-  ( ( T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
13 12 3adant1 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( T <_op U <-> A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
14 11 13 anbi12d 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( ( S <_op T /\ T <_op U ) <-> ( A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( T ` x ) .ih x ) /\ A. x e. ~H ( ( T ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) ) )
15 leop2 
 |-  ( ( S e. HrmOp /\ U e. HrmOp ) -> ( S <_op U <-> A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
16 15 3adant2 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( S <_op U <-> A. x e. ~H ( ( S ` x ) .ih x ) <_ ( ( U ` x ) .ih x ) ) )
17 9 14 16 3imtr4d 
 |-  ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) -> ( ( S <_op T /\ T <_op U ) -> S <_op U ) )
18 17 imp 
 |-  ( ( ( S e. HrmOp /\ T e. HrmOp /\ U e. HrmOp ) /\ ( S <_op T /\ T <_op U ) ) -> S <_op U )