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 )