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 ⊢ 𝑄 = ( ℂfld ↾s ℚ )
zringfrac.2 ⊢ ∼ = ( ℤring ~RL ( ℤ ∖ { 0 } ) )
zringfrac.3 ⊢ 𝐹 = ( 𝑞 ∈ ℚ ↦ [ ⟨ ( numer ‘ 𝑞 ) , ( denom ‘ 𝑞 ) ⟩ ] ∼ )
Assertion zringfrac 𝐹 ∈ ( 𝑄 RingIso ( Frac ‘ ℤring ) )

Proof

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