Metamath Proof Explorer


Theorem lterpq

Description: Compatibility of ordering on equivalent fractions. (Contributed by Mario Carneiro, 9-May-2013) (New usage is discouraged.)

Ref Expression
Assertion lterpq
|- ( A  ( /Q ` A ) 

Proof

Step Hyp Ref Expression
1 df-ltpq
 |-  . | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) 
2 opabssxp
 |-  { <. x , y >. | ( ( x e. ( N. X. N. ) /\ y e. ( N. X. N. ) ) /\ ( ( 1st ` x ) .N ( 2nd ` y ) ) 
3 1 2 eqsstri
 |-  
4 3 brel
 |-  ( A  ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) )
5 ltrelnq
 |-  
6 5 brel
 |-  ( ( /Q ` A )  ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) )
7 elpqn
 |-  ( ( /Q ` A ) e. Q. -> ( /Q ` A ) e. ( N. X. N. ) )
8 elpqn
 |-  ( ( /Q ` B ) e. Q. -> ( /Q ` B ) e. ( N. X. N. ) )
9 nqerf
 |-  /Q : ( N. X. N. ) --> Q.
10 9 fdmi
 |-  dom /Q = ( N. X. N. )
11 0nelxp
 |-  -. (/) e. ( N. X. N. )
12 10 11 ndmfvrcl
 |-  ( ( /Q ` A ) e. ( N. X. N. ) -> A e. ( N. X. N. ) )
13 10 11 ndmfvrcl
 |-  ( ( /Q ` B ) e. ( N. X. N. ) -> B e. ( N. X. N. ) )
14 12 13 anim12i
 |-  ( ( ( /Q ` A ) e. ( N. X. N. ) /\ ( /Q ` B ) e. ( N. X. N. ) ) -> ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) )
15 7 8 14 syl2an
 |-  ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) )
16 6 15 syl
 |-  ( ( /Q ` A )  ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) )
17 xp1st
 |-  ( A e. ( N. X. N. ) -> ( 1st ` A ) e. N. )
18 xp2nd
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` B ) e. N. )
19 mulclpi
 |-  ( ( ( 1st ` A ) e. N. /\ ( 2nd ` B ) e. N. ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
20 17 18 19 syl2an
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. )
21 ltmpi
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) e. N. -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) )  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) 
22 20 21 syl
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) )  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) 
23 nqercl
 |-  ( A e. ( N. X. N. ) -> ( /Q ` A ) e. Q. )
24 nqercl
 |-  ( B e. ( N. X. N. ) -> ( /Q ` B ) e. Q. )
25 ordpinq
 |-  ( ( ( /Q ` A ) e. Q. /\ ( /Q ` B ) e. Q. ) -> ( ( /Q ` A )  ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) 
26 23 24 25 syl2an
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( /Q ` A )  ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) 
27 1st2nd2
 |-  ( A e. ( N. X. N. ) -> A = <. ( 1st ` A ) , ( 2nd ` A ) >. )
28 1st2nd2
 |-  ( B e. ( N. X. N. ) -> B = <. ( 1st ` B ) , ( 2nd ` B ) >. )
29 27 28 breqan12d
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A  <. ( 1st ` A ) , ( 2nd ` A ) >. . ) )
30 ordpipq
 |-  ( <. ( 1st ` A ) , ( 2nd ` A ) >. . <-> ( ( 1st ` A ) .N ( 2nd ` B ) ) 
31 29 30 bitrdi
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A  ( ( 1st ` A ) .N ( 2nd ` B ) ) 
32 xp1st
 |-  ( ( /Q ` A ) e. ( N. X. N. ) -> ( 1st ` ( /Q ` A ) ) e. N. )
33 23 7 32 3syl
 |-  ( A e. ( N. X. N. ) -> ( 1st ` ( /Q ` A ) ) e. N. )
34 xp2nd
 |-  ( ( /Q ` B ) e. ( N. X. N. ) -> ( 2nd ` ( /Q ` B ) ) e. N. )
35 24 8 34 3syl
 |-  ( B e. ( N. X. N. ) -> ( 2nd ` ( /Q ` B ) ) e. N. )
36 mulclpi
 |-  ( ( ( 1st ` ( /Q ` A ) ) e. N. /\ ( 2nd ` ( /Q ` B ) ) e. N. ) -> ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) e. N. )
37 33 35 36 syl2an
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) e. N. )
38 ltmpi
 |-  ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) e. N. -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) 
39 37 38 syl
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` A ) .N ( 2nd ` B ) )  ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) 
40 mulcompi
 |-  ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) )
41 40 a1i
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) )
42 nqerrel
 |-  ( A e. ( N. X. N. ) -> A ~Q ( /Q ` A ) )
43 23 7 syl
 |-  ( A e. ( N. X. N. ) -> ( /Q ` A ) e. ( N. X. N. ) )
44 enqbreq2
 |-  ( ( A e. ( N. X. N. ) /\ ( /Q ` A ) e. ( N. X. N. ) ) -> ( A ~Q ( /Q ` A ) <-> ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) = ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) ) )
45 43 44 mpdan
 |-  ( A e. ( N. X. N. ) -> ( A ~Q ( /Q ` A ) <-> ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) = ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) ) )
46 42 45 mpbid
 |-  ( A e. ( N. X. N. ) -> ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) = ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) )
47 46 eqcomd
 |-  ( A e. ( N. X. N. ) -> ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) = ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) )
48 nqerrel
 |-  ( B e. ( N. X. N. ) -> B ~Q ( /Q ` B ) )
49 24 8 syl
 |-  ( B e. ( N. X. N. ) -> ( /Q ` B ) e. ( N. X. N. ) )
50 enqbreq2
 |-  ( ( B e. ( N. X. N. ) /\ ( /Q ` B ) e. ( N. X. N. ) ) -> ( B ~Q ( /Q ` B ) <-> ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) = ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) )
51 49 50 mpdan
 |-  ( B e. ( N. X. N. ) -> ( B ~Q ( /Q ` B ) <-> ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) = ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) )
52 48 51 mpbid
 |-  ( B e. ( N. X. N. ) -> ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) = ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) )
53 47 52 oveqan12d
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) ) )
54 mulcompi
 |-  ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) )
55 fvex
 |-  ( 1st ` B ) e. _V
56 fvex
 |-  ( 2nd ` A ) e. _V
57 fvex
 |-  ( 1st ` ( /Q ` A ) ) e. _V
58 mulcompi
 |-  ( x .N y ) = ( y .N x )
59 mulasspi
 |-  ( ( x .N y ) .N z ) = ( x .N ( y .N z ) )
60 fvex
 |-  ( 2nd ` ( /Q ` B ) ) e. _V
61 55 56 57 58 59 60 caov411
 |-  ( ( ( 1st ` B ) .N ( 2nd ` A ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) = ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) )
62 54 61 eqtri
 |-  ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` A ) ) .N ( ( 1st ` B ) .N ( 2nd ` ( /Q ` B ) ) ) )
63 mulcompi
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) ) = ( ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) )
64 fvex
 |-  ( 1st ` ( /Q ` B ) ) e. _V
65 fvex
 |-  ( 2nd ` ( /Q ` A ) ) e. _V
66 fvex
 |-  ( 1st ` A ) e. _V
67 fvex
 |-  ( 2nd ` B ) e. _V
68 64 65 66 58 59 67 caov411
 |-  ( ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) )
69 63 68 eqtri
 |-  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` ( /Q ` A ) ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` B ) ) )
70 53 62 69 3eqtr4g
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` B ) .N ( 2nd ` A ) ) ) = ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` B ) ) .N ( 2nd ` ( /Q ` A ) ) ) ) )
71 41 70 breq12d
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( ( ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) .N ( ( 1st ` A ) .N ( 2nd ` B ) ) )  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) 
72 31 39 71 3bitrd
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A  ( ( ( 1st ` A ) .N ( 2nd ` B ) ) .N ( ( 1st ` ( /Q ` A ) ) .N ( 2nd ` ( /Q ` B ) ) ) ) 
73 22 26 72 3bitr4rd
 |-  ( ( A e. ( N. X. N. ) /\ B e. ( N. X. N. ) ) -> ( A  ( /Q ` A ) 
74 4 16 73 pm5.21nii
 |-  ( A  ( /Q ` A )