zringfrac - Mathbox for Thierry Arnoux

	Mathbox for Thierry Arnoux		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > zringfrac		Structured version Visualization version GIF version

Theorem zringfrac 33635

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.)

**Hypotheses**
Ref	Expression
zringfrac.1	⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
zringfrac.2	⊢ ∼ = (ℤ_ring ~_RL (ℤ ∖ {0}))
zringfrac.3	⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )

**Assertion**
Ref	Expression
zringfrac	⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring))

Distinct variable groups: ∼ ,𝑞 𝐹,𝑞 𝑄,𝑞

Proof of Theorem zringfrac Dummy variables 𝑎 𝑏 𝑧 𝑝 𝑢 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		zringfrac.1	. . . . . 6 ⊢ 𝑄 = (ℂ_fld ↾_s ℚ)
2	1	qdrng 27587	. . . . 5 ⊢ 𝑄 ∈ DivRing
3		drngring 20669	. . . . 5 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
4	2, 3	ax-mp 5	. . . 4 ⊢ 𝑄 ∈ Ring
5		zringidom 33632	. . . . 5 ⊢ ℤ_ring ∈ IDomn
6		id 22	. . . . . . . 8 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ IDomn)
7	6	fracfld 33390	. . . . . . 7 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Field)
8	7	fldcrngd 20675	. . . . . 6 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ CRing)
9	8	crngringd 20181	. . . . 5 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Ring)
10	5, 9	ax-mp 5	. . . 4 ⊢ ( Frac ‘ℤ_ring) ∈ Ring
11	4, 10	pm3.2i 470	. . 3 ⊢ (𝑄 ∈ Ring ∧ ( Frac ‘ℤ_ring) ∈ Ring)
12		ringgrp 20173	. . . . . . 7 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ Grp)
13	4, 12	ax-mp 5	. . . . . 6 ⊢ 𝑄 ∈ Grp
14		ringgrp 20173	. . . . . . 7 ⊢ (( Frac ‘ℤ_ring) ∈ Ring → ( Frac ‘ℤ_ring) ∈ Grp)
15	10, 14	ax-mp 5	. . . . . 6 ⊢ ( Frac ‘ℤ_ring) ∈ Grp
16	13, 15	pm3.2i 470	. . . . 5 ⊢ (𝑄 ∈ Grp ∧ ( Frac ‘ℤ_ring) ∈ Grp)
17		zringfrac.3	. . . . . . 7 ⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
18		qnumcl 16667	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19		qdencl 16668	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
20	19	nnzd 12514	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
21	19	nnne0d 12195	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
22	20, 21	eldifsnd 4743	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
23	18, 22	opelxpd 5663	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24		zringfrac.2	. . . . . . . . . . 11 ⊢ ∼ = (ℤ_ring ~_RL (ℤ ∖ {0}))
25	24	ovexi 7392	. . . . . . . . . 10 ⊢ ∼ ∈ V
26	25	ecelqsi 8707	. . . . . . . . 9 ⊢ (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
27	23, 26	syl 17	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
28		zringbas 21408	. . . . . . . . . 10 ⊢ ℤ = (Base‘ℤ_ring)
29		zring0 21413	. . . . . . . . . 10 ⊢ 0 = (0_g‘ℤ_ring)
30		zringmulr 21412	. . . . . . . . . 10 ⊢ · = (._r‘ℤ_ring)
31		eqid 2736	. . . . . . . . . 10 ⊢ (-_g‘ℤ_ring) = (-_g‘ℤ_ring)
32		eqid 2736	. . . . . . . . . 10 ⊢ (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33		fracval 33386	. . . . . . . . . . 11 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
34	6	idomdomd 20659	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ Domn)
35	5, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℤ_ring ∈ Domn
36		eqid 2736	. . . . . . . . . . . . . . 15 ⊢ (RLReg‘ℤ_ring) = (RLReg‘ℤ_ring)
37	28, 36, 29	isdomn6 20647	. . . . . . . . . . . . . 14 ⊢ (ℤ_ring ∈ Domn ↔ (ℤ_ring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤ_ring)))
38	35, 37	mpbi 230	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤ_ring))
39	38	simpri 485	. . . . . . . . . . . 12 ⊢ (ℤ ∖ {0}) = (RLReg‘ℤ_ring)
40	39	oveq2i 7369	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
41	33, 40	eqtr4i 2762	. . . . . . . . . 10 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (ℤ ∖ {0}))
42	5	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℤ_ring ∈ IDomn)
43		difssd 4089	. . . . . . . . . 10 ⊢ (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
44	28, 29, 30, 31, 32, 41, 24, 42, 43	rlocbas 33349	. . . . . . . . 9 ⊢ (⊤ → ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring)))
45	44	mptru 1548	. . . . . . . 8 ⊢ ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring))
46	27, 45	eleqtrdi 2846	. . . . . . 7 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)))
47	17, 46	fmpti 7057	. . . . . 6 ⊢ 𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring))
48		ecexg 8639	. . . . . . . . . . . 12 ⊢ ( ∼ ∈ V → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V)
49	25, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V
50	17	fvmpt2 6952	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
51	49, 50	mpan2 691	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
52	51	adantr 480	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
53		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
55	53, 54	opeq12d 4837	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
56	55	eceq1d 8675	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
57	56, 17, 27	fvmpt3 6945	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℚ → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
58	57	adantl 481	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
59	52, 58	oveq12d 7376	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
60	41	fveq2i 6837	. . . . . . . . . 10 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
61	60	oveqi 7371	. . . . . . . . 9 ⊢ ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝))
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)))
63		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
65	63, 64	opeq12d 4837	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
66	65	eceq1d 8675	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
67	66	cbvmptv 5202	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
68	17, 67	eqtri 2759	. . . . . . . . 9 ⊢ 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
69		zring1 21414	. . . . . . . . . . . . 13 ⊢ 1 = (1_r‘ℤ_ring)
70	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ IDomn)
71	70	idomcringd 20660	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ CRing)
72	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ Domn)
73		eqid 2736	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘ℤ_ring) = (mulGrp‘ℤ_ring)
74	28, 29, 73	isdomn3 20648	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ Domn ↔ (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))))
75	72, 74	sylib 218	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))))
76	75	simprd 495	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
77	28, 29, 69, 30, 31, 32, 24, 71, 76	erler 33347	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ∼ Er (ℤ × (ℤ ∖ {0})))
78		qcn 12876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80		qcn 12876	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
81	80	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
82	79, 81	addcld 11151	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83		qaddcl 12878	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84		qdencl 16668	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
85	83, 84	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
86	85	nncnd 12161	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
87	19	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
88	87	nncnd 12161	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89		qdencl 16668	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
90	89	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
91	90	nncnd 12161	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
92	88, 91	mulcld 11152	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
93	82, 86, 92	mul32d 11343	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94		qmuldeneqnum 16674	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
95	83, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
96	95	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
97	79, 88, 91	mulassd 11155	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98		qmuldeneqnum 16674	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
99	98	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
100	99	oveq1d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
101	97, 100	eqtr3d 2773	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
102	81, 91, 88	mulassd 11155	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103		qmuldeneqnum 16674	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104	103	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105	104	oveq1d 7373	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
106	91, 88	mulcomd 11153	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107	106	oveq2d 7374	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108	102, 105, 107	3eqtr3rd 2780	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109	101, 108	oveq12d 7376	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
110	79, 92, 81, 109	joinlmuladdmuld 11159	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111	110	oveq1d 7373	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
112	93, 96, 111	3eqtr3d 2779	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
113	39	oveq2i 7369	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ~_RL (ℤ ∖ {0})) = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
114	24, 113	eqtri 2759	. . . . . . . . . . . . . 14 ⊢ ∼ = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
115		qnumcl 16667	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
116	83, 115	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
117	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
118	89	nnzd 12514	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119	118	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120	117, 119	zmulcld 12602	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121		qnumcl 16667	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122	121	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
123	20	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124	122, 123	zmulcld 12602	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125	120, 124	zaddcld 12600	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
126	85	nnzd 12514	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
127	85	nnne0d 12195	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128	126, 127	eldifsnd 4743	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129	128, 39	eleqtrdi 2846	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤ_ring))
130	123, 119	zmulcld 12602	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
131	87, 90	nnmulcld 12198	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132	131	nnne0d 12195	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133	130, 132	eldifsnd 4743	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134	133, 39	eleqtrdi 2846	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤ_ring))
135	28, 30, 114, 71, 116, 125, 129, 134	fracerl 33388	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ∼ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩ ↔ ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝)))))
136	112, 135	mpbird 257	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ∼ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩)
137	77, 136	erthi 8691	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
138	137	adantr 480	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
139		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140		fveq2 6834	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141	139, 140	opeq12d 4837	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142	141	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143	142	eceq1d 8675	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ )
144		zringplusg 21409	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
145		eqid 2736	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (ℤ ∖ {0}))
146		zringcrng 21403	. . . . . . . . . . . 12 ⊢ ℤ_ring ∈ CRing
147	146	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ℤ_ring ∈ CRing)
148	35, 74	mpbi 230	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
149	148	simpri 485	. . . . . . . . . . . 12 ⊢ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))
150	149	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
151	117	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑞) ∈ ℤ)
152	122	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑝) ∈ ℤ)
153	22	adantr 480	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
154	153	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
155	89	nnne0d 12195	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156	118, 155	eldifsnd 4743	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157	156	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158	157	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159		eqid 2736	. . . . . . . . . . 11 ⊢ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
160	28, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159	rlocaddval 33350	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
161	138, 143, 160	3eqtr4d 2781	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
162		ovexd 7393	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) ∈ V)
163	68, 161, 83, 162	fvmptd2 6949	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
164	59, 62, 163	3eqtr4rd 2782	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
165	164	rgen2 3176	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
166	47, 165	pm3.2i 470	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
167	1	qrngbas 27586	. . . . . 6 ⊢ ℚ = (Base‘𝑄)
168		eqid 2736	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘( Frac ‘ℤ_ring))
169		qex 12874	. . . . . . 7 ⊢ ℚ ∈ V
170		cnfldadd 21315	. . . . . . . 8 ⊢ + = (+_g‘ℂ_fld)
171	1, 170	ressplusg 17211	. . . . . . 7 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
172	169, 171	ax-mp 5	. . . . . 6 ⊢ + = (+_g‘𝑄)
173		eqid 2736	. . . . . 6 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘( Frac ‘ℤ_ring))
174	167, 168, 172, 173	isghm 19144	. . . . 5 ⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ↔ ((𝑄 ∈ Grp ∧ ( Frac ‘ℤ_ring) ∈ Grp) ∧ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))))
175	16, 166, 174	mpbir2an 711	. . . 4 ⊢ 𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring))
176		eqid 2736	. . . . . . . 8 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
177	176	ringmgp 20174	. . . . . . 7 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
178	4, 177	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘𝑄) ∈ Mnd
179		eqid 2736	. . . . . . . 8 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) = (mulGrp‘( Frac ‘ℤ_ring))
180	179	ringmgp 20174	. . . . . . 7 ⊢ (( Frac ‘ℤ_ring) ∈ Ring → (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd)
181	10, 180	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd
182	178, 181	pm3.2i 470	. . . . 5 ⊢ ((mulGrp‘𝑄) ∈ Mnd ∧ (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd)
183		eqid 2736	. . . . . . . . . 10 ⊢ (._r‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))
184	28, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183	rlocmulval 33351	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
185	79, 81	mulcld 11152	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186		qmulcl 12880	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187		qdencl 16668	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188	186, 187	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189	188	nncnd 12161	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190	185, 189, 92	mul32d 11343	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
191	79, 81, 88, 91	mul4d 11345	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192	191	oveq1d 7373	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193	190, 192	eqtrd 2771	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194		qmuldeneqnum 16674	. . . . . . . . . . . . . 14 ⊢ ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195	186, 194	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196	195	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
197	99, 104	oveq12d 7376	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198	197	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199	193, 196, 198	3eqtr3rd 2780	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200	117, 122	zmulcld 12602	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201		qnumcl 16667	. . . . . . . . . . . . 13 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202	186, 201	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203	188	nnzd 12514	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204	188	nnne0d 12195	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205	203, 204	eldifsnd 4743	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206	205, 39	eleqtrdi 2846	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤ_ring))
207	28, 30, 114, 71, 200, 202, 134, 206	fracerl 33388	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ∼ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩ ↔ (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))))
208	199, 207	mpbird 257	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ∼ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
209	77, 208	erthi 8691	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
210	184, 209	eqtrd 2771	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
211	41	fveq2i 6837	. . . . . . . . . 10 ⊢ (._r‘( Frac ‘ℤ_ring)) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))
212	211	a1i 11	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (._r‘( Frac ‘ℤ_ring)) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0}))))
213	212, 52, 58	oveq123d 7379	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
214		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216	214, 215	opeq12d 4837	. . . . . . . . . 10 ⊢ (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217	216	eceq1d 8675	. . . . . . . . 9 ⊢ (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
218		ecexg 8639	. . . . . . . . . 10 ⊢ ( ∼ ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
219	25, 218	mp1i 13	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
220	68, 217, 186, 219	fvmptd3 6964	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
221	210, 213, 220	3eqtr4rd 2782	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
222	221	rgen2 3176	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
223		zssq 12869	. . . . . . . 8 ⊢ ℤ ⊆ ℚ
224		1z 12521	. . . . . . . 8 ⊢ 1 ∈ ℤ
225	223, 224	sselii 3930	. . . . . . 7 ⊢ 1 ∈ ℚ
226		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227		1zzd 12522	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ IDomn → 1 ∈ ℤ)
228	227	znumd 32893	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (numer‘1) = 1)
229	5, 228	ax-mp 5	. . . . . . . . . . 11 ⊢ (numer‘1) = 1
230	226, 229	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (numer‘𝑞) = 1)
231		fveq2 6834	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232	227	zdend 32894	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (denom‘1) = 1)
233	5, 232	ax-mp 5	. . . . . . . . . . 11 ⊢ (denom‘1) = 1
234	231, 233	eqtrdi 2787	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (denom‘𝑞) = 1)
235	230, 234	opeq12d 4837	. . . . . . . . 9 ⊢ (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236	235	eceq1d 8675	. . . . . . . 8 ⊢ (𝑞 = 1 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨1, 1⟩] ∼ )
237	236, 17, 49	fvmpt3i 6946	. . . . . . 7 ⊢ (1 ∈ ℚ → (𝐹‘1) = [⟨1, 1⟩] ∼ )
238	225, 237	ax-mp 5	. . . . . 6 ⊢ (𝐹‘1) = [⟨1, 1⟩] ∼
239	47, 222, 238	3pm3.2i 1340	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] ∼ )
240	176, 167	mgpbas 20080	. . . . . 6 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
241	179, 168	mgpbas 20080	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘(mulGrp‘( Frac ‘ℤ_ring)))
242		cnfldmul 21317	. . . . . . . . 9 ⊢ · = (._r‘ℂ_fld)
243	1, 242	ressmulr 17227	. . . . . . . 8 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
244	169, 243	ax-mp 5	. . . . . . 7 ⊢ · = (._r‘𝑄)
245	176, 244	mgpplusg 20079	. . . . . 6 ⊢ · = (+_g‘(mulGrp‘𝑄))
246		eqid 2736	. . . . . . 7 ⊢ (._r‘( Frac ‘ℤ_ring)) = (._r‘( Frac ‘ℤ_ring))
247	179, 246	mgpplusg 20079	. . . . . 6 ⊢ (._r‘( Frac ‘ℤ_ring)) = (+_g‘(mulGrp‘( Frac ‘ℤ_ring)))
248	1	qrng1 27589	. . . . . . 7 ⊢ 1 = (1_r‘𝑄)
249	176, 248	ringidval 20118	. . . . . 6 ⊢ 1 = (0_g‘(mulGrp‘𝑄))
250	146	a1i 11	. . . . . . . . 9 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ CRing)
251	149	a1i 11	. . . . . . . . 9 ⊢ (ℤ_ring ∈ IDomn → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
252		eqid 2736	. . . . . . . . 9 ⊢ [⟨1, 1⟩] ∼ = [⟨1, 1⟩] ∼
253	29, 69, 41, 24, 250, 251, 252	rloc1r 33354	. . . . . . . 8 ⊢ (ℤ_ring ∈ IDomn → [⟨1, 1⟩] ∼ = (1_r‘( Frac ‘ℤ_ring)))
254	5, 253	ax-mp 5	. . . . . . 7 ⊢ [⟨1, 1⟩] ∼ = (1_r‘( Frac ‘ℤ_ring))
255	179, 254	ringidval 20118	. . . . . 6 ⊢ [⟨1, 1⟩] ∼ = (0_g‘(mulGrp‘( Frac ‘ℤ_ring)))
256	240, 241, 245, 247, 249, 255	ismhm 18710	. . . . 5 ⊢ (𝐹 ∈ ((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 711	. . . 4 ⊢ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring)))
258	175, 257	pm3.2i 470	. . 3 ⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring))))
259	176, 179	isrhm 20414	. . 3 ⊢ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ↔ ((𝑄 ∈ Ring ∧ ( Frac ‘ℤ_ring) ∈ Ring) ∧ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring))))))
260	11, 258, 259	mpbir2an 711	. 2 ⊢ 𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring))
261	46	rgen 3053	. . . 4 ⊢ ∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring))
262	117	zcnd 12597	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263	122	zcnd 12597	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
264	21	adantr 480	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265	155	adantl 481	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266	262, 88, 263, 91, 264, 265	divmuleqd 11963	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267	153, 39	eleqtrdi 2846	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤ_ring))
268	157, 39	eleqtrdi 2846	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤ_ring))
269	28, 30, 114, 71, 117, 122, 267, 268	fracerl 33388	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
270	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
271	77, 270	erth 8689	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
272	266, 269, 271	3bitr2rd 308	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ↔ ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝))))
273	272	biimpa 476	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)))
274		qeqnumdivden 16673	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275	274	ad2antrr 726	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276		qeqnumdivden 16673	. . . . . . . 8 ⊢ (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277	276	ad2antlr 727	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278	273, 275, 277	3eqtr4d 2781	. . . . . 6 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = 𝑝)
279	278	ex 412	. . . . 5 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝))
280	279	rgen2 3176	. . . 4 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)
281	17, 56	f1mpt 7207	. . . 4 ⊢ (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)))
282	261, 280, 281	mpbir2an 711	. . 3 ⊢ 𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring))
283		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284		fveq2 6834	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285	283, 284	opeq12d 4837	. . . . . . . . 9 ⊢ (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286	285	eceq1d 8675	. . . . . . . 8 ⊢ (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
287	286	eqeq2d 2747	. . . . . . 7 ⊢ (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ↔ 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ ))
288		simpllr 775	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℤ)
289	223, 288	sselid 3931	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℚ)
290		simplr 768	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ (ℤ ∖ {0}))
291	290	eldifad 3913	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℤ)
292	223, 291	sselid 3931	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℚ)
293		eldifsni 4746	. . . . . . . . 9 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294	290, 293	syl 17	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ≠ 0)
295		qdivcl 12883	. . . . . . . 8 ⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296	289, 292, 294, 295	syl3anc 1373	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → (𝑎 / 𝑏) ∈ ℚ)
297		simpr 484	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑧 = [⟨𝑎, 𝑏⟩] ∼ )
298	146	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ℤ_ring ∈ CRing)
299	149	a1i 11	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
300	28, 29, 69, 30, 31, 32, 24, 298, 299	erler 33347	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∼ Er (ℤ × (ℤ ∖ {0})))
301		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302	301	zcnd 12597	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303		eldifi 4083	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304	303	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305	304	zcnd 12597	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306	293	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307	302, 305, 306	divcld 11917	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308	223, 301	sselid 3931	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309	223, 304	sselid 3931	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310	308, 309, 306, 295	syl3anc 1373	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311		qdencl 16668	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312	310, 311	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313	312	nncnd 12161	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314	307, 313, 305	mul32d 11343	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315		qmuldeneqnum 16674	. . . . . . . . . . . . . 14 ⊢ ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316	310, 315	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317	316	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318	302, 305, 306	divcan1d 11918	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319	318	oveq1d 7373	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320	314, 317, 319	3eqtr3rd 2780	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤ_ring ∈ CRing)
322		qnumcl 16667	. . . . . . . . . . . . 13 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323	310, 322	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325	324, 39	eleqtrdi 2846	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤ_ring))
326	312	nnzd 12514	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327	312	nnne0d 12195	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328	326, 327	eldifsnd 4743	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329	328, 39	eleqtrdi 2846	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤ_ring))
330	28, 30, 114, 321, 301, 323, 325, 329	fracerl 33388	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩ ↔ (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏)))
331	320, 330	mpbird 257	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
332	331	ad4ant23 753	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
333	300, 332	erthi 8691	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → [⟨𝑎, 𝑏⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
334	297, 333	eqtrd 2771	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
335	287, 296, 334	rspcedvdw 3579	. . . . . 6 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
336	45	eleq2i 2828	. . . . . . . 8 ⊢ (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤ_ring)))
337	336	biimpri 228	. . . . . . 7 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
338	337	elrlocbasi 33348	. . . . . 6 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] ∼ )
339	335, 338	r19.29vva 3196	. . . . 5 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
340	339	rgen 3053	. . . 4 ⊢ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼
341	17	fompt 7063	. . . 4 ⊢ (𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ))
342	261, 340, 341	mpbir2an 711	. . 3 ⊢ 𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring))
343		df-f1o 6499	. . 3 ⊢ (𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring)) ↔ (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring))))
344	282, 342, 343	mpbir2an 711	. 2 ⊢ 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring))
345	167, 168	isrim 20427	. 2 ⊢ (𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring)) ↔ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring))))
346	260, 344, 345	mpbir2an 711	1 ⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 395 ∧ w3a 1086 = wceq 1541 ⊤wtru 1542 ∈ wcel 2113 ≠ wne 2932 ∀wral 3051 ∃wrex 3060 Vcvv 3440 ∖ cdif 3898 {csn 4580 ⟨cop 4586 class class class wbr 5098 ↦ cmpt 5179 × cxp 5622 ⟶wf 6488 –1-1→wf1 6489 –onto→wfo 6490 –1-1-onto→wf1o 6491 ‘cfv 6492 (class class class)co 7358 [cec 8633 / cqs 8634 ℂcc 11024 0cc0 11026 1c1 11027 + caddc 11029 · cmul 11031 / cdiv 11794 ℕcn 12145 ℤcz 12488 ℚcq 12861 numercnumer 16660 denomcdenom 16661 Basecbs 17136 ↾_s cress 17157 +_gcplusg 17177 ._rcmulr 17178 Mndcmnd 18659 MndHom cmhm 18706 SubMndcsubmnd 18707 Grpcgrp 18863 -_gcsg 18865 GrpHom cghm 19141 mulGrpcmgp 20075 1_rcur 20116 Ringcrg 20168 CRingccrg 20169 RingHom crh 20405 RingIso crs 20406 NzRingcnzr 20445 RLRegcrlreg 20624 Domncdomn 20625 IDomncidom 20626 DivRingcdr 20662 ℂ_fldccnfld 21309 ℤ_ringczring 21401 ~_RL cerl 33335 RLocal crloc 33336 Frac cfrac 33384

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1796 ax-4 1810 ax-5 1911 ax-6 1968 ax-7 2009 ax-8 2115 ax-9 2123 ax-10 2146 ax-11 2162 ax-12 2184 ax-ext 2708 ax-rep 5224 ax-sep 5241 ax-nul 5251 ax-pow 5310 ax-pr 5377 ax-un 7680 ax-cnex 11082 ax-resscn 11083 ax-1cn 11084 ax-icn 11085 ax-addcl 11086 ax-addrcl 11087 ax-mulcl 11088 ax-mulrcl 11089 ax-mulcom 11090 ax-addass 11091 ax-mulass 11092 ax-distr 11093 ax-i2m1 11094 ax-1ne0 11095 ax-1rid 11096 ax-rnegex 11097 ax-rrecex 11098 ax-cnre 11099 ax-pre-lttri 11100 ax-pre-lttrn 11101 ax-pre-ltadd 11102 ax-pre-mulgt0 11103 ax-pre-sup 11104 ax-addf 11105 ax-mulf 11106

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1544 df-fal 1554 df-ex 1781 df-nf 1785 df-sb 2068 df-mo 2539 df-eu 2569 df-clab 2715 df-cleq 2728 df-clel 2811 df-nfc 2885 df-ne 2933 df-nel 3037 df-ral 3052 df-rex 3061 df-rmo 3350 df-reu 3351 df-rab 3400 df-v 3442 df-sbc 3741 df-csb 3850 df-dif 3904 df-un 3906 df-in 3908 df-ss 3918 df-pss 3921 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4581 df-pr 4583 df-tp 4585 df-op 4587 df-uni 4864 df-iun 4948 df-br 5099 df-opab 5161 df-mpt 5180 df-tr 5206 df-id 5519 df-eprel 5524 df-po 5532 df-so 5533 df-fr 5577 df-we 5579 df-xp 5630 df-rel 5631 df-cnv 5632 df-co 5633 df-dm 5634 df-rn 5635 df-res 5636 df-ima 5637 df-pred 6259 df-ord 6320 df-on 6321 df-lim 6322 df-suc 6323 df-iota 6448 df-fun 6494 df-fn 6495 df-f 6496 df-f1 6497 df-fo 6498 df-f1o 6499 df-fv 6500 df-riota 7315 df-ov 7361 df-oprab 7362 df-mpo 7363 df-om 7809 df-1st 7933 df-2nd 7934 df-tpos 8168 df-frecs 8223 df-wrecs 8254 df-recs 8303 df-rdg 8341 df-1o 8397 df-er 8635 df-ec 8637 df-qs 8641 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-pnf 11168 df-mnf 11169 df-xr 11170 df-ltxr 11171 df-le 11172 df-sub 11366 df-neg 11367 df-div 11795 df-nn 12146 df-2 12208 df-3 12209 df-4 12210 df-5 12211 df-6 12212 df-7 12213 df-8 12214 df-9 12215 df-n0 12402 df-z 12489 df-dec 12608 df-uz 12752 df-q 12862 df-rp 12906 df-fz 13424 df-fl 13712 df-mod 13790 df-seq 13925 df-exp 13985 df-cj 15022 df-re 15023 df-im 15024 df-sqrt 15158 df-abs 15159 df-dvds 16180 df-gcd 16422 df-numer 16662 df-denom 16663 df-struct 17074 df-sets 17091 df-slot 17109 df-ndx 17121 df-base 17137 df-ress 17158 df-plusg 17190 df-mulr 17191 df-starv 17192 df-sca 17193 df-vsca 17194 df-ip 17195 df-tset 17196 df-ple 17197 df-ds 17199 df-unif 17200 df-0g 17361 df-imas 17429 df-qus 17430 df-mgm 18565 df-sgrp 18644 df-mnd 18660 df-mhm 18708 df-submnd 18709 df-grp 18866 df-minusg 18867 df-sbg 18868 df-subg 19053 df-ghm 19142 df-cmn 19711 df-abl 19712 df-mgp 20076 df-rng 20088 df-ur 20117 df-ring 20170 df-cring 20171 df-oppr 20273 df-dvdsr 20293 df-unit 20294 df-invr 20324 df-dvr 20337 df-rhm 20408 df-rim 20409 df-nzr 20446 df-subrng 20479 df-subrg 20503 df-rlreg 20627 df-domn 20628 df-idom 20629 df-drng 20664 df-field 20665 df-cnfld 21310 df-zring 21402 df-erl 33337 df-rloc 33338 df-frac 33385

This theorem is referenced by: (None)

W3C validator