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 33637

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 27601	. . . . 5 ⊢ 𝑄 ∈ DivRing
3		drngring 20708	. . . . 5 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
4	2, 3	ax-mp 5	. . . 4 ⊢ 𝑄 ∈ Ring
5		zringidom 33634	. . . . 5 ⊢ ℤ_ring ∈ IDomn
6		id 22	. . . . . . . 8 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ IDomn)
7	6	fracfld 33392	. . . . . . 7 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Field)
8	7	fldcrngd 20714	. . . . . 6 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ CRing)
9	8	crngringd 20218	. . . . 5 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Ring)
10	5, 9	ax-mp 5	. . . 4 ⊢ ( Frac ‘ℤ_ring) ∈ Ring
11	4, 10	pm3.2i 471	. . 3 ⊢ (𝑄 ∈ Ring ∧ ( Frac ‘ℤ_ring) ∈ Ring)
12		ringgrp 20210	. . . . . . 7 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ Grp)
13	4, 12	ax-mp 5	. . . . . 6 ⊢ 𝑄 ∈ Grp
14		ringgrp 20210	. . . . . . 7 ⊢ (( Frac ‘ℤ_ring) ∈ Ring → ( Frac ‘ℤ_ring) ∈ Grp)
15	10, 14	ax-mp 5	. . . . . 6 ⊢ ( Frac ‘ℤ_ring) ∈ Grp
16	13, 15	pm3.2i 471	. . . . 5 ⊢ (𝑄 ∈ Grp ∧ ( Frac ‘ℤ_ring) ∈ Grp)
17		zringfrac.3	. . . . . . 7 ⊢ 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
18		qnumcl 16701	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19		qdencl 16702	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
20	19	nnzd 12541	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
21	19	nnne0d 12218	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
22	20, 21	eldifsnd 4720	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
23	18, 22	opelxpd 5657	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24		zringfrac.2	. . . . . . . . . . 11 ⊢ ∼ = (ℤ_ring ~_RL (ℤ ∖ {0}))
25	24	ovexi 7390	. . . . . . . . . 10 ⊢ ∼ ∈ V
26	25	ecelqsi 8706	. . . . . . . . 9 ⊢ (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
27	23, 26	syl 17	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
28		zringbas 21428	. . . . . . . . . 10 ⊢ ℤ = (Base‘ℤ_ring)
29		zring0 21433	. . . . . . . . . 10 ⊢ 0 = (0_g‘ℤ_ring)
30		zringmulr 21432	. . . . . . . . . 10 ⊢ · = (._r‘ℤ_ring)
31		eqid 2739	. . . . . . . . . 10 ⊢ (-_g‘ℤ_ring) = (-_g‘ℤ_ring)
32		eqid 2739	. . . . . . . . . 10 ⊢ (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33		fracval 33388	. . . . . . . . . . 11 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
34	6	idomdomd 20698	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ Domn)
35	5, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℤ_ring ∈ Domn
36		eqid 2739	. . . . . . . . . . . . . . 15 ⊢ (RLReg‘ℤ_ring) = (RLReg‘ℤ_ring)
37	28, 36, 29	isdomn6 20686	. . . . . . . . . . . . . 14 ⊢ (ℤ_ring ∈ Domn ↔ (ℤ_ring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤ_ring)))
38	35, 37	mpbi 231	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤ_ring))
39	38	simpri 486	. . . . . . . . . . . 12 ⊢ (ℤ ∖ {0}) = (RLReg‘ℤ_ring)
40	39	oveq2i 7367	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
41	33, 40	eqtr4i 2765	. . . . . . . . . 10 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (ℤ ∖ {0}))
42	5	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℤ_ring ∈ IDomn)
43		difssd 4067	. . . . . . . . . 10 ⊢ (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
44	28, 29, 30, 31, 32, 41, 24, 42, 43	rlocbas 33348	. . . . . . . . 9 ⊢ (⊤ → ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring)))
45	44	mptru 1554	. . . . . . . 8 ⊢ ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring))
46	27, 45	eleqtrdi 2849	. . . . . . 7 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)))
47	17, 46	fmpti 7053	. . . . . 6 ⊢ 𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring))
48		ecexg 8637	. . . . . . . . . . . 12 ⊢ ( ∼ ∈ V → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V)
49	25, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V
50	17	fvmpt2 6947	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
51	49, 50	mpan2 697	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
52	51	adantr 481	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
53		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
55	53, 54	opeq12d 4812	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
56	55	eceq1d 8674	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
57	56, 17, 27	fvmpt3 6940	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℚ → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
58	57	adantl 482	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
59	52, 58	oveq12d 7374	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
60	41	fveq2i 6830	. . . . . . . . . 10 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
61	60	oveqi 7369	. . . . . . . . 9 ⊢ ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝))
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)))
63		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
65	63, 64	opeq12d 4812	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
66	65	eceq1d 8674	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
67	66	cbvmptv 5176	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
68	17, 67	eqtri 2762	. . . . . . . . 9 ⊢ 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
69		zring1 21434	. . . . . . . . . . . . 13 ⊢ 1 = (1_r‘ℤ_ring)
70	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ IDomn)
71	70	idomcringd 20699	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ CRing)
72	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ Domn)
73		eqid 2739	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘ℤ_ring) = (mulGrp‘ℤ_ring)
74	28, 29, 73	isdomn3 20687	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ Domn ↔ (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))))
75	72, 74	sylib 219	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))))
76	75	simprd 496	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
77	28, 29, 69, 30, 31, 32, 24, 71, 76	erler 33346	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ∼ Er (ℤ × (ℤ ∖ {0})))
78		qcn 12904	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
79	78	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80		qcn 12904	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
81	80	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
82	79, 81	addcld 11155	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83		qaddcl 12906	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84		qdencl 16702	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
85	83, 84	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
86	85	nncnd 12181	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
87	19	adantr 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
88	87	nncnd 12181	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89		qdencl 16702	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
90	89	adantl 482	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
91	90	nncnd 12181	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
92	88, 91	mulcld 11156	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
93	82, 86, 92	mul32d 11347	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94		qmuldeneqnum 16708	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
95	83, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
96	95	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
97	79, 88, 91	mulassd 11159	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98		qmuldeneqnum 16708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
99	98	adantr 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
100	99	oveq1d 7371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
101	97, 100	eqtr3d 2776	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
102	81, 91, 88	mulassd 11159	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103		qmuldeneqnum 16708	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104	103	adantl 482	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105	104	oveq1d 7371	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
106	91, 88	mulcomd 11157	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107	106	oveq2d 7372	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108	102, 105, 107	3eqtr3rd 2783	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109	101, 108	oveq12d 7374	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
110	79, 92, 81, 109	joinlmuladdmuld 11163	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111	110	oveq1d 7371	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
112	93, 96, 111	3eqtr3d 2782	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
113	39	oveq2i 7367	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ~_RL (ℤ ∖ {0})) = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
114	24, 113	eqtri 2762	. . . . . . . . . . . . . 14 ⊢ ∼ = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
115		qnumcl 16701	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
116	83, 115	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
117	18	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
118	89	nnzd 12541	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119	118	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120	117, 119	zmulcld 12630	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121		qnumcl 16701	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122	121	adantl 482	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
123	20	adantr 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124	122, 123	zmulcld 12630	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125	120, 124	zaddcld 12628	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
126	85	nnzd 12541	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
127	85	nnne0d 12218	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128	126, 127	eldifsnd 4720	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129	128, 39	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤ_ring))
130	123, 119	zmulcld 12630	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
131	87, 90	nnmulcld 12221	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132	131	nnne0d 12218	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133	130, 132	eldifsnd 4720	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134	133, 39	eleqtrdi 2849	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤ_ring))
135	28, 30, 114, 71, 116, 125, 129, 134	fracerl 33390	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ∼ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩ ↔ ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝)))))
136	112, 135	mpbird 258	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ∼ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩)
137	77, 136	erthi 8690	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
138	137	adantr 481	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
139		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140		fveq2 6827	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141	139, 140	opeq12d 4812	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142	141	adantl 482	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143	142	eceq1d 8674	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ )
144		zringplusg 21429	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
145		eqid 2739	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (ℤ ∖ {0}))
146		zringcrng 21423	. . . . . . . . . . . 12 ⊢ ℤ_ring ∈ CRing
147	146	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ℤ_ring ∈ CRing)
148	35, 74	mpbi 231	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
149	148	simpri 486	. . . . . . . . . . . 12 ⊢ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring))
150	149	a1i 11	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤ_ring)))
151	117	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑞) ∈ ℤ)
152	122	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑝) ∈ ℤ)
153	22	adantr 481	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
154	153	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
155	89	nnne0d 12218	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156	118, 155	eldifsnd 4720	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157	156	adantl 482	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158	157	adantr 481	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159		eqid 2739	. . . . . . . . . . 11 ⊢ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
160	28, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159	rlocaddval 33349	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
161	138, 143, 160	3eqtr4d 2784	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
162		ovexd 7391	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) ∈ V)
163	68, 161, 83, 162	fvmptd2 6944	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
164	59, 62, 163	3eqtr4rd 2785	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
165	164	rgen2 3179	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
166	47, 165	pm3.2i 471	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
167	1	qrngbas 27600	. . . . . 6 ⊢ ℚ = (Base‘𝑄)
168		eqid 2739	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘( Frac ‘ℤ_ring))
169		qex 12902	. . . . . . 7 ⊢ ℚ ∈ V
170		cnfldadd 21353	. . . . . . . 8 ⊢ + = (+_g‘ℂ_fld)
171	1, 170	ressplusg 17245	. . . . . . 7 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
172	169, 171	ax-mp 5	. . . . . 6 ⊢ + = (+_g‘𝑄)
173		eqid 2739	. . . . . 6 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘( Frac ‘ℤ_ring))
174	167, 168, 172, 173	isghm 19181	. . . . 5 ⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ↔ ((𝑄 ∈ Grp ∧ ( Frac ‘ℤ_ring) ∈ Grp) ∧ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))))
175	16, 166, 174	mpbir2an 717	. . . 4 ⊢ 𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring))
176		eqid 2739	. . . . . . . 8 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
177	176	ringmgp 20211	. . . . . . 7 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
178	4, 177	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘𝑄) ∈ Mnd
179		eqid 2739	. . . . . . . 8 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) = (mulGrp‘( Frac ‘ℤ_ring))
180	179	ringmgp 20211	. . . . . . 7 ⊢ (( Frac ‘ℤ_ring) ∈ Ring → (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd)
181	10, 180	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd
182	178, 181	pm3.2i 471	. . . . 5 ⊢ ((mulGrp‘𝑄) ∈ Mnd ∧ (mulGrp‘( Frac ‘ℤ_ring)) ∈ Mnd)
183		eqid 2739	. . . . . . . . . 10 ⊢ (._r‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))
184	28, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183	rlocmulval 33350	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
185	79, 81	mulcld 11156	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186		qmulcl 12908	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187		qdencl 16702	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188	186, 187	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189	188	nncnd 12181	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190	185, 189, 92	mul32d 11347	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
191	79, 81, 88, 91	mul4d 11349	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192	191	oveq1d 7371	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193	190, 192	eqtrd 2774	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194		qmuldeneqnum 16708	. . . . . . . . . . . . . 14 ⊢ ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195	186, 194	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196	195	oveq1d 7371	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
197	99, 104	oveq12d 7374	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198	197	oveq1d 7371	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199	193, 196, 198	3eqtr3rd 2783	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200	117, 122	zmulcld 12630	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201		qnumcl 16701	. . . . . . . . . . . . 13 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202	186, 201	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203	188	nnzd 12541	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204	188	nnne0d 12218	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205	203, 204	eldifsnd 4720	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206	205, 39	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤ_ring))
207	28, 30, 114, 71, 200, 202, 134, 206	fracerl 33390	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ∼ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩ ↔ (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))))
208	199, 207	mpbird 258	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ∼ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
209	77, 208	erthi 8690	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
210	184, 209	eqtrd 2774	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
211	41	fveq2i 6830	. . . . . . . . . 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 7377	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
214		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216	214, 215	opeq12d 4812	. . . . . . . . . 10 ⊢ (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217	216	eceq1d 8674	. . . . . . . . 9 ⊢ (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
218		ecexg 8637	. . . . . . . . . 10 ⊢ ( ∼ ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
219	25, 218	mp1i 13	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
220	68, 217, 186, 219	fvmptd3 6959	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
221	210, 213, 220	3eqtr4rd 2785	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
222	221	rgen2 3179	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
223		zssq 12897	. . . . . . . 8 ⊢ ℤ ⊆ ℚ
224		1z 12548	. . . . . . . 8 ⊢ 1 ∈ ℤ
225	223, 224	sselii 3912	. . . . . . 7 ⊢ 1 ∈ ℚ
226		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227		1zzd 12549	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ IDomn → 1 ∈ ℤ)
228	227	znumd 32905	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (numer‘1) = 1)
229	5, 228	ax-mp 5	. . . . . . . . . . 11 ⊢ (numer‘1) = 1
230	226, 229	eqtrdi 2790	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (numer‘𝑞) = 1)
231		fveq2 6827	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232	227	zdend 32906	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (denom‘1) = 1)
233	5, 232	ax-mp 5	. . . . . . . . . . 11 ⊢ (denom‘1) = 1
234	231, 233	eqtrdi 2790	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (denom‘𝑞) = 1)
235	230, 234	opeq12d 4812	. . . . . . . . 9 ⊢ (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236	235	eceq1d 8674	. . . . . . . 8 ⊢ (𝑞 = 1 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨1, 1⟩] ∼ )
237	236, 17, 49	fvmpt3i 6941	. . . . . . 7 ⊢ (1 ∈ ℚ → (𝐹‘1) = [⟨1, 1⟩] ∼ )
238	225, 237	ax-mp 5	. . . . . 6 ⊢ (𝐹‘1) = [⟨1, 1⟩] ∼
239	47, 222, 238	3pm3.2i 1346	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] ∼ )
240	176, 167	mgpbas 20117	. . . . . 6 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
241	179, 168	mgpbas 20117	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘(mulGrp‘( Frac ‘ℤ_ring)))
242		cnfldmul 21355	. . . . . . . . 9 ⊢ · = (._r‘ℂ_fld)
243	1, 242	ressmulr 17261	. . . . . . . 8 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
244	169, 243	ax-mp 5	. . . . . . 7 ⊢ · = (._r‘𝑄)
245	176, 244	mgpplusg 20116	. . . . . 6 ⊢ · = (+_g‘(mulGrp‘𝑄))
246		eqid 2739	. . . . . . 7 ⊢ (._r‘( Frac ‘ℤ_ring)) = (._r‘( Frac ‘ℤ_ring))
247	179, 246	mgpplusg 20116	. . . . . 6 ⊢ (._r‘( Frac ‘ℤ_ring)) = (+_g‘(mulGrp‘( Frac ‘ℤ_ring)))
248	1	qrng1 27603	. . . . . . 7 ⊢ 1 = (1_r‘𝑄)
249	176, 248	ringidval 20155	. . . . . 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 2739	. . . . . . . . 9 ⊢ [⟨1, 1⟩] ∼ = [⟨1, 1⟩] ∼
253	29, 69, 41, 24, 250, 251, 252	rloc1r 33353	. . . . . . . 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 20155	. . . . . 6 ⊢ [⟨1, 1⟩] ∼ = (0_g‘(mulGrp‘( Frac ‘ℤ_ring)))
256	240, 241, 245, 247, 249, 255	ismhm 18744	. . . . 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 717	. . . 4 ⊢ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring)))
258	175, 257	pm3.2i 471	. . 3 ⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring))))
259	176, 179	isrhm 20449	. . 3 ⊢ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ↔ ((𝑄 ∈ Ring ∧ ( Frac ‘ℤ_ring) ∈ Ring) ∧ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤ_ring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤ_ring))))))
260	11, 258, 259	mpbir2an 717	. 2 ⊢ 𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring))
261	46	rgen 3055	. . . 4 ⊢ ∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring))
262	117	zcnd 12625	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263	122	zcnd 12625	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
264	21	adantr 481	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265	155	adantl 482	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266	262, 88, 263, 91, 264, 265	divmuleqd 11968	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267	153, 39	eleqtrdi 2849	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤ_ring))
268	157, 39	eleqtrdi 2849	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤ_ring))
269	28, 30, 114, 71, 117, 122, 267, 268	fracerl 33390	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
270	23	adantr 481	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
271	77, 270	erth 8688	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
272	266, 269, 271	3bitr2rd 309	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ↔ ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝))))
273	272	biimpa 477	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)))
274		qeqnumdivden 16707	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275	274	ad2antrr 732	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276		qeqnumdivden 16707	. . . . . . . 8 ⊢ (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277	276	ad2antlr 733	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278	273, 275, 277	3eqtr4d 2784	. . . . . 6 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = 𝑝)
279	278	ex 413	. . . . 5 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝))
280	279	rgen2 3179	. . . 4 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)
281	17, 56	f1mpt 7205	. . . 4 ⊢ (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)))
282	261, 280, 281	mpbir2an 717	. . 3 ⊢ 𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring))
283		fveq2 6827	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284		fveq2 6827	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285	283, 284	opeq12d 4812	. . . . . . . . 9 ⊢ (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286	285	eceq1d 8674	. . . . . . . 8 ⊢ (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
287	286	eqeq2d 2750	. . . . . . 7 ⊢ (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ↔ 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ ))
288		simpllr 781	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℤ)
289	223, 288	sselid 3913	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℚ)
290		simplr 774	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ (ℤ ∖ {0}))
291	290	eldifad 3895	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℤ)
292	223, 291	sselid 3913	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℚ)
293		eldifsni 4723	. . . . . . . . 9 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294	290, 293	syl 17	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ≠ 0)
295		qdivcl 12911	. . . . . . . 8 ⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296	289, 292, 294, 295	syl3anc 1379	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → (𝑎 / 𝑏) ∈ ℚ)
297		simpr 485	. . . . . . . 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 33346	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∼ Er (ℤ × (ℤ ∖ {0})))
301		simpl 483	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302	301	zcnd 12625	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303		eldifi 4061	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304	303	adantl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305	304	zcnd 12625	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306	293	adantl 482	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307	302, 305, 306	divcld 11922	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308	223, 301	sselid 3913	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309	223, 304	sselid 3913	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310	308, 309, 306, 295	syl3anc 1379	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311		qdencl 16702	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312	310, 311	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313	312	nncnd 12181	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314	307, 313, 305	mul32d 11347	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315		qmuldeneqnum 16708	. . . . . . . . . . . . . 14 ⊢ ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316	310, 315	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317	316	oveq1d 7371	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318	302, 305, 306	divcan1d 11923	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319	318	oveq1d 7371	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320	314, 317, 319	3eqtr3rd 2783	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤ_ring ∈ CRing)
322		qnumcl 16701	. . . . . . . . . . . . 13 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323	310, 322	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324		simpr 485	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325	324, 39	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤ_ring))
326	312	nnzd 12541	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327	312	nnne0d 12218	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328	326, 327	eldifsnd 4720	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329	328, 39	eleqtrdi 2849	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤ_ring))
330	28, 30, 114, 321, 301, 323, 325, 329	fracerl 33390	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩ ↔ (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏)))
331	320, 330	mpbird 258	. . . . . . . . . 10 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
332	331	ad4ant23 759	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ⟨𝑎, 𝑏⟩ ∼ ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
333	300, 332	erthi 8690	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → [⟨𝑎, 𝑏⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
334	297, 333	eqtrd 2774	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
335	287, 296, 334	rspcedvdw 3563	. . . . . 6 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
336	45	eleq2i 2831	. . . . . . . 8 ⊢ (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤ_ring)))
337	336	biimpri 229	. . . . . . 7 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
338	337	elrlocbasi 33347	. . . . . 6 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] ∼ )
339	335, 338	r19.29vva 3199	. . . . 5 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
340	339	rgen 3055	. . . 4 ⊢ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼
341	17	fompt 7059	. . . 4 ⊢ (𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ))
342	261, 340, 341	mpbir2an 717	. . 3 ⊢ 𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring))
343		df-f1o 6492	. . 3 ⊢ (𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring)) ↔ (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring))))
344	282, 342, 343	mpbir2an 717	. 2 ⊢ 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring))
345	167, 168	isrim 20463	. 2 ⊢ (𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring)) ↔ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring))))
346	260, 344, 345	mpbir2an 717	1 ⊢ 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ wa 396 ∧ w3a 1092 = wceq 1547 ⊤wtru 1548 ∈ wcel 2119 ≠ wne 2934 ∀wral 3053 ∃wrex 3063 Vcvv 3431 ∖ cdif 3880 {csn 4555 ⟨cop 4561 class class class wbr 5072 ↦ cmpt 5153 × cxp 5616 ⟶wf 6481 –1-1→wf1 6482 –onto→wfo 6483 –1-1-onto→wf1o 6484 ‘cfv 6485 (class class class)co 7356 [cec 8631 / cqs 8632 ℂcc 11027 0cc0 11029 1c1 11030 + caddc 11032 · cmul 11034 / cdiv 11798 ℕcn 12165 ℤcz 12515 ℚcq 12889 numercnumer 16694 denomcdenom 16695 Basecbs 17170 ↾_s cress 17191 +_gcplusg 17211 ._rcmulr 17212 Mndcmnd 18693 MndHom cmhm 18740 SubMndcsubmnd 18741 Grpcgrp 18900 -_gcsg 18902 GrpHom cghm 19178 mulGrpcmgp 20112 1_rcur 20153 Ringcrg 20205 CRingccrg 20206 RingHom crh 20440 RingIso crs 20441 NzRingcnzr 20484 RLRegcrlreg 20663 Domncdomn 20664 IDomncidom 20665 DivRingcdr 20701 ℂ_fldccnfld 21347 ℤ_ringczring 21421 ~_RL cerl 33334 RLocal crloc 33335 Frac cfrac 33386

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1802 ax-4 1816 ax-5 1917 ax-6 1974 ax-7 2015 ax-8 2121 ax-9 2129 ax-10 2152 ax-11 2168 ax-12 2189 ax-ext 2711 ax-rep 5199 ax-sep 5218 ax-nul 5228 ax-pow 5294 ax-pr 5362 ax-un 7678 ax-cnex 11085 ax-resscn 11086 ax-1cn 11087 ax-icn 11088 ax-addcl 11089 ax-addrcl 11090 ax-mulcl 11091 ax-mulrcl 11092 ax-mulcom 11093 ax-addass 11094 ax-mulass 11095 ax-distr 11096 ax-i2m1 11097 ax-1ne0 11098 ax-1rid 11099 ax-rnegex 11100 ax-rrecex 11101 ax-cnre 11102 ax-pre-lttri 11103 ax-pre-lttrn 11104 ax-pre-ltadd 11105 ax-pre-mulgt0 11106 ax-pre-sup 11107 ax-addf 11108 ax-mulf 11109

This theorem depends on definitions: df-bi 208 df-an 397 df-or 854 df-3or 1093 df-3an 1094 df-tru 1550 df-fal 1560 df-ex 1787 df-nf 1791 df-sb 2074 df-mo 2543 df-eu 2573 df-clab 2718 df-cleq 2731 df-clel 2814 df-nfc 2888 df-ne 2935 df-nel 3039 df-ral 3054 df-rex 3064 df-rmo 3344 df-reu 3345 df-rab 3392 df-v 3433 df-sbc 3724 df-csb 3832 df-dif 3886 df-un 3888 df-in 3890 df-ss 3900 df-pss 3903 df-nul 4262 df-if 4455 df-pw 4531 df-sn 4556 df-pr 4558 df-tp 4560 df-op 4562 df-uni 4839 df-iun 4923 df-br 5073 df-opab 5135 df-mpt 5154 df-tr 5180 df-id 5513 df-eprel 5518 df-po 5526 df-so 5527 df-fr 5571 df-we 5573 df-xp 5624 df-rel 5625 df-cnv 5626 df-co 5627 df-dm 5628 df-rn 5629 df-res 5630 df-ima 5631 df-pred 6252 df-ord 6313 df-on 6314 df-lim 6315 df-suc 6316 df-iota 6441 df-fun 6487 df-fn 6488 df-f 6489 df-f1 6490 df-fo 6491 df-f1o 6492 df-fv 6493 df-riota 7313 df-ov 7359 df-oprab 7360 df-mpo 7361 df-om 7807 df-1st 7931 df-2nd 7932 df-tpos 8166 df-frecs 8221 df-wrecs 8252 df-recs 8301 df-rdg 8339 df-1o 8395 df-er 8633 df-ec 8635 df-qs 8639 df-map 8765 df-en 8884 df-dom 8885 df-sdom 8886 df-fin 8887 df-sup 9345 df-inf 9346 df-pnf 11172 df-mnf 11173 df-xr 11174 df-ltxr 11175 df-le 11176 df-sub 11370 df-neg 11371 df-div 11799 df-nn 12166 df-2 12235 df-3 12236 df-4 12237 df-5 12238 df-6 12239 df-7 12240 df-8 12241 df-9 12242 df-n0 12429 df-z 12516 df-dec 12636 df-uz 12780 df-q 12890 df-rp 12934 df-fz 13453 df-fl 13742 df-mod 13820 df-seq 13955 df-exp 14015 df-cj 15052 df-re 15053 df-im 15054 df-sqrt 15188 df-abs 15189 df-dvds 16213 df-gcd 16455 df-numer 16696 df-denom 16697 df-struct 17108 df-sets 17125 df-slot 17143 df-ndx 17155 df-base 17171 df-ress 17192 df-plusg 17224 df-mulr 17225 df-starv 17226 df-sca 17227 df-vsca 17228 df-ip 17229 df-tset 17230 df-ple 17231 df-ds 17233 df-unif 17234 df-0g 17395 df-imas 17463 df-qus 17464 df-mgm 18599 df-sgrp 18678 df-mnd 18694 df-mhm 18742 df-submnd 18743 df-grp 18903 df-minusg 18904 df-sbg 18905 df-subg 19090 df-ghm 19179 df-cmn 19748 df-abl 19749 df-mgp 20113 df-rng 20125 df-ur 20154 df-ring 20207 df-cring 20208 df-oppr 20308 df-dvdsr 20328 df-unit 20329 df-invr 20359 df-dvr 20372 df-rhm 20443 df-rim 20444 df-nzr 20485 df-subrng 20518 df-subrg 20542 df-rlreg 20666 df-domn 20667 df-idom 20668 df-drng 20703 df-field 20704 df-cnfld 21348 df-zring 21422 df-erl 33336 df-rloc 33337 df-frac 33387

This theorem is referenced by: (None)

W3C validator