Metamath Proof Explorer

Theorem zringfrac

Description: The field of fractions of the ring of integers is isomorphic to the field of the rational numbers. (Contributed by Thierry Arnoux, 4-May-2025)

Ref Expression
Hypotheses zringfrac.1 
|- Q = ( CCfld |`s QQ )
zringfrac.2 
|- .~ = ( ZZring ~RL ( ZZ \ { 0 } ) )
zringfrac.3 
|- F = ( q e. QQ |-> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
Assertion zringfrac 
|- F e. ( Q RingIso ( Frac ` ZZring ) )

Proof

Step Hyp Ref Expression
1 zringfrac.1 
 |-  Q = ( CCfld |`s QQ )
2 zringfrac.2 
 |-  .~ = ( ZZring ~RL ( ZZ \ { 0 } ) )
3 zringfrac.3 
 |-  F = ( q e. QQ |-> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
4 1 qdrng 
 |-  Q e. DivRing
5 drngring 
 |-  ( Q e. DivRing -> Q e. Ring )
6 4 5 ax-mp 
 |-  Q e. Ring
7 zringidom 
 |-  ZZring e. IDomn
8 id 
 |-  ( ZZring e. IDomn -> ZZring e. IDomn )
9 8 fracfld 
 |-  ( ZZring e. IDomn -> ( Frac ` ZZring ) e. Field )
10 9 fldcrngd 
 |-  ( ZZring e. IDomn -> ( Frac ` ZZring ) e. CRing )
11 10 crngringd 
 |-  ( ZZring e. IDomn -> ( Frac ` ZZring ) e. Ring )
12 7 11 ax-mp 
 |-  ( Frac ` ZZring ) e. Ring
13 6 12 pm3.2i 
 |-  ( Q e. Ring /\ ( Frac ` ZZring ) e. Ring )
14 ringgrp 
 |-  ( Q e. Ring -> Q e. Grp )
15 6 14 ax-mp 
 |-  Q e. Grp
16 ringgrp 
 |-  ( ( Frac ` ZZring ) e. Ring -> ( Frac ` ZZring ) e. Grp )
17 12 16 ax-mp 
 |-  ( Frac ` ZZring ) e. Grp
18 15 17 pm3.2i 
 |-  ( Q e. Grp /\ ( Frac ` ZZring ) e. Grp )
19 qnumcl 
 |-  ( q e. QQ -> ( numer ` q ) e. ZZ )
20 qdencl 
 |-  ( q e. QQ -> ( denom ` q ) e. NN )
21 20 nnzd 
 |-  ( q e. QQ -> ( denom ` q ) e. ZZ )
22 20 nnne0d 
 |-  ( q e. QQ -> ( denom ` q ) =/= 0 )
23 21 22 eldifsnd 
 |-  ( q e. QQ -> ( denom ` q ) e. ( ZZ \ { 0 } ) )
24 19 23 opelxpd 
 |-  ( q e. QQ -> <. ( numer ` q ) , ( denom ` q ) >. e. ( ZZ X. ( ZZ \ { 0 } ) ) )
25 2 ovexi 
 |-  .~ e. _V
26 25 ecelqsi 
 |-  ( <. ( numer ` q ) , ( denom ` q ) >. e. ( ZZ X. ( ZZ \ { 0 } ) ) -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) )
27 24 26 syl 
 |-  ( q e. QQ -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) )
28 zringbas 
 |-  ZZ = ( Base ` ZZring )
29 zring0 
 |-  0 = ( 0g ` ZZring )
30 zringmulr 
 |-  x. = ( .r ` ZZring )
31 eqid 
 |-  ( -g ` ZZring ) = ( -g ` ZZring )
32 eqid 
 |-  ( ZZ X. ( ZZ \ { 0 } ) ) = ( ZZ X. ( ZZ \ { 0 } ) )
33 fracval 
 |-  ( Frac ` ZZring ) = ( ZZring RLocal ( RLReg ` ZZring ) )
34 8 idomdomd 
 |-  ( ZZring e. IDomn -> ZZring e. Domn )
35 7 34 ax-mp 
 |-  ZZring e. Domn
36 eqid 
 |-  ( RLReg ` ZZring ) = ( RLReg ` ZZring )
37 28 36 29 isdomn6 
 |-  ( ZZring e. Domn <-> ( ZZring e. NzRing /\ ( ZZ \ { 0 } ) = ( RLReg ` ZZring ) ) )
38 35 37 mpbi 
 |-  ( ZZring e. NzRing /\ ( ZZ \ { 0 } ) = ( RLReg ` ZZring ) )
39 38 simpri 
 |-  ( ZZ \ { 0 } ) = ( RLReg ` ZZring )
40 39 oveq2i 
 |-  ( ZZring RLocal ( ZZ \ { 0 } ) ) = ( ZZring RLocal ( RLReg ` ZZring ) )
41 33 40 eqtr4i 
 |-  ( Frac ` ZZring ) = ( ZZring RLocal ( ZZ \ { 0 } ) )
42 7 a1i 
 |-  ( T. -> ZZring e. IDomn )
43 difssd 
 |-  ( T. -> ( ZZ \ { 0 } ) C_ ZZ )
44 28 29 30 31 32 41 2 42 43 rlocbas 
 |-  ( T. -> ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) = ( Base ` ( Frac ` ZZring ) ) )
45 44 mptru 
 |-  ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) = ( Base ` ( Frac ` ZZring ) )
46 27 45 eleqtrdi 
 |-  ( q e. QQ -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) )
47 3 46 fmpti 
 |-  F : QQ --> ( Base ` ( Frac ` ZZring ) )
48 ecexg 
 |-  ( .~ e. _V -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. _V )
49 25 48 ax-mp 
 |-  [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. _V
50 3 fvmpt2 
 |-  ( ( q e. QQ /\ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. _V ) -> ( F ` q ) = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
51 49 50 mpan2 
 |-  ( q e. QQ -> ( F ` q ) = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
52 51 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( F ` q ) = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
53 fveq2 
 |-  ( q = p -> ( numer ` q ) = ( numer ` p ) )
54 fveq2 
 |-  ( q = p -> ( denom ` q ) = ( denom ` p ) )
55 53 54 opeq12d 
 |-  ( q = p -> <. ( numer ` q ) , ( denom ` q ) >. = <. ( numer ` p ) , ( denom ` p ) >. )
56 55 eceq1d 
 |-  ( q = p -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ )
57 56 3 27 fvmpt3 
 |-  ( p e. QQ -> ( F ` p ) = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ )
58 57 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( F ` p ) = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ )
59 52 58 oveq12d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) )
60 41 fveq2i 
 |-  ( +g ` ( Frac ` ZZring ) ) = ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) )
61 60 oveqi 
 |-  ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) )
62 61 a1i 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( ( F ` q ) ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) ( F ` p ) ) )
63 fveq2 
 |-  ( q = u -> ( numer ` q ) = ( numer ` u ) )
64 fveq2 
 |-  ( q = u -> ( denom ` q ) = ( denom ` u ) )
65 63 64 opeq12d 
 |-  ( q = u -> <. ( numer ` q ) , ( denom ` q ) >. = <. ( numer ` u ) , ( denom ` u ) >. )
66 65 eceq1d 
 |-  ( q = u -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ )
67 66 cbvmptv 
 |-  ( q e. QQ |-> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) = ( u e. QQ |-> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ )
68 3 67 eqtri 
 |-  F = ( u e. QQ |-> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ )
69 zring1 
 |-  1 = ( 1r ` ZZring )
70 7 a1i 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ZZring e. IDomn )
71 70 idomcringd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ZZring e. CRing )
72 35 a1i 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ZZring e. Domn )
73 eqid 
 |-  ( mulGrp ` ZZring ) = ( mulGrp ` ZZring )
74 28 29 73 isdomn3 
 |-  ( ZZring e. Domn <-> ( ZZring e. Ring /\ ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) ) )
75 72 74 sylib 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ZZring e. Ring /\ ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) ) )
76 75 simprd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) )
77 28 29 69 30 31 32 2 71 76 erler 
 |-  ( ( q e. QQ /\ p e. QQ ) -> .~ Er ( ZZ X. ( ZZ \ { 0 } ) ) )
78 qcn 
 |-  ( q e. QQ -> q e. CC )
79 78 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> q e. CC )
80 qcn 
 |-  ( p e. QQ -> p e. CC )
81 80 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> p e. CC )
82 79 81 addcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( q + p ) e. CC )
83 qaddcl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( q + p ) e. QQ )
84 qdencl 
 |-  ( ( q + p ) e. QQ -> ( denom ` ( q + p ) ) e. NN )
85 83 84 syl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q + p ) ) e. NN )
86 85 nncnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q + p ) ) e. CC )
87 20 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` q ) e. NN )
88 87 nncnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` q ) e. CC )
89 qdencl 
 |-  ( p e. QQ -> ( denom ` p ) e. NN )
90 89 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` p ) e. NN )
91 90 nncnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` p ) e. CC )
92 88 91 mulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` q ) x. ( denom ` p ) ) e. CC )
93 82 86 92 mul32d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q + p ) x. ( denom ` ( q + p ) ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( ( q + p ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) x. ( denom ` ( q + p ) ) ) )
94 qmuldeneqnum 
 |-  ( ( q + p ) e. QQ -> ( ( q + p ) x. ( denom ` ( q + p ) ) ) = ( numer ` ( q + p ) ) )
95 83 94 syl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q + p ) x. ( denom ` ( q + p ) ) ) = ( numer ` ( q + p ) ) )
96 95 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q + p ) x. ( denom ` ( q + p ) ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( numer ` ( q + p ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) )
97 79 88 91 mulassd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q x. ( denom ` q ) ) x. ( denom ` p ) ) = ( q x. ( ( denom ` q ) x. ( denom ` p ) ) ) )
98 qmuldeneqnum 
 |-  ( q e. QQ -> ( q x. ( denom ` q ) ) = ( numer ` q ) )
99 98 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( q x. ( denom ` q ) ) = ( numer ` q ) )
100 99 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q x. ( denom ` q ) ) x. ( denom ` p ) ) = ( ( numer ` q ) x. ( denom ` p ) ) )
101 97 100 eqtr3d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( q x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( numer ` q ) x. ( denom ` p ) ) )
102 81 91 88 mulassd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( p x. ( denom ` p ) ) x. ( denom ` q ) ) = ( p x. ( ( denom ` p ) x. ( denom ` q ) ) ) )
103 qmuldeneqnum 
 |-  ( p e. QQ -> ( p x. ( denom ` p ) ) = ( numer ` p ) )
104 103 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( p x. ( denom ` p ) ) = ( numer ` p ) )
105 104 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( p x. ( denom ` p ) ) x. ( denom ` q ) ) = ( ( numer ` p ) x. ( denom ` q ) ) )
106 91 88 mulcomd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` p ) x. ( denom ` q ) ) = ( ( denom ` q ) x. ( denom ` p ) ) )
107 106 oveq2d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( p x. ( ( denom ` p ) x. ( denom ` q ) ) ) = ( p x. ( ( denom ` q ) x. ( denom ` p ) ) ) )
108 102 105 107 3eqtr3rd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( p x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( numer ` p ) x. ( denom ` q ) ) )
109 101 108 oveq12d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q x. ( ( denom ` q ) x. ( denom ` p ) ) ) + ( p x. ( ( denom ` q ) x. ( denom ` p ) ) ) ) = ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) )
110 79 92 81 109 joinlmuladdmuld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q + p ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) )
111 110 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q + p ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) x. ( denom ` ( q + p ) ) ) = ( ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) x. ( denom ` ( q + p ) ) ) )
112 93 96 111 3eqtr3d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( numer ` ( q + p ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) x. ( denom ` ( q + p ) ) ) )
113 39 oveq2i 
 |-  ( ZZring ~RL ( ZZ \ { 0 } ) ) = ( ZZring ~RL ( RLReg ` ZZring ) )
114 2 113 eqtri 
 |-  .~ = ( ZZring ~RL ( RLReg ` ZZring ) )
115 qnumcl 
 |-  ( ( q + p ) e. QQ -> ( numer ` ( q + p ) ) e. ZZ )
116 83 115 syl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( numer ` ( q + p ) ) e. ZZ )
117 19 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( numer ` q ) e. ZZ )
118 89 nnzd 
 |-  ( p e. QQ -> ( denom ` p ) e. ZZ )
119 118 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` p ) e. ZZ )
120 117 119 zmulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( numer ` q ) x. ( denom ` p ) ) e. ZZ )
121 qnumcl 
 |-  ( p e. QQ -> ( numer ` p ) e. ZZ )
122 121 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( numer ` p ) e. ZZ )
123 21 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` q ) e. ZZ )
124 122 123 zmulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( numer ` p ) x. ( denom ` q ) ) e. ZZ )
125 120 124 zaddcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) e. ZZ )
126 85 nnzd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q + p ) ) e. ZZ )
127 85 nnne0d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q + p ) ) =/= 0 )
128 126 127 eldifsnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q + p ) ) e. ( ZZ \ { 0 } ) )
129 128 39 eleqtrdi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q + p ) ) e. ( RLReg ` ZZring ) )
130 123 119 zmulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` q ) x. ( denom ` p ) ) e. ZZ )
131 87 90 nnmulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` q ) x. ( denom ` p ) ) e. NN )
132 131 nnne0d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` q ) x. ( denom ` p ) ) =/= 0 )
133 130 132 eldifsnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` q ) x. ( denom ` p ) ) e. ( ZZ \ { 0 } ) )
134 133 39 eleqtrdi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( denom ` q ) x. ( denom ` p ) ) e. ( RLReg ` ZZring ) )
135 28 30 114 71 116 125 129 134 fracerl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. .~ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. <-> ( ( numer ` ( q + p ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) x. ( denom ` ( q + p ) ) ) ) )
136 112 135 mpbird 
 |-  ( ( q e. QQ /\ p e. QQ ) -> <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. .~ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. )
137 77 136 erthi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> [ <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. ] .~ = [ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ )
138 137 adantr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> [ <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. ] .~ = [ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ )
139 fveq2 
 |-  ( u = ( q + p ) -> ( numer ` u ) = ( numer ` ( q + p ) ) )
140 fveq2 
 |-  ( u = ( q + p ) -> ( denom ` u ) = ( denom ` ( q + p ) ) )
141 139 140 opeq12d 
 |-  ( u = ( q + p ) -> <. ( numer ` u ) , ( denom ` u ) >. = <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. )
142 141 adantl 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> <. ( numer ` u ) , ( denom ` u ) >. = <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. )
143 142 eceq1d 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ = [ <. ( numer ` ( q + p ) ) , ( denom ` ( q + p ) ) >. ] .~ )
144 zringplusg 
 |-  + = ( +g ` ZZring )
145 eqid 
 |-  ( ZZring RLocal ( ZZ \ { 0 } ) ) = ( ZZring RLocal ( ZZ \ { 0 } ) )
146 zringcrng 
 |-  ZZring e. CRing
147 146 a1i 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ZZring e. CRing )
148 35 74 mpbi 
 |-  ( ZZring e. Ring /\ ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) )
149 148 simpri 
 |-  ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) )
150 149 a1i 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) )
151 117 adantr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( numer ` q ) e. ZZ )
152 122 adantr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( numer ` p ) e. ZZ )
153 23 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` q ) e. ( ZZ \ { 0 } ) )
154 153 adantr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( denom ` q ) e. ( ZZ \ { 0 } ) )
155 89 nnne0d 
 |-  ( p e. QQ -> ( denom ` p ) =/= 0 )
156 118 155 eldifsnd 
 |-  ( p e. QQ -> ( denom ` p ) e. ( ZZ \ { 0 } ) )
157 156 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` p ) e. ( ZZ \ { 0 } ) )
158 157 adantr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( denom ` p ) e. ( ZZ \ { 0 } ) )
159 eqid 
 |-  ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) = ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) )
160 28 30 144 145 2 147 150 151 152 154 158 159 rlocaddval 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( ( ( numer ` q ) x. ( denom ` p ) ) + ( ( numer ` p ) x. ( denom ` q ) ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ )
161 138 143 160 3eqtr4d 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ u = ( q + p ) ) -> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) )
162 ovexd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) e. _V )
163 68 161 83 162 fvmptd2 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q + p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( +g ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) )
164 59 62 163 3eqtr4rd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) )
165 164 rgen2 
 |-  A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) )
166 47 165 pm3.2i 
 |-  ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) )
167 1 qrngbas 
 |-  QQ = ( Base ` Q )
168 eqid 
 |-  ( Base ` ( Frac ` ZZring ) ) = ( Base ` ( Frac ` ZZring ) )
169 qex 
 |-  QQ e. _V
170 cnfldadd 
 |-  + = ( +g ` CCfld )
171 1 170 ressplusg 
 |-  ( QQ e. _V -> + = ( +g ` Q ) )
172 169 171 ax-mp 
 |-  + = ( +g ` Q )
173 eqid 
 |-  ( +g ` ( Frac ` ZZring ) ) = ( +g ` ( Frac ` ZZring ) )
174 167 168 172 173 isghm 
 |-  ( F e. ( Q GrpHom ( Frac ` ZZring ) ) <-> ( ( Q e. Grp /\ ( Frac ` ZZring ) e. Grp ) /\ ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q + p ) ) = ( ( F ` q ) ( +g ` ( Frac ` ZZring ) ) ( F ` p ) ) ) ) )
175 18 166 174 mpbir2an 
 |-  F e. ( Q GrpHom ( Frac ` ZZring ) )
176 eqid 
 |-  ( mulGrp ` Q ) = ( mulGrp ` Q )
177 176 ringmgp 
 |-  ( Q e. Ring -> ( mulGrp ` Q ) e. Mnd )
178 6 177 ax-mp 
 |-  ( mulGrp ` Q ) e. Mnd
179 eqid 
 |-  ( mulGrp ` ( Frac ` ZZring ) ) = ( mulGrp ` ( Frac ` ZZring ) )
180 179 ringmgp 
 |-  ( ( Frac ` ZZring ) e. Ring -> ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd )
181 12 180 ax-mp 
 |-  ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd
182 178 181 pm3.2i 
 |-  ( ( mulGrp ` Q ) e. Mnd /\ ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd )
183 eqid 
 |-  ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) )
184 28 30 144 145 2 71 76 117 122 153 157 183 rlocmulval 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( ( numer ` q ) x. ( numer ` p ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ )
185 79 81 mulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( q x. p ) e. CC )
186 qmulcl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( q x. p ) e. QQ )
187 qdencl 
 |-  ( ( q x. p ) e. QQ -> ( denom ` ( q x. p ) ) e. NN )
188 186 187 syl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q x. p ) ) e. NN )
189 188 nncnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q x. p ) ) e. CC )
190 185 189 92 mul32d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q x. p ) x. ( denom ` ( q x. p ) ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( ( q x. p ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) x. ( denom ` ( q x. p ) ) ) )
191 79 81 88 91 mul4d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q x. p ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( q x. ( denom ` q ) ) x. ( p x. ( denom ` p ) ) ) )
192 191 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q x. p ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) x. ( denom ` ( q x. p ) ) ) = ( ( ( q x. ( denom ` q ) ) x. ( p x. ( denom ` p ) ) ) x. ( denom ` ( q x. p ) ) ) )
193 190 192 eqtrd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q x. p ) x. ( denom ` ( q x. p ) ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( ( q x. ( denom ` q ) ) x. ( p x. ( denom ` p ) ) ) x. ( denom ` ( q x. p ) ) ) )
194 qmuldeneqnum 
 |-  ( ( q x. p ) e. QQ -> ( ( q x. p ) x. ( denom ` ( q x. p ) ) ) = ( numer ` ( q x. p ) ) )
195 186 194 syl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q x. p ) x. ( denom ` ( q x. p ) ) ) = ( numer ` ( q x. p ) ) )
196 195 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q x. p ) x. ( denom ` ( q x. p ) ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) = ( ( numer ` ( q x. p ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) )
197 99 104 oveq12d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( q x. ( denom ` q ) ) x. ( p x. ( denom ` p ) ) ) = ( ( numer ` q ) x. ( numer ` p ) ) )
198 197 oveq1d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( q x. ( denom ` q ) ) x. ( p x. ( denom ` p ) ) ) x. ( denom ` ( q x. p ) ) ) = ( ( ( numer ` q ) x. ( numer ` p ) ) x. ( denom ` ( q x. p ) ) ) )
199 193 196 198 3eqtr3rd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( numer ` q ) x. ( numer ` p ) ) x. ( denom ` ( q x. p ) ) ) = ( ( numer ` ( q x. p ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) )
200 117 122 zmulcld 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( numer ` q ) x. ( numer ` p ) ) e. ZZ )
201 qnumcl 
 |-  ( ( q x. p ) e. QQ -> ( numer ` ( q x. p ) ) e. ZZ )
202 186 201 syl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( numer ` ( q x. p ) ) e. ZZ )
203 188 nnzd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q x. p ) ) e. ZZ )
204 188 nnne0d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q x. p ) ) =/= 0 )
205 203 204 eldifsnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q x. p ) ) e. ( ZZ \ { 0 } ) )
206 205 39 eleqtrdi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` ( q x. p ) ) e. ( RLReg ` ZZring ) )
207 28 30 114 71 200 202 134 206 fracerl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( <. ( ( numer ` q ) x. ( numer ` p ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. .~ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. <-> ( ( ( numer ` q ) x. ( numer ` p ) ) x. ( denom ` ( q x. p ) ) ) = ( ( numer ` ( q x. p ) ) x. ( ( denom ` q ) x. ( denom ` p ) ) ) ) )
208 199 207 mpbird 
 |-  ( ( q e. QQ /\ p e. QQ ) -> <. ( ( numer ` q ) x. ( numer ` p ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. .~ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. )
209 77 208 erthi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> [ <. ( ( numer ` q ) x. ( numer ` p ) ) , ( ( denom ` q ) x. ( denom ` p ) ) >. ] .~ = [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ )
210 184 209 eqtrd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) = [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ )
211 41 fveq2i 
 |-  ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) )
212 211 a1i 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) )
213 212 52 58 oveq123d 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) = ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ( .r ` ( ZZring RLocal ( ZZ \ { 0 } ) ) ) [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) )
214 fveq2 
 |-  ( u = ( q x. p ) -> ( numer ` u ) = ( numer ` ( q x. p ) ) )
215 fveq2 
 |-  ( u = ( q x. p ) -> ( denom ` u ) = ( denom ` ( q x. p ) ) )
216 214 215 opeq12d 
 |-  ( u = ( q x. p ) -> <. ( numer ` u ) , ( denom ` u ) >. = <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. )
217 216 eceq1d 
 |-  ( u = ( q x. p ) -> [ <. ( numer ` u ) , ( denom ` u ) >. ] .~ = [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ )
218 ecexg 
 |-  ( .~ e. _V -> [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ e. _V )
219 25 218 mp1i 
 |-  ( ( q e. QQ /\ p e. QQ ) -> [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ e. _V )
220 68 217 186 219 fvmptd3 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q x. p ) ) = [ <. ( numer ` ( q x. p ) ) , ( denom ` ( q x. p ) ) >. ] .~ )
221 210 213 220 3eqtr4rd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) )
222 221 rgen2 
 |-  A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) )
223 zssq 
 |-  ZZ C_ QQ
224 1z 
 |-  1 e. ZZ
225 223 224 sselii 
 |-  1 e. QQ
226 fveq2 
 |-  ( q = 1 -> ( numer ` q ) = ( numer ` 1 ) )
227 1zzd 
 |-  ( ZZring e. IDomn -> 1 e. ZZ )
228 227 znumd 
 |-  ( ZZring e. IDomn -> ( numer ` 1 ) = 1 )
229 7 228 ax-mp 
 |-  ( numer ` 1 ) = 1
230 226 229 eqtrdi 
 |-  ( q = 1 -> ( numer ` q ) = 1 )
231 fveq2 
 |-  ( q = 1 -> ( denom ` q ) = ( denom ` 1 ) )
232 227 zdend 
 |-  ( ZZring e. IDomn -> ( denom ` 1 ) = 1 )
233 7 232 ax-mp 
 |-  ( denom ` 1 ) = 1
234 231 233 eqtrdi 
 |-  ( q = 1 -> ( denom ` q ) = 1 )
235 230 234 opeq12d 
 |-  ( q = 1 -> <. ( numer ` q ) , ( denom ` q ) >. = <. 1 , 1 >. )
236 235 eceq1d 
 |-  ( q = 1 -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. 1 , 1 >. ] .~ )
237 236 3 49 fvmpt3i 
 |-  ( 1 e. QQ -> ( F ` 1 ) = [ <. 1 , 1 >. ] .~ )
238 225 237 ax-mp 
 |-  ( F ` 1 ) = [ <. 1 , 1 >. ] .~
239 47 222 238 3pm3.2i 
 |-  ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) /\ ( F ` 1 ) = [ <. 1 , 1 >. ] .~ )
240 176 167 mgpbas 
 |-  QQ = ( Base ` ( mulGrp ` Q ) )
241 179 168 mgpbas 
 |-  ( Base ` ( Frac ` ZZring ) ) = ( Base ` ( mulGrp ` ( Frac ` ZZring ) ) )
242 cnfldmul 
 |-  x. = ( .r ` CCfld )
243 1 242 ressmulr 
 |-  ( QQ e. _V -> x. = ( .r ` Q ) )
244 169 243 ax-mp 
 |-  x. = ( .r ` Q )
245 176 244 mgpplusg 
 |-  x. = ( +g ` ( mulGrp ` Q ) )
246 eqid 
 |-  ( .r ` ( Frac ` ZZring ) ) = ( .r ` ( Frac ` ZZring ) )
247 179 246 mgpplusg 
 |-  ( .r ` ( Frac ` ZZring ) ) = ( +g ` ( mulGrp ` ( Frac ` ZZring ) ) )
248 1 qrng1 
 |-  1 = ( 1r ` Q )
249 176 248 ringidval 
 |-  1 = ( 0g ` ( mulGrp ` Q ) )
250 146 a1i 
 |-  ( ZZring e. IDomn -> ZZring e. CRing )
251 149 a1i 
 |-  ( ZZring e. IDomn -> ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) )
252 eqid 
 |-  [ <. 1 , 1 >. ] .~ = [ <. 1 , 1 >. ] .~
253 29 69 41 2 250 251 252 rloc1r 
 |-  ( ZZring e. IDomn -> [ <. 1 , 1 >. ] .~ = ( 1r ` ( Frac ` ZZring ) ) )
254 7 253 ax-mp 
 |-  [ <. 1 , 1 >. ] .~ = ( 1r ` ( Frac ` ZZring ) )
255 179 254 ringidval 
 |-  [ <. 1 , 1 >. ] .~ = ( 0g ` ( mulGrp ` ( Frac ` ZZring ) ) )
256 240 241 245 247 249 255 ismhm 
 |-  ( F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) <-> ( ( ( mulGrp ` Q ) e. Mnd /\ ( mulGrp ` ( Frac ` ZZring ) ) e. Mnd ) /\ ( F : QQ --> ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( F ` ( q x. p ) ) = ( ( F ` q ) ( .r ` ( Frac ` ZZring ) ) ( F ` p ) ) /\ ( F ` 1 ) = [ <. 1 , 1 >. ] .~ ) ) )
257 182 239 256 mpbir2an 
 |-  F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) )
258 175 257 pm3.2i 
 |-  ( F e. ( Q GrpHom ( Frac ` ZZring ) ) /\ F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) )
259 176 179 isrhm 
 |-  ( F e. ( Q RingHom ( Frac ` ZZring ) ) <-> ( ( Q e. Ring /\ ( Frac ` ZZring ) e. Ring ) /\ ( F e. ( Q GrpHom ( Frac ` ZZring ) ) /\ F e. ( ( mulGrp ` Q ) MndHom ( mulGrp ` ( Frac ` ZZring ) ) ) ) ) )
260 13 258 259 mpbir2an 
 |-  F e. ( Q RingHom ( Frac ` ZZring ) )
261 46 rgen 
 |-  A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) )
262 117 zcnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( numer ` q ) e. CC )
263 122 zcnd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( numer ` p ) e. CC )
264 22 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` q ) =/= 0 )
265 155 adantl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` p ) =/= 0 )
266 262 88 263 91 264 265 divmuleqd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( ( ( numer ` q ) / ( denom ` q ) ) = ( ( numer ` p ) / ( denom ` p ) ) <-> ( ( numer ` q ) x. ( denom ` p ) ) = ( ( numer ` p ) x. ( denom ` q ) ) ) )
267 153 39 eleqtrdi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` q ) e. ( RLReg ` ZZring ) )
268 157 39 eleqtrdi 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( denom ` p ) e. ( RLReg ` ZZring ) )
269 28 30 114 71 117 122 267 268 fracerl 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( <. ( numer ` q ) , ( denom ` q ) >. .~ <. ( numer ` p ) , ( denom ` p ) >. <-> ( ( numer ` q ) x. ( denom ` p ) ) = ( ( numer ` p ) x. ( denom ` q ) ) ) )
270 24 adantr 
 |-  ( ( q e. QQ /\ p e. QQ ) -> <. ( numer ` q ) , ( denom ` q ) >. e. ( ZZ X. ( ZZ \ { 0 } ) ) )
271 77 270 erth 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( <. ( numer ` q ) , ( denom ` q ) >. .~ <. ( numer ` p ) , ( denom ` p ) >. <-> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) )
272 266 269 271 3bitr2rd 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ <-> ( ( numer ` q ) / ( denom ` q ) ) = ( ( numer ` p ) / ( denom ` p ) ) ) )
273 272 biimpa 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) -> ( ( numer ` q ) / ( denom ` q ) ) = ( ( numer ` p ) / ( denom ` p ) ) )
274 qeqnumdivden 
 |-  ( q e. QQ -> q = ( ( numer ` q ) / ( denom ` q ) ) )
275 274 ad2antrr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) -> q = ( ( numer ` q ) / ( denom ` q ) ) )
276 qeqnumdivden 
 |-  ( p e. QQ -> p = ( ( numer ` p ) / ( denom ` p ) ) )
277 276 ad2antlr 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) -> p = ( ( numer ` p ) / ( denom ` p ) ) )
278 273 275 277 3eqtr4d 
 |-  ( ( ( q e. QQ /\ p e. QQ ) /\ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ ) -> q = p )
279 278 ex 
 |-  ( ( q e. QQ /\ p e. QQ ) -> ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ -> q = p ) )
280 279 rgen2 
 |-  A. q e. QQ A. p e. QQ ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ -> q = p )
281 3 56 f1mpt 
 |-  ( F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) <-> ( A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) /\ A. q e. QQ A. p e. QQ ( [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` p ) , ( denom ` p ) >. ] .~ -> q = p ) ) )
282 261 280 281 mpbir2an 
 |-  F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) )
283 fveq2 
 |-  ( q = ( a / b ) -> ( numer ` q ) = ( numer ` ( a / b ) ) )
284 fveq2 
 |-  ( q = ( a / b ) -> ( denom ` q ) = ( denom ` ( a / b ) ) )
285 283 284 opeq12d 
 |-  ( q = ( a / b ) -> <. ( numer ` q ) , ( denom ` q ) >. = <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. )
286 285 eceq1d 
 |-  ( q = ( a / b ) -> [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ )
287 286 eqeq2d 
 |-  ( q = ( a / b ) -> ( z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ <-> z = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ ) )
288 simpllr 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> a e. ZZ )
289 223 288 sselid 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> a e. QQ )
290 simplr 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. ( ZZ \ { 0 } ) )
291 290 eldifad 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. ZZ )
292 223 291 sselid 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b e. QQ )
293 eldifsni 
 |-  ( b e. ( ZZ \ { 0 } ) -> b =/= 0 )
294 290 293 syl 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> b =/= 0 )
295 qdivcl 
 |-  ( ( a e. QQ /\ b e. QQ /\ b =/= 0 ) -> ( a / b ) e. QQ )
296 289 292 294 295 syl3anc 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ( a / b ) e. QQ )
297 simpr 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> z = [ <. a , b >. ] .~ )
298 146 a1i 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ZZring e. CRing )
299 149 a1i 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> ( ZZ \ { 0 } ) e. ( SubMnd ` ( mulGrp ` ZZring ) ) )
300 28 29 69 30 31 32 2 298 299 erler 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> .~ Er ( ZZ X. ( ZZ \ { 0 } ) ) )
301 simpl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> a e. ZZ )
302 301 zcnd 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> a e. CC )
303 eldifi 
 |-  ( b e. ( ZZ \ { 0 } ) -> b e. ZZ )
304 303 adantl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> b e. ZZ )
305 304 zcnd 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> b e. CC )
306 293 adantl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> b =/= 0 )
307 302 305 306 divcld 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( a / b ) e. CC )
308 223 301 sselid 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> a e. QQ )
309 223 304 sselid 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> b e. QQ )
310 308 309 306 295 syl3anc 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( a / b ) e. QQ )
311 qdencl 
 |-  ( ( a / b ) e. QQ -> ( denom ` ( a / b ) ) e. NN )
312 310 311 syl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( denom ` ( a / b ) ) e. NN )
313 312 nncnd 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( denom ` ( a / b ) ) e. CC )
314 307 313 305 mul32d 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( ( ( a / b ) x. ( denom ` ( a / b ) ) ) x. b ) = ( ( ( a / b ) x. b ) x. ( denom ` ( a / b ) ) ) )
315 qmuldeneqnum 
 |-  ( ( a / b ) e. QQ -> ( ( a / b ) x. ( denom ` ( a / b ) ) ) = ( numer ` ( a / b ) ) )
316 310 315 syl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( ( a / b ) x. ( denom ` ( a / b ) ) ) = ( numer ` ( a / b ) ) )
317 316 oveq1d 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( ( ( a / b ) x. ( denom ` ( a / b ) ) ) x. b ) = ( ( numer ` ( a / b ) ) x. b ) )
318 302 305 306 divcan1d 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( ( a / b ) x. b ) = a )
319 318 oveq1d 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( ( ( a / b ) x. b ) x. ( denom ` ( a / b ) ) ) = ( a x. ( denom ` ( a / b ) ) ) )
320 314 317 319 3eqtr3rd 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( a x. ( denom ` ( a / b ) ) ) = ( ( numer ` ( a / b ) ) x. b ) )
321 146 a1i 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ZZring e. CRing )
322 qnumcl 
 |-  ( ( a / b ) e. QQ -> ( numer ` ( a / b ) ) e. ZZ )
323 310 322 syl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( numer ` ( a / b ) ) e. ZZ )
324 simpr 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> b e. ( ZZ \ { 0 } ) )
325 324 39 eleqtrdi 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> b e. ( RLReg ` ZZring ) )
326 312 nnzd 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( denom ` ( a / b ) ) e. ZZ )
327 312 nnne0d 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( denom ` ( a / b ) ) =/= 0 )
328 326 327 eldifsnd 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( denom ` ( a / b ) ) e. ( ZZ \ { 0 } ) )
329 328 39 eleqtrdi 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( denom ` ( a / b ) ) e. ( RLReg ` ZZring ) )
330 28 30 114 321 301 323 325 329 fracerl 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> ( <. a , b >. .~ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. <-> ( a x. ( denom ` ( a / b ) ) ) = ( ( numer ` ( a / b ) ) x. b ) ) )
331 320 330 mpbird 
 |-  ( ( a e. ZZ /\ b e. ( ZZ \ { 0 } ) ) -> <. a , b >. .~ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. )
332 331 ad4ant23 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> <. a , b >. .~ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. )
333 300 332 erthi 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> [ <. a , b >. ] .~ = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ )
334 297 333 eqtrd 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> z = [ <. ( numer ` ( a / b ) ) , ( denom ` ( a / b ) ) >. ] .~ )
335 287 296 334 rspcedvdw 
 |-  ( ( ( ( z e. ( Base ` ( Frac ` ZZring ) ) /\ a e. ZZ ) /\ b e. ( ZZ \ { 0 } ) ) /\ z = [ <. a , b >. ] .~ ) -> E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
336 45 eleq2i 
 |-  ( z e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) <-> z e. ( Base ` ( Frac ` ZZring ) ) )
337 336 biimpri 
 |-  ( z e. ( Base ` ( Frac ` ZZring ) ) -> z e. ( ( ZZ X. ( ZZ \ { 0 } ) ) /. .~ ) )
338 337 elrlocbasi 
 |-  ( z e. ( Base ` ( Frac ` ZZring ) ) -> E. a e. ZZ E. b e. ( ZZ \ { 0 } ) z = [ <. a , b >. ] .~ )
339 335 338 r19.29vva 
 |-  ( z e. ( Base ` ( Frac ` ZZring ) ) -> E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ )
340 339 rgen 
 |-  A. z e. ( Base ` ( Frac ` ZZring ) ) E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~
341 3 fompt 
 |-  ( F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) <-> ( A. q e. QQ [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ e. ( Base ` ( Frac ` ZZring ) ) /\ A. z e. ( Base ` ( Frac ` ZZring ) ) E. q e. QQ z = [ <. ( numer ` q ) , ( denom ` q ) >. ] .~ ) )
342 261 340 341 mpbir2an 
 |-  F : QQ -onto-> ( Base ` ( Frac ` ZZring ) )
343 df-f1o 
 |-  ( F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) <-> ( F : QQ -1-1-> ( Base ` ( Frac ` ZZring ) ) /\ F : QQ -onto-> ( Base ` ( Frac ` ZZring ) ) ) )
344 282 342 343 mpbir2an 
 |-  F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) )
345 167 168 isrim 
 |-  ( F e. ( Q RingIso ( Frac ` ZZring ) ) <-> ( F e. ( Q RingHom ( Frac ` ZZring ) ) /\ F : QQ -1-1-onto-> ( Base ` ( Frac ` ZZring ) ) ) )
346 260 344 345 mpbir2an 
 |-  F e. ( Q RingIso ( Frac ` ZZring ) )