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 34189

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 28004	. . . . 5 ⊢ 𝑄 ∈ DivRing
3		drngring 21038	. . . . 5 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
4	2, 3	ax-mp 5	. . . 4 ⊢ 𝑄 ∈ Ring
5		zringidom 33957	. . . . 5 ⊢ ℤ_ring ∈ IDomn
6		id 23	. . . . . . . 8 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ IDomn)
7	6	fracfld 33974	. . . . . . 7 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Field)
8	7	fldcrngd 21046	. . . . . 6 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ CRing)
9	8	crngringd 20524	. . . . 5 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Ring)
10	5, 9	ax-mp 5	. . . 4 ⊢ ( Frac ‘ℤ_ring) ∈ Ring
11	4, 10	pm3.2i 476	. . 3 ⊢ (𝑄 ∈ Ring ∧ ( Frac ‘ℤ_ring) ∈ Ring)
12		ringgrp 20515	. . . . . . 7 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ Grp)
13	4, 12	ax-mp 5	. . . . . 6 ⊢ 𝑄 ∈ Grp
14		ringgrp 20515	. . . . . . 7 ⊢ (( Frac ‘ℤ_ring) ∈ Ring → ( Frac ‘ℤ_ring) ∈ Grp)
15	10, 14	ax-mp 5	. . . . . 6 ⊢ ( Frac ‘ℤ_ring) ∈ Grp
16	13, 15	pm3.2i 476	. . . . 5 ⊢ (𝑄 ∈ Grp ∧ ( Frac ‘ℤ_ring) ∈ Grp)
17		zringfrac.3	. . . . . . 7 ⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
18		qnumcl 16960	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19		qdencl 16961	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
20	19	nnzd 12759	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
21	19	nnne0d 12428	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
22	20, 21	eldifsnd 4752	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
23	18, 22	opelxpd 5697	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24		zringfrac.2	. . . . . . . . . . 11 ⊢ ∼ = (ℤ_ring ~_RL (ℤ ∖ {0}))
25	24	ovexi 7485	. . . . . . . . . 10 ⊢ ∼ ∈ V
26	25	ecelqsi 8828	. . . . . . . . 9 ⊢ (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
27	23, 26	syl 18	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
28		zringbas 21813	. . . . . . . . . 10 ⊢ ℤ = (Base‘ℤ_ring)
29		zring0 21819	. . . . . . . . . 10 ⊢ 0 = (0_g‘ℤ_ring)
30		zringmulr 21818	. . . . . . . . . 10 ⊢ · = (._r‘ℤ_ring)
31		eqid 2763	. . . . . . . . . 10 ⊢ (-_g‘ℤ_ring) = (-_g‘ℤ_ring)
32		eqid 2763	. . . . . . . . . 10 ⊢ (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33		fracval 33970	. . . . . . . . . . 11 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
34	6	idomdomd 21028	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ Domn)
35	5, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℤ_ring ∈ Domn
36		eqid 2763	. . . . . . . . . . . . . . 15 ⊢ (RLReg‘ℤ_ring) = (RLReg‘ℤ_ring)
37	28, 36, 29	isdomn6 21016	. . . . . . . . . . . . . 14 ⊢ (ℤ_ring ∈ Domn ↔ (ℤ_ring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤ_ring)))
38	35, 37	mpbi 233	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤ_ring))
39	38	simpri 491	. . . . . . . . . . . 12 ⊢ (ℤ ∖ {0}) = (RLReg‘ℤ_ring)
40	39	oveq2i 7462	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
41	33, 40	eqtr4i 2789	. . . . . . . . . 10 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (ℤ ∖ {0}))
42	5	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℤ_ring ∈ IDomn)
43		difssd 4076	. . . . . . . . . 10 ⊢ (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
44	28, 29, 30, 31, 32, 41, 24, 42, 43	rlocbas 33928	. . . . . . . . 9 ⊢ (⊤ → ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring)))
45	44	mptru 1577	. . . . . . . 8 ⊢ ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring))
46	27, 45	eleqtrdi 2874	. . . . . . 7 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)))
47	17, 46	fmpti 7144	. . . . . 6 ⊢ 𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring))
48		ecexg 8759	. . . . . . . . . . . 12 ⊢ ( ∼ ∈ V → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V)
49	25, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V
50	17	fvmpt2 7036	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
51	49, 50	mpan2 704	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
52	51	adantr 486	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
53		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
55	53, 54	opeq12d 4853	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
56	55	eceq1d 8796	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
57	56, 17, 27	fvmpt3 7029	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℚ → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
58	57	adantl 487	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
59	52, 58	oveq12d 7469	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
60	41	fveq2i 6919	. . . . . . . . . 10 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
61	60	oveqi 7464	. . . . . . . . 9 ⊢ ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝))
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)))
63		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
65	63, 64	opeq12d 4853	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
66	65	eceq1d 8796	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
67	66	cbvmptv 5215	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
68	17, 67	eqtri 2786	. . . . . . . . 9 ⊢ 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
69		zring1 21820	. . . . . . . . . . . . 13 ⊢ 1 = (1_r‘ℤ_ring)
70	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ IDomn)
71	70	idomcringd 21029	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ CRing)
72	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ Domn)
73		eqid 2763	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘ℤ_ring) = (mulGrp‘ℤ_ring)
74	28, 29, 73	isdomn3 21017	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ Domn ↔ (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))))
75	72, 74	sylib 221	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))))
76	75	simprd 501	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
77	28, 29, 69, 30, 31, 32, 24, 71, 76	erler 33925	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ∼ Er (ℤ × (ℤ ∖ {0})))
78		qcn 13130	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
79	78	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80		qcn 13130	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
81	80	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
82	79, 81	addcld 11367	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83		qaddcl 13133	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84		qdencl 16961	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
85	83, 84	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
86	85	nncnd 12391	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
87	19	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
88	87	nncnd 12391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89		qdencl 16961	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
90	89	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
91	90	nncnd 12391	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
92	88, 91	mulcld 11368	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
93	82, 86, 92	mul32d 11559	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94		qmuldeneqnum 16967	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
95	83, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
96	95	oveq1d 7466	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
97	79, 88, 91	mulassd 11371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98		qmuldeneqnum 16967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
99	98	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
100	99	oveq1d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
101	97, 100	eqtr3d 2800	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
102	81, 91, 88	mulassd 11371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103		qmuldeneqnum 16967	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104	103	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105	104	oveq1d 7466	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
106	91, 88	mulcomd 11369	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107	106	oveq2d 7467	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108	102, 105, 107	3eqtr3rd 2807	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109	101, 108	oveq12d 7469	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
110	79, 92, 81, 109	joinlmuladdmuld 11375	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111	110	oveq1d 7466	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
112	93, 96, 111	3eqtr3d 2806	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
113	39	oveq2i 7462	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ~_RL (ℤ ∖ {0})) = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
114	24, 113	eqtri 2786	. . . . . . . . . . . . . 14 ⊢ ∼ = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
115		qnumcl 16960	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
116	83, 115	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
117	18	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
118	89	nnzd 12759	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119	118	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120	117, 119	zmulcld 12849	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121		qnumcl 16960	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122	121	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
123	20	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124	122, 123	zmulcld 12849	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125	120, 124	zaddcld 12847	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
126	85	nnzd 12759	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
127	85	nnne0d 12428	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128	126, 127	eldifsnd 4752	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129	128, 39	eleqtrdi 2874	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤ_ring))
130	123, 119	zmulcld 12849	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
131	87, 90	nnmulcld 12431	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132	131	nnne0d 12428	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133	130, 132	eldifsnd 4752	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134	133, 39	eleqtrdi 2874	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤ_ring))
135	28, 30, 114, 71, 116, 125, 129, 134	fracerl 33972	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ∼ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩ ↔ ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝)))))
136	112, 135	mpbird 260	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ∼ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩)
137	77, 136	erthi 8812	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
138	137	adantr 486	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
139		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140		fveq2 6916	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141	139, 140	opeq12d 4853	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142	141	adantl 487	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143	142	eceq1d 8796	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ )
144		zringplusg 21814	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
145		eqid 2763	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (ℤ ∖ {0}))
146		zringcrng 21808	. . . . . . . . . . . 12 ⊢ ℤ_ring ∈ CRing
147	146	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ℤ_ring ∈ CRing)
148	35, 74	mpbi 233	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
149	148	simpri 491	. . . . . . . . . . . 12 ⊢ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))
150	149	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
151	117	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑞) ∈ ℤ)
152	122	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑝) ∈ ℤ)
153	22	adantr 486	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
154	153	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
155	89	nnne0d 12428	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156	118, 155	eldifsnd 4752	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157	156	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158	157	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159		eqid 2763	. . . . . . . . . . 11 ⊢ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
160	28, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159	rlocaddval 33929	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
161	138, 143, 160	3eqtr4d 2808	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
162		ovexd 7486	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) ∈ V)
163	68, 161, 83, 162	fvmptd2 7033	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
164	59, 62, 163	3eqtr4rd 2809	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
165	164	rgen2 3206	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
166	47, 165	pm3.2i 476	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
167	1	qrngbas 28003	. . . . . 6 ⊢ ℚ = (Base‘𝑄)
168		eqid 2763	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘( Frac ‘ℤ_ring))
169		qex 13128	. . . . . . 7 ⊢ ℚ ∈ V
170		cnfldadd 21735	. . . . . . . 8 ⊢ + = (+_g‘ℂ_fld)
171	1, 170	ressplusg 17508	. . . . . . 7 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
172	169, 171	ax-mp 5	. . . . . 6 ⊢ + = (+_g‘𝑄)
173		eqid 2763	. . . . . 6 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘( Frac ‘ℤ_ring))
174	167, 168, 172, 173	isghm 19480	. . . . 5 ⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ↔ ((𝑄 ∈ Grp ∧ ( Frac ‘ℤ_ring) ∈ Grp) ∧ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))))
175	16, 166, 174	mpbir2an 724	. . . 4 ⊢ 𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring))
176		eqid 2763	. . . . . . . 8 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
177	176	ringmgp 20516	. . . . . . 7 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
178	4, 177	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘𝑄) ∈ Mnd
179		eqid 2763	. . . . . . . 8 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) = (mulGrp‘( Frac ‘ℤ_ring))
180	179	ringmgp 20516	. . . . . . 7 ⊢ (( Frac ‘ℤ_ring) ∈ Ring → (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd)
181	10, 180	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd
182	178, 181	pm3.2i 476	. . . . 5 ⊢ ((mulGrp‘𝑄) ∈ Mnd ∧ (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd)
183		eqid 2763	. . . . . . . . . 10 ⊢ (._r‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))
184	28, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183	rlocmulval 33930	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
185	79, 81	mulcld 11368	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186		qmulcl 13135	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187		qdencl 16961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188	186, 187	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189	188	nncnd 12391	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190	185, 189, 92	mul32d 11559	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
191	79, 81, 88, 91	mul4d 11561	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192	191	oveq1d 7466	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193	190, 192	eqtrd 2798	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194		qmuldeneqnum 16967	. . . . . . . . . . . . . 14 ⊢ ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195	186, 194	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196	195	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
197	99, 104	oveq12d 7469	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198	197	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199	193, 196, 198	3eqtr3rd 2807	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200	117, 122	zmulcld 12849	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201		qnumcl 16960	. . . . . . . . . . . . 13 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202	186, 201	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203	188	nnzd 12759	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204	188	nnne0d 12428	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205	203, 204	eldifsnd 4752	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206	205, 39	eleqtrdi 2874	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤ_ring))
207	28, 30, 114, 71, 200, 202, 134, 206	fracerl 33972	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ∼ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩ ↔ (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))))
208	199, 207	mpbird 260	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ∼ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
209	77, 208	erthi 8812	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
210	184, 209	eqtrd 2798	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
211	41	fveq2i 6919	. . . . . . . . . 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 7472	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
214		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216	214, 215	opeq12d 4853	. . . . . . . . . 10 ⊢ (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217	216	eceq1d 8796	. . . . . . . . 9 ⊢ (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
218		ecexg 8759	. . . . . . . . . 10 ⊢ ( ∼ ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
219	25, 218	mp1i 14	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
220	68, 217, 186, 219	fvmptd3 7048	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
221	210, 213, 220	3eqtr4rd 2809	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
222	221	rgen2 3206	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
223		zssq 13123	. . . . . . . 8 ⊢ ℤ ⊆ ℚ
224		1z 12766	. . . . . . . 8 ⊢ 1 ∈ ℤ
225	223, 224	sselii 3910	. . . . . . 7 ⊢ 1 ∈ ℚ
226		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227		1zzd 12767	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ IDomn → 1 ∈ ℤ)
228	227	znumd 33500	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (numer‘1) = 1)
229	5, 228	ax-mp 5	. . . . . . . . . . 11 ⊢ (numer‘1) = 1
230	226, 229	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (numer‘𝑞) = 1)
231		fveq2 6916	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232	227	zdend 33501	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (denom‘1) = 1)
233	5, 232	ax-mp 5	. . . . . . . . . . 11 ⊢ (denom‘1) = 1
234	231, 233	eqtrdi 2814	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (denom‘𝑞) = 1)
235	230, 234	opeq12d 4853	. . . . . . . . 9 ⊢ (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236	235	eceq1d 8796	. . . . . . . 8 ⊢ (𝑞 = 1 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨1, 1⟩] ∼ )
237	236, 17, 49	fvmpt3i 7030	. . . . . . 7 ⊢ (1 ∈ ℚ → (𝐹‘1) = [⟨1, 1⟩] ∼ )
238	225, 237	ax-mp 5	. . . . . 6 ⊢ (𝐹‘1) = [⟨1, 1⟩] ∼
239	47, 222, 238	3pm3.2i 1358	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] ∼ )
240	176, 167	mgpbas 20416	. . . . . 6 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
241	179, 168	mgpbas 20416	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘(mulGrp‘( Frac ‘ℤ_ring)))
242		cnfldmul 21737	. . . . . . . . 9 ⊢ · = (._r‘ℂ_fld)
243	1, 242	ressmulr 17524	. . . . . . . 8 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
244	169, 243	ax-mp 5	. . . . . . 7 ⊢ · = (._r‘𝑄)
245	176, 244	mgpplusg 20415	. . . . . 6 ⊢ · = (+_g‘(mulGrp‘𝑄))
246		eqid 2763	. . . . . . 7 ⊢ (._r‘( Frac ‘ℤ_ring)) = (._r‘( Frac ‘ℤ_ring))
247	179, 246	mgpplusg 20415	. . . . . 6 ⊢ (._r‘( Frac ‘ℤ_ring)) = (+_g‘(mulGrp‘( Frac ‘ℤ_ring)))
248	1	qrng1 28006	. . . . . . 7 ⊢ 1 = (1_r‘𝑄)
249	176, 248	ringidval 20460	. . . . . 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 2763	. . . . . . . . 9 ⊢ [⟨1, 1⟩] ∼ = [⟨1, 1⟩] ∼
253	29, 69, 41, 24, 250, 251, 252	rloc1r 33933	. . . . . . . 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 20460	. . . . . 6 ⊢ [⟨1, 1⟩] ∼ = (0_g‘(mulGrp‘( Frac ‘ℤ_ring)))
256	240, 241, 245, 247, 249, 255	ismhm 19030	. . . . 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 724	. . . 4 ⊢ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring)))
258	175, 257	pm3.2i 476	. . 3 ⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring))))
259	176, 179	isrhm 20760	. . 3 ⊢ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ↔ ((𝑄 ∈ Ring ∧ ( Frac ‘ℤ_ring) ∈ Ring) ∧ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring))))))
260	11, 258, 259	mpbir2an 724	. 2 ⊢ 𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring))
261	46	rgen 3082	. . . 4 ⊢ ∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring))
262	117	zcnd 12844	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263	122	zcnd 12844	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
264	21	adantr 486	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265	155	adantl 487	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266	262, 88, 263, 91, 264, 265	divmuleqd 12179	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267	153, 39	eleqtrdi 2874	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤ_ring))
268	157, 39	eleqtrdi 2874	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤ_ring))
269	28, 30, 114, 71, 117, 122, 267, 268	fracerl 33972	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
270	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
271	77, 270	erth 8810	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
272	266, 269, 271	3bitr2rd 311	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ↔ ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝))))
273	272	biimpa 482	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)))
274		qeqnumdivden 16966	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275	274	ad2antrr 739	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276		qeqnumdivden 16966	. . . . . . . 8 ⊢ (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277	276	ad2antlr 740	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278	273, 275, 277	3eqtr4d 2808	. . . . . 6 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = 𝑝)
279	278	ex 418	. . . . 5 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝))
280	279	rgen2 3206	. . . 4 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)
281	17, 56	f1mpt 7296	. . . 4 ⊢ (𝐹:ℚ⟶1-1(Base‘( Frac ‘ℤ_ring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)))
282	261, 280, 281	mpbir2an 724	. . 3 ⊢ 𝐹:ℚ⟶1-1(Base‘( Frac ‘ℤ_ring))
283		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284		fveq2 6916	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285	283, 284	opeq12d 4853	. . . . . . . . 9 ⊢ (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286	285	eceq1d 8796	. . . . . . . 8 ⊢ (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
287	286	eqeq2d 2774	. . . . . . 7 ⊢ (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ↔ 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ ))
288		simpllr 788	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℤ)
289	223, 288	sselid 3911	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℚ)
290		simplr 781	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ (ℤ ∖ {0}))
291	290	eldifad 4054	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℤ)
292	223, 291	sselid 3911	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℚ)
293		eldifsni 4755	. . . . . . . . 9 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294	290, 293	syl 18	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ≠ 0)
295		qdivcl 13138	. . . . . . . 8 ⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296	289, 292, 294, 295	syl3anc 1399	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → (𝑎 / 𝑏) ∈ ℚ)
297		simpr 490	. . . . . . . 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 33925	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∼ Er (ℤ × (ℤ ∖ {0})))
301		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302	301	zcnd 12844	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303		eldifi 4070	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304	303	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305	304	zcnd 12844	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306	293	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307	302, 305, 306	divcld 12133	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308	223, 301	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309	223, 304	sselid 3911	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310	308, 309, 306, 295	syl3anc 1399	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311		qdencl 16961	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312	310, 311	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313	312	nncnd 12391	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314	307, 313, 305	mul32d 11559	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315		qmuldeneqnum 16967	. . . . . . . . . . . . . 14 ⊢ ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316	310, 315	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317	316	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318	302, 305, 306	divcan1d 12134	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319	318	oveq1d 7466	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320	314, 317, 319	3eqtr3rd 2807	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤ_ring ∈ CRing)
322		qnumcl 16960	. . . . . . . . . . . . 13 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323	310, 322	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325	324, 39	eleqtrdi 2874	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤ_ring))
326	312	nnzd 12759	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327	312	nnne0d 12428	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328	326, 327	eldifsnd 4752	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329	328, 39	eleqtrdi 2874	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤ_ring))
330	28, 30, 114, 321, 301, 323, 325, 329	fracerl 33972	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩ ↔ (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏)))
331	320, 330	mpbird 260	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
332	331	ad4ant23 766	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
333	300, 332	erthi 8812	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → [⟨𝑎, 𝑏⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
334	297, 333	eqtrd 2798	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
335	287, 296, 334	rspcedvdw 3583	. . . . . 6 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
336	45	eleq2i 2856	. . . . . . . 8 ⊢ (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤ_ring)))
337	336	biimpri 231	. . . . . . 7 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
338	337	elrlocbasi 33927	. . . . . 6 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] ∼ )
339	335, 338	r19.29vva 3226	. . . . 5 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
340	339	rgen 3082	. . . 4 ⊢ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼
341	17	fompt 7150	. . . 4 ⊢ (𝐹:ℚ⟶onto(Base‘( Frac ‘ℤ_ring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ))
342	261, 340, 341	mpbir2an 724	. . 3 ⊢ 𝐹:ℚ⟶onto(Base‘( Frac ‘ℤ_ring))
343		df-f1o 6573	. . 3 ⊢ (𝐹:ℚ⟶1-1onto(Base‘( Frac ‘ℤ_ring)) ↔ (𝐹:ℚ⟶1-1(Base‘( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ⟶onto(Base‘( Frac ‘ℤ_ring))))
344	282, 342, 343	mpbir2an 724	. 2 ⊢ 𝐹:ℚ⟶1-1onto(Base‘( Frac ‘ℤ_ring))
345	167, 168	isrim 20779	. 2 ⊢ (𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring)) ↔ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ⟶1-1onto(Base‘( Frac ‘ℤ_ring))))
346	260, 344, 345	mpbir2an 724	1 ⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring))

Colors of variables: wff setvar class

This proof depends on syntax axioms: → wi 4 ∧ wa 401 ∧ w3a 1103 = wceq 1570 ⊤wtru 1571 ∈ wcel 2147 ≠ wne 2959 ∀wral 3080 ∃wrex 3090 Vcvv 3454 ∖ cdif 4048 {csn 4588 ⟨cop 4840 class class class wbr 5108 ↦ cmpt 5192 × cxp 5656 ⟶wf 6562 ⟶1-1wf1 6563 ⟶ontowfo 6564 ⟶1-1ontowf1o 6565 ‘cfv 6566 (class class class)co 7451 [cec 8753 / cqs 8754 ℂcc 11237 0cc0 11239 1c1 11240 + caddc 11242 · cmul 11244 / cdiv 12013 ℕcn 12375 ℤcz 12733 ℚcq 13115 numercnumer 16953 denomcdenom 16954 Basecbs 17431 ↾_s cress 17452 +_gcplusg 17472 ._rcmulr 17473 Mndcmnd 18973 MndHom cmhm 19026 SubMndcsubmnd 19027 Grpcgrp 19194 -_gcsg 19196 GrpHom cghm 19477 mulGrpcmgp 20411 1_rcur 20458 Ringcrg 20510 CRingccrg 20511 RingHom crh 20750 RingIso crs 20751 NzRingcnzr 20813 RLRegcrlreg 20994 Domncdomn 20995 IDomncidom 20996 DivRingcdr 21031 ℂ_fldccnfld 21729 ℤ_ringczring 21806 ~_RL cerl 33913 RLocal crloc 33914 Frac cfrac 33968

This proof depends on axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1828 ax-4 1842 ax-5 1945 ax-6 2002 ax-7 2043 ax-8 2149 ax-9 2157 ax-10 2180 ax-11 2197 ax-12 2216 ax-ext 2735 ax-rep 5238 ax-sep 5255 ax-nul 5266 ax-pow 5334 ax-pr 5398 ax-un 7783 ax-cnex 11295 ax-resscn 11296 ax-1cn 11297 ax-icn 11298 ax-addcl 11299 ax-addrcl 11300 ax-mulcl 11301 ax-mulrcl 11302 ax-mulcom 11303 ax-addass 11304 ax-mulass 11305 ax-distr 11306 ax-i2m1 11307 ax-1ne0 11308 ax-1rid 11309 ax-rnegex 11310 ax-rrecex 11311 ax-cnre 11312 ax-pre-lttri 11313 ax-pre-lttrn 11314 ax-pre-ltadd 11315 ax-pre-mulgt0 11316 ax-pre-sup 11317 ax-addf 11318 ax-mulf 11319

This proof depends on definitions: df-bi 210 df-an 402 df-or 862 df-3or 1104 df-3an 1105 df-tru 1573 df-fal 1583 df-ex 1813 df-nf 1817 df-sb 2102 df-mo 2567 df-eu 2597 df-clab 2742 df-cleq 2755 df-clel 2839 df-nfc 2913 df-ne 2960 df-nel 3066 df-ral 3081 df-rex 3091 df-rmo 3369 df-reu 3370 df-rab 3417 df-v 3456 df-sbc 3743 df-csb 3852 df-ss 3901 df-pss 4017 df-dif 4050 df-in 4094 df-un 4154 df-nul 4282 df-if 4486 df-pw 4562 df-sn 4589 df-pr 4591 df-tp 4593 df-op 4841 df-uni 4873 df-iun 4958 df-br 5109 df-opab 5174 df-mpt 5193 df-tr 5219 df-id 5553 df-eprel 5558 df-po 5566 df-so 5567 df-fr 5611 df-we 5613 df-xp 5664 df-rel 5665 df-cnv 5666 df-co 5667 df-dm 5668 df-rn 5669 df-res 5670 df-ima 5671 df-pred 6330 df-ord 6391 df-on 6392 df-lim 6393 df-suc 6394 df-iota 6520 df-fun 6568 df-fn 6569 df-f 6570 df-f1 6571 df-fo 6572 df-f1o 6573 df-fv 6574 df-riota 7408 df-ov 7454 df-oprab 7455 df-mpo 7456 df-om 7912 df-1st 8035 df-2nd 8036 df-tpos 8281 df-frecs 8337 df-wrecs 8368 df-recs 8417 df-rdg 8456 df-1o 8514 df-er 8755 df-ec 8757 df-qs 8761 df-map 8887 df-en 9012 df-dom 9013 df-sdom 9014 df-fin 9015 df-sup 9471 df-inf 9472 df-pnf 11384 df-mnf 11385 df-xr 11386 df-ltxr 11387 df-le 11388 df-sub 11582 df-neg 11583 df-div 12014 df-nn 12376 df-2 12445 df-3 12446 df-4 12447 df-5 12448 df-6 12449 df-7 12450 df-8 12451 df-9 12452 df-n0 12647 df-z 12734 df-dec 12855 df-uz 13006 df-q 13116 df-rp 13161 df-fz 13680 df-fl 13972 df-mod 14050 df-seq 14185 df-exp 14245 df-cj 15309 df-re 15310 df-im 15311 df-sqrt 15445 df-abs 15446 df-dvds 16467 df-gcd 16709 df-numer 16955 df-denom 16956 df-struct 17369 df-sets 17386 df-slot 17404 df-ndx 17416 df-base 17432 df-ress 17453 df-plusg 17486 df-mulr 17487 df-starv 17488 df-sca 17489 df-vsca 17490 df-ip 17491 df-tset 17492 df-ple 17493 df-ds 17495 df-unif 17496 df-euf 17499 df-0g 17662 df-imas 17730 df-qus 17731 df-mgm 18866 df-sgrp 18958 df-mnd 18974 df-mhm 19028 df-submnd 19029 df-grp 19197 df-minusg 19198 df-sbg 19199 df-subg 19383 df-ghm 19478 df-cmn 20047 df-abl 20048 df-mgp 20412 df-rng 20426 df-ur 20459 df-ring 20512 df-cring 20513 df-oppr 20618 df-dvdsr 20638 df-unit 20639 df-invr 20669 df-dvr 20682 df-rhm 20753 df-rim 20754 df-nzr 20814 df-subrng 20849 df-subrg 20873 df-rlreg 20997 df-domn 20998 df-idom 20999 df-drng 21033 df-field 21034 df-cnfld 21730 df-zring 21807 df-erl 33915 df-rloc 33916 df-frac 33969

This theorem is used by: (None)

W3C validator