Metamath Proof Explorer

Theorem recmulnq

Description: Relationship between reciprocal and multiplication on positive fractions. (Contributed by NM, 6-Mar-1996) (Revised by Mario Carneiro, 28-Apr-2015) (New usage is discouraged.)

Ref Expression
Assertion recmulnq 
|- ( A e. Q. -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) )

Proof

Step Hyp Ref Expression
1 fvex 
 |-  ( *Q ` A ) e. _V
2 1 a1i 
 |-  ( A e. Q. -> ( *Q ` A ) e. _V )
3 eleq1 
 |-  ( ( *Q ` A ) = B -> ( ( *Q ` A ) e. _V <-> B e. _V ) )
4 2 3 syl5ibcom 
 |-  ( A e. Q. -> ( ( *Q ` A ) = B -> B e. _V ) )
5 id 
 |-  ( ( A .Q B ) = 1Q -> ( A .Q B ) = 1Q )
6 1nq 
 |-  1Q e. Q.
7 5 6 eqeltrdi 
 |-  ( ( A .Q B ) = 1Q -> ( A .Q B ) e. Q. )
8 mulnqf 
 |-  .Q : ( Q. X. Q. ) --> Q.
9 8 fdmi 
 |-  dom .Q = ( Q. X. Q. )
10 0nnq 
 |-  -. (/) e. Q.
11 9 10 ndmovrcl 
 |-  ( ( A .Q B ) e. Q. -> ( A e. Q. /\ B e. Q. ) )
12 7 11 syl 
 |-  ( ( A .Q B ) = 1Q -> ( A e. Q. /\ B e. Q. ) )
13 elex 
 |-  ( B e. Q. -> B e. _V )
14 12 13 simpl2im 
 |-  ( ( A .Q B ) = 1Q -> B e. _V )
15 14 a1i 
 |-  ( A e. Q. -> ( ( A .Q B ) = 1Q -> B e. _V ) )
16 oveq1 
 |-  ( x = A -> ( x .Q y ) = ( A .Q y ) )
17 16 eqeq1d 
 |-  ( x = A -> ( ( x .Q y ) = 1Q <-> ( A .Q y ) = 1Q ) )
18 oveq2 
 |-  ( y = B -> ( A .Q y ) = ( A .Q B ) )
19 18 eqeq1d 
 |-  ( y = B -> ( ( A .Q y ) = 1Q <-> ( A .Q B ) = 1Q ) )
20 nqerid 
 |-  ( x e. Q. -> ( /Q ` x ) = x )
21 relxp 
 |-  Rel ( N. X. N. )
22 elpqn 
 |-  ( x e. Q. -> x e. ( N. X. N. ) )
23 1st2nd 
 |-  ( ( Rel ( N. X. N. ) /\ x e. ( N. X. N. ) ) -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
24 21 22 23 sylancr 
 |-  ( x e. Q. -> x = <. ( 1st ` x ) , ( 2nd ` x ) >. )
25 24 fveq2d 
 |-  ( x e. Q. -> ( /Q ` x ) = ( /Q ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
26 20 25 eqtr3d 
 |-  ( x e. Q. -> x = ( /Q ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) )
27 26 oveq1d 
 |-  ( x e. Q. -> ( x .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = ( ( /Q ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) )
28 mulerpq 
 |-  ( ( /Q ` <. ( 1st ` x ) , ( 2nd ` x ) >. ) .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = ( /Q ` ( <. ( 1st ` x ) , ( 2nd ` x ) >. .pQ <. ( 2nd ` x ) , ( 1st ` x ) >. ) )
29 27 28 eqtrdi 
 |-  ( x e. Q. -> ( x .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = ( /Q ` ( <. ( 1st ` x ) , ( 2nd ` x ) >. .pQ <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) )
30 xp1st 
 |-  ( x e. ( N. X. N. ) -> ( 1st ` x ) e. N. )
31 22 30 syl 
 |-  ( x e. Q. -> ( 1st ` x ) e. N. )
32 xp2nd 
 |-  ( x e. ( N. X. N. ) -> ( 2nd ` x ) e. N. )
33 22 32 syl 
 |-  ( x e. Q. -> ( 2nd ` x ) e. N. )
34 mulpipq 
 |-  ( ( ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) /\ ( ( 2nd ` x ) e. N. /\ ( 1st ` x ) e. N. ) ) -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. .pQ <. ( 2nd ` x ) , ( 1st ` x ) >. ) = <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 2nd ` x ) .N ( 1st ` x ) ) >. )
35 31 33 33 31 34 syl22anc 
 |-  ( x e. Q. -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. .pQ <. ( 2nd ` x ) , ( 1st ` x ) >. ) = <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 2nd ` x ) .N ( 1st ` x ) ) >. )
36 mulcompi 
 |-  ( ( 2nd ` x ) .N ( 1st ` x ) ) = ( ( 1st ` x ) .N ( 2nd ` x ) )
37 36 opeq2i 
 |-  <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 2nd ` x ) .N ( 1st ` x ) ) >. = <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >.
38 35 37 eqtrdi 
 |-  ( x e. Q. -> ( <. ( 1st ` x ) , ( 2nd ` x ) >. .pQ <. ( 2nd ` x ) , ( 1st ` x ) >. ) = <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. )
39 38 fveq2d 
 |-  ( x e. Q. -> ( /Q ` ( <. ( 1st ` x ) , ( 2nd ` x ) >. .pQ <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = ( /Q ` <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. ) )
40 nqerid 
 |-  ( 1Q e. Q. -> ( /Q ` 1Q ) = 1Q )
41 6 40 ax-mp 
 |-  ( /Q ` 1Q ) = 1Q
42 mulclpi 
 |-  ( ( ( 1st ` x ) e. N. /\ ( 2nd ` x ) e. N. ) -> ( ( 1st ` x ) .N ( 2nd ` x ) ) e. N. )
43 31 33 42 syl2anc 
 |-  ( x e. Q. -> ( ( 1st ` x ) .N ( 2nd ` x ) ) e. N. )
44 1nqenq 
 |-  ( ( ( 1st ` x ) .N ( 2nd ` x ) ) e. N. -> 1Q ~Q <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. )
45 43 44 syl 
 |-  ( x e. Q. -> 1Q ~Q <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. )
46 elpqn 
 |-  ( 1Q e. Q. -> 1Q e. ( N. X. N. ) )
47 6 46 ax-mp 
 |-  1Q e. ( N. X. N. )
48 43 43 opelxpd 
 |-  ( x e. Q. -> <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. e. ( N. X. N. ) )
49 nqereq 
 |-  ( ( 1Q e. ( N. X. N. ) /\ <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. e. ( N. X. N. ) ) -> ( 1Q ~Q <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. <-> ( /Q ` 1Q ) = ( /Q ` <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. ) ) )
50 47 48 49 sylancr 
 |-  ( x e. Q. -> ( 1Q ~Q <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. <-> ( /Q ` 1Q ) = ( /Q ` <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. ) ) )
51 45 50 mpbid 
 |-  ( x e. Q. -> ( /Q ` 1Q ) = ( /Q ` <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. ) )
52 41 51 syl5reqr 
 |-  ( x e. Q. -> ( /Q ` <. ( ( 1st ` x ) .N ( 2nd ` x ) ) , ( ( 1st ` x ) .N ( 2nd ` x ) ) >. ) = 1Q )
53 29 39 52 3eqtrd 
 |-  ( x e. Q. -> ( x .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = 1Q )
54 fvex 
 |-  ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) e. _V
55 oveq2 
 |-  ( y = ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) -> ( x .Q y ) = ( x .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) )
56 55 eqeq1d 
 |-  ( y = ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) -> ( ( x .Q y ) = 1Q <-> ( x .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = 1Q ) )
57 54 56 spcev 
 |-  ( ( x .Q ( /Q ` <. ( 2nd ` x ) , ( 1st ` x ) >. ) ) = 1Q -> E. y ( x .Q y ) = 1Q )
58 53 57 syl 
 |-  ( x e. Q. -> E. y ( x .Q y ) = 1Q )
59 mulcomnq 
 |-  ( r .Q s ) = ( s .Q r )
60 mulassnq 
 |-  ( ( r .Q s ) .Q t ) = ( r .Q ( s .Q t ) )
61 mulidnq 
 |-  ( r e. Q. -> ( r .Q 1Q ) = r )
62 6 9 10 59 60 61 caovmo 
 |-  E* y ( x .Q y ) = 1Q
63 df-eu 
 |-  ( E! y ( x .Q y ) = 1Q <-> ( E. y ( x .Q y ) = 1Q /\ E* y ( x .Q y ) = 1Q ) )
64 58 62 63 sylanblrc 
 |-  ( x e. Q. -> E! y ( x .Q y ) = 1Q )
65 cnvimass 
 |-  ( `' .Q " { 1Q } ) C_ dom .Q
66 df-rq 
 |-  *Q = ( `' .Q " { 1Q } )
67 9 eqcomi 
 |-  ( Q. X. Q. ) = dom .Q
68 65 66 67 3sstr4i 
 |-  *Q C_ ( Q. X. Q. )
69 relxp 
 |-  Rel ( Q. X. Q. )
70 relss 
 |-  ( *Q C_ ( Q. X. Q. ) -> ( Rel ( Q. X. Q. ) -> Rel *Q ) )
71 68 69 70 mp2 
 |-  Rel *Q
72 66 eleq2i 
 |-  ( <. x , y >. e. *Q <-> <. x , y >. e. ( `' .Q " { 1Q } ) )
73 ffn 
 |-  ( .Q : ( Q. X. Q. ) --> Q. -> .Q Fn ( Q. X. Q. ) )
74 fniniseg 
 |-  ( .Q Fn ( Q. X. Q. ) -> ( <. x , y >. e. ( `' .Q " { 1Q } ) <-> ( <. x , y >. e. ( Q. X. Q. ) /\ ( .Q ` <. x , y >. ) = 1Q ) ) )
75 8 73 74 mp2b 
 |-  ( <. x , y >. e. ( `' .Q " { 1Q } ) <-> ( <. x , y >. e. ( Q. X. Q. ) /\ ( .Q ` <. x , y >. ) = 1Q ) )
76 ancom 
 |-  ( ( <. x , y >. e. ( Q. X. Q. ) /\ ( .Q ` <. x , y >. ) = 1Q ) <-> ( ( .Q ` <. x , y >. ) = 1Q /\ <. x , y >. e. ( Q. X. Q. ) ) )
77 ancom 
 |-  ( ( x e. Q. /\ ( x .Q y ) = 1Q ) <-> ( ( x .Q y ) = 1Q /\ x e. Q. ) )
78 eleq1 
 |-  ( ( x .Q y ) = 1Q -> ( ( x .Q y ) e. Q. <-> 1Q e. Q. ) )
79 6 78 mpbiri 
 |-  ( ( x .Q y ) = 1Q -> ( x .Q y ) e. Q. )
80 9 10 ndmovrcl 
 |-  ( ( x .Q y ) e. Q. -> ( x e. Q. /\ y e. Q. ) )
81 79 80 syl 
 |-  ( ( x .Q y ) = 1Q -> ( x e. Q. /\ y e. Q. ) )
82 opelxpi 
 |-  ( ( x e. Q. /\ y e. Q. ) -> <. x , y >. e. ( Q. X. Q. ) )
83 81 82 syl 
 |-  ( ( x .Q y ) = 1Q -> <. x , y >. e. ( Q. X. Q. ) )
84 81 simpld 
 |-  ( ( x .Q y ) = 1Q -> x e. Q. )
85 83 84 2thd 
 |-  ( ( x .Q y ) = 1Q -> ( <. x , y >. e. ( Q. X. Q. ) <-> x e. Q. ) )
86 85 pm5.32i 
 |-  ( ( ( x .Q y ) = 1Q /\ <. x , y >. e. ( Q. X. Q. ) ) <-> ( ( x .Q y ) = 1Q /\ x e. Q. ) )
87 df-ov 
 |-  ( x .Q y ) = ( .Q ` <. x , y >. )
88 87 eqeq1i 
 |-  ( ( x .Q y ) = 1Q <-> ( .Q ` <. x , y >. ) = 1Q )
89 88 anbi1i 
 |-  ( ( ( x .Q y ) = 1Q /\ <. x , y >. e. ( Q. X. Q. ) ) <-> ( ( .Q ` <. x , y >. ) = 1Q /\ <. x , y >. e. ( Q. X. Q. ) ) )
90 77 86 89 3bitr2ri 
 |-  ( ( ( .Q ` <. x , y >. ) = 1Q /\ <. x , y >. e. ( Q. X. Q. ) ) <-> ( x e. Q. /\ ( x .Q y ) = 1Q ) )
91 76 90 bitri 
 |-  ( ( <. x , y >. e. ( Q. X. Q. ) /\ ( .Q ` <. x , y >. ) = 1Q ) <-> ( x e. Q. /\ ( x .Q y ) = 1Q ) )
92 72 75 91 3bitri 
 |-  ( <. x , y >. e. *Q <-> ( x e. Q. /\ ( x .Q y ) = 1Q ) )
93 92 a1i 
 |-  ( T. -> ( <. x , y >. e. *Q <-> ( x e. Q. /\ ( x .Q y ) = 1Q ) ) )
94 71 93 opabbi2dv 
 |-  ( T. -> *Q = { <. x , y >. | ( x e. Q. /\ ( x .Q y ) = 1Q ) } )
95 94 mptru 
 |-  *Q = { <. x , y >. | ( x e. Q. /\ ( x .Q y ) = 1Q ) }
96 17 19 64 95 fvopab3g 
 |-  ( ( A e. Q. /\ B e. _V ) -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) )
97 96 ex 
 |-  ( A e. Q. -> ( B e. _V -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) ) )
98 4 15 97 pm5.21ndd 
 |-  ( A e. Q. -> ( ( *Q ` A ) = B <-> ( A .Q B ) = 1Q ) )