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 = ℂ_{fld} ↾_{𝑠} ℚ$
	zringfrac.2	$⊢ \underset{˙}{\sim} = ℤ_{ring} ~_{RL} (ℤ ∖ \{0\})$
	zringfrac.3	$⊢ F = (q \in ℚ ⟼ [⟨numer (q), denom (q)⟩] \underset{˙}{\sim})$
Assertion	zringfrac	$⊢ F \in (Q RingIso Frac (ℤ_{ring}))$

Proof

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

Metamath Proof Explorer

Theorem zringfrac

Proof