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 33517

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 27600	. . . . 5 ⊢ 𝑄 ∈ DivRing
3		drngring 20704	. . . . 5 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
4	2, 3	ax-mp 5	. . . 4 ⊢ 𝑄 ∈ Ring
5		zringidom 33514	. . . . 5 ⊢ ℤ_ring ∈ IDomn
6		id 22	. . . . . . . 8 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ IDomn)
7	6	fracfld 33250	. . . . . . 7 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Field)
8	7	fldcrngd 20710	. . . . . 6 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ CRing)
9	8	crngringd 20211	. . . . 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 20203	. . . . . . 7 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ Grp)
13	4, 12	ax-mp 5	. . . . . 6 ⊢ 𝑄 ∈ Grp
14		ringgrp 20203	. . . . . . 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 16759	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19		qdencl 16760	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
20	19	nnzd 12623	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
21	19	nnne0d 12298	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
22	20, 21	eldifsnd 4767	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
23	18, 22	opelxpd 5704	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24		zringfrac.2	. . . . . . . . . . 11 ⊢ ∼ = (ℤ_ring ~_RL (ℤ ∖ {0}))
25	24	ovexi 7447	. . . . . . . . . 10 ⊢ ∼ ∈ V
26	25	ecelqsi 8795	. . . . . . . . 9 ⊢ (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
27	23, 26	syl 17	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
28		zringbas 21426	. . . . . . . . . 10 ⊢ ℤ = (Base‘ℤ_ring)
29		zring0 21431	. . . . . . . . . 10 ⊢ 0 = (0_g‘ℤ_ring)
30		zringmulr 21430	. . . . . . . . . 10 ⊢ · = (._r‘ℤ_ring)
31		eqid 2734	. . . . . . . . . 10 ⊢ (-_g‘ℤ_ring) = (-_g‘ℤ_ring)
32		eqid 2734	. . . . . . . . . 10 ⊢ (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33		fracval 33246	. . . . . . . . . . 11 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
34	6	idomdomd 20694	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ Domn)
35	5, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℤ_ring ∈ Domn
36		eqid 2734	. . . . . . . . . . . . . . 15 ⊢ (RLReg‘ℤ_ring) = (RLReg‘ℤ_ring)
37	28, 36, 29	isdomn6 20682	. . . . . . . . . . . . . 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 7424	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
41	33, 40	eqtr4i 2760	. . . . . . . . . 10 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (ℤ ∖ {0}))
42	5	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℤ_ring ∈ IDomn)
43		difssd 4117	. . . . . . . . . 10 ⊢ (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
44	28, 29, 30, 31, 32, 41, 24, 42, 43	rlocbas 33210	. . . . . . . . 9 ⊢ (⊤ → ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring)))
45	44	mptru 1546	. . . . . . . 8 ⊢ ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring))
46	27, 45	eleqtrdi 2843	. . . . . . 7 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)))
47	17, 46	fmpti 7112	. . . . . 6 ⊢ 𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring))
48		ecexg 8731	. . . . . . . . . . . 12 ⊢ ( ∼ ∈ V → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V)
49	25, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V
50	17	fvmpt2 7007	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
51	49, 50	mpan2 691	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
52	51	adantr 480	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
53		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
55	53, 54	opeq12d 4861	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
56	55	eceq1d 8767	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
57	56, 17, 27	fvmpt3 7000	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℚ → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
58	57	adantl 481	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
59	52, 58	oveq12d 7431	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
60	41	fveq2i 6889	. . . . . . . . . 10 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
61	60	oveqi 7426	. . . . . . . . 9 ⊢ ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝))
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)))
63		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
65	63, 64	opeq12d 4861	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
66	65	eceq1d 8767	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
67	66	cbvmptv 5235	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
68	17, 67	eqtri 2757	. . . . . . . . 9 ⊢ 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
69		zring1 21432	. . . . . . . . . . . . 13 ⊢ 1 = (1_r‘ℤ_ring)
70	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ IDomn)
71	70	idomcringd 20695	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ CRing)
72	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ Domn)
73		eqid 2734	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘ℤ_ring) = (mulGrp‘ℤ_ring)
74	28, 29, 73	isdomn3 20683	. . . . . . . . . . . . . . 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 33208	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ∼ Er (ℤ × (ℤ ∖ {0})))
78		qcn 12987	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
79	78	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80		qcn 12987	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
81	80	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
82	79, 81	addcld 11262	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83		qaddcl 12989	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84		qdencl 16760	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
85	83, 84	syl 17	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
86	85	nncnd 12264	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
87	19	adantr 480	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
88	87	nncnd 12264	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89		qdencl 16760	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
90	89	adantl 481	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
91	90	nncnd 12264	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
92	88, 91	mulcld 11263	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
93	82, 86, 92	mul32d 11453	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94		qmuldeneqnum 16766	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
95	83, 94	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
96	95	oveq1d 7428	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
97	79, 88, 91	mulassd 11266	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98		qmuldeneqnum 16766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
99	98	adantr 480	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
100	99	oveq1d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
101	97, 100	eqtr3d 2771	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
102	81, 91, 88	mulassd 11266	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103		qmuldeneqnum 16766	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104	103	adantl 481	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105	104	oveq1d 7428	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
106	91, 88	mulcomd 11264	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107	106	oveq2d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108	102, 105, 107	3eqtr3rd 2778	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109	101, 108	oveq12d 7431	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
110	79, 92, 81, 109	joinlmuladdmuld 11270	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111	110	oveq1d 7428	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
112	93, 96, 111	3eqtr3d 2777	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
113	39	oveq2i 7424	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ~_RL (ℤ ∖ {0})) = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
114	24, 113	eqtri 2757	. . . . . . . . . . . . . 14 ⊢ ∼ = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
115		qnumcl 16759	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
116	83, 115	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
117	18	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
118	89	nnzd 12623	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119	118	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120	117, 119	zmulcld 12711	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121		qnumcl 16759	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122	121	adantl 481	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
123	20	adantr 480	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124	122, 123	zmulcld 12711	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125	120, 124	zaddcld 12709	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
126	85	nnzd 12623	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
127	85	nnne0d 12298	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128	126, 127	eldifsnd 4767	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129	128, 39	eleqtrdi 2843	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤ_ring))
130	123, 119	zmulcld 12711	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
131	87, 90	nnmulcld 12301	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132	131	nnne0d 12298	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133	130, 132	eldifsnd 4767	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134	133, 39	eleqtrdi 2843	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤ_ring))
135	28, 30, 114, 71, 116, 125, 129, 134	fracerl 33248	. . . . . . . . . . . . 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 8780	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
138	137	adantr 480	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
139		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140		fveq2 6886	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141	139, 140	opeq12d 4861	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142	141	adantl 481	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143	142	eceq1d 8767	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ )
144		zringplusg 21427	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
145		eqid 2734	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (ℤ ∖ {0}))
146		zringcrng 21421	. . . . . . . . . . . 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 12298	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156	118, 155	eldifsnd 4767	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157	156	adantl 481	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158	157	adantr 480	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159		eqid 2734	. . . . . . . . . . 11 ⊢ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
160	28, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159	rlocaddval 33211	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
161	138, 143, 160	3eqtr4d 2779	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
162		ovexd 7448	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) ∈ V)
163	68, 161, 83, 162	fvmptd2 7004	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
164	59, 62, 163	3eqtr4rd 2780	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
165	164	rgen2 3186	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
166	47, 165	pm3.2i 470	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
167	1	qrngbas 27599	. . . . . 6 ⊢ ℚ = (Base‘𝑄)
168		eqid 2734	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘( Frac ‘ℤ_ring))
169		qex 12985	. . . . . . 7 ⊢ ℚ ∈ V
170		cnfldadd 21332	. . . . . . . 8 ⊢ + = (+_g‘ℂ_fld)
171	1, 170	ressplusg 17307	. . . . . . 7 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
172	169, 171	ax-mp 5	. . . . . 6 ⊢ + = (+_g‘𝑄)
173		eqid 2734	. . . . . 6 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘( Frac ‘ℤ_ring))
174	167, 168, 172, 173	isghm 19202	. . . . 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 2734	. . . . . . . 8 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
177	176	ringmgp 20204	. . . . . . 7 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
178	4, 177	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘𝑄) ∈ Mnd
179		eqid 2734	. . . . . . . 8 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) = (mulGrp‘( Frac ‘ℤ_ring))
180	179	ringmgp 20204	. . . . . . 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 2734	. . . . . . . . . 10 ⊢ (._r‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))
184	28, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183	rlocmulval 33212	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
185	79, 81	mulcld 11263	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186		qmulcl 12991	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187		qdencl 16760	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188	186, 187	syl 17	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189	188	nncnd 12264	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190	185, 189, 92	mul32d 11453	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
191	79, 81, 88, 91	mul4d 11455	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192	191	oveq1d 7428	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193	190, 192	eqtrd 2769	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194		qmuldeneqnum 16766	. . . . . . . . . . . . . 14 ⊢ ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195	186, 194	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196	195	oveq1d 7428	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
197	99, 104	oveq12d 7431	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198	197	oveq1d 7428	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199	193, 196, 198	3eqtr3rd 2778	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200	117, 122	zmulcld 12711	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201		qnumcl 16759	. . . . . . . . . . . . 13 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202	186, 201	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203	188	nnzd 12623	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204	188	nnne0d 12298	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205	203, 204	eldifsnd 4767	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206	205, 39	eleqtrdi 2843	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤ_ring))
207	28, 30, 114, 71, 200, 202, 134, 206	fracerl 33248	. . . . . . . . . . 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 8780	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
210	184, 209	eqtrd 2769	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
211	41	fveq2i 6889	. . . . . . . . . 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 7434	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
214		fveq2 6886	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215		fveq2 6886	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216	214, 215	opeq12d 4861	. . . . . . . . . 10 ⊢ (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217	216	eceq1d 8767	. . . . . . . . 9 ⊢ (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
218		ecexg 8731	. . . . . . . . . 10 ⊢ ( ∼ ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
219	25, 218	mp1i 13	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
220	68, 217, 186, 219	fvmptd3 7019	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
221	210, 213, 220	3eqtr4rd 2780	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
222	221	rgen2 3186	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
223		zssq 12980	. . . . . . . 8 ⊢ ℤ ⊆ ℚ
224		1z 12630	. . . . . . . 8 ⊢ 1 ∈ ℤ
225	223, 224	sselii 3960	. . . . . . 7 ⊢ 1 ∈ ℚ
226		fveq2 6886	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227		1zzd 12631	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ IDomn → 1 ∈ ℤ)
228	227	znumd 32754	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (numer‘1) = 1)
229	5, 228	ax-mp 5	. . . . . . . . . . 11 ⊢ (numer‘1) = 1
230	226, 229	eqtrdi 2785	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (numer‘𝑞) = 1)
231		fveq2 6886	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232	227	zdend 32755	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (denom‘1) = 1)
233	5, 232	ax-mp 5	. . . . . . . . . . 11 ⊢ (denom‘1) = 1
234	231, 233	eqtrdi 2785	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (denom‘𝑞) = 1)
235	230, 234	opeq12d 4861	. . . . . . . . 9 ⊢ (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236	235	eceq1d 8767	. . . . . . . 8 ⊢ (𝑞 = 1 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨1, 1⟩] ∼ )
237	236, 17, 49	fvmpt3i 7001	. . . . . . 7 ⊢ (1 ∈ ℚ → (𝐹‘1) = [⟨1, 1⟩] ∼ )
238	225, 237	ax-mp 5	. . . . . 6 ⊢ (𝐹‘1) = [⟨1, 1⟩] ∼
239	47, 222, 238	3pm3.2i 1339	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] ∼ )
240	176, 167	mgpbas 20110	. . . . . 6 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
241	179, 168	mgpbas 20110	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘(mulGrp‘( Frac ‘ℤ_ring)))
242		cnfldmul 21334	. . . . . . . . 9 ⊢ · = (._r‘ℂ_fld)
243	1, 242	ressmulr 17323	. . . . . . . 8 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
244	169, 243	ax-mp 5	. . . . . . 7 ⊢ · = (._r‘𝑄)
245	176, 244	mgpplusg 20109	. . . . . 6 ⊢ · = (+_g‘(mulGrp‘𝑄))
246		eqid 2734	. . . . . . 7 ⊢ (._r‘( Frac ‘ℤ_ring)) = (._r‘( Frac ‘ℤ_ring))
247	179, 246	mgpplusg 20109	. . . . . 6 ⊢ (._r‘( Frac ‘ℤ_ring)) = (+_g‘(mulGrp‘( Frac ‘ℤ_ring)))
248	1	qrng1 27602	. . . . . . 7 ⊢ 1 = (1_r‘𝑄)
249	176, 248	ringidval 20148	. . . . . 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 2734	. . . . . . . . 9 ⊢ [⟨1, 1⟩] ∼ = [⟨1, 1⟩] ∼
253	29, 69, 41, 24, 250, 251, 252	rloc1r 33215	. . . . . . . 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 20148	. . . . . 6 ⊢ [⟨1, 1⟩] ∼ = (0_g‘(mulGrp‘( Frac ‘ℤ_ring)))
256	240, 241, 245, 247, 249, 255	ismhm 18767	. . . . 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 20446	. . 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 3052	. . . 4 ⊢ ∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring))
262	117	zcnd 12706	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263	122	zcnd 12706	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
264	21	adantr 480	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265	155	adantl 481	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266	262, 88, 263, 91, 264, 265	divmuleqd 12071	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267	153, 39	eleqtrdi 2843	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤ_ring))
268	157, 39	eleqtrdi 2843	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤ_ring))
269	28, 30, 114, 71, 117, 122, 267, 268	fracerl 33248	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
270	23	adantr 480	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
271	77, 270	erth 8778	. . . . . . . . 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 16765	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275	274	ad2antrr 726	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276		qeqnumdivden 16765	. . . . . . . 8 ⊢ (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277	276	ad2antlr 727	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278	273, 275, 277	3eqtr4d 2779	. . . . . 6 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = 𝑝)
279	278	ex 412	. . . . 5 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝))
280	279	rgen2 3186	. . . 4 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)
281	17, 56	f1mpt 7263	. . . 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 6886	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284		fveq2 6886	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285	283, 284	opeq12d 4861	. . . . . . . . 9 ⊢ (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286	285	eceq1d 8767	. . . . . . . 8 ⊢ (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
287	286	eqeq2d 2745	. . . . . . 7 ⊢ (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ↔ 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ ))
288		simpllr 775	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℤ)
289	223, 288	sselid 3961	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℚ)
290		simplr 768	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ (ℤ ∖ {0}))
291	290	eldifad 3943	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℤ)
292	223, 291	sselid 3961	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℚ)
293		eldifsni 4770	. . . . . . . . 9 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294	290, 293	syl 17	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ≠ 0)
295		qdivcl 12994	. . . . . . . 8 ⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296	289, 292, 294, 295	syl3anc 1372	. . . . . . 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 33208	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∼ Er (ℤ × (ℤ ∖ {0})))
301		simpl 482	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302	301	zcnd 12706	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303		eldifi 4111	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304	303	adantl 481	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305	304	zcnd 12706	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306	293	adantl 481	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307	302, 305, 306	divcld 12025	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308	223, 301	sselid 3961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309	223, 304	sselid 3961	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310	308, 309, 306, 295	syl3anc 1372	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311		qdencl 16760	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312	310, 311	syl 17	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313	312	nncnd 12264	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314	307, 313, 305	mul32d 11453	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315		qmuldeneqnum 16766	. . . . . . . . . . . . . 14 ⊢ ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316	310, 315	syl 17	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317	316	oveq1d 7428	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318	302, 305, 306	divcan1d 12026	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319	318	oveq1d 7428	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320	314, 317, 319	3eqtr3rd 2778	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤ_ring ∈ CRing)
322		qnumcl 16759	. . . . . . . . . . . . 13 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323	310, 322	syl 17	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324		simpr 484	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325	324, 39	eleqtrdi 2843	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤ_ring))
326	312	nnzd 12623	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327	312	nnne0d 12298	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328	326, 327	eldifsnd 4767	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329	328, 39	eleqtrdi 2843	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤ_ring))
330	28, 30, 114, 321, 301, 323, 325, 329	fracerl 33248	. . . . . . . . . . 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 8780	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → [⟨𝑎, 𝑏⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
334	297, 333	eqtrd 2769	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
335	287, 296, 334	rspcedvdw 3608	. . . . . 6 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
336	45	eleq2i 2825	. . . . . . . 8 ⊢ (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤ_ring)))
337	336	biimpri 228	. . . . . . 7 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
338	337	elrlocbasi 33209	. . . . . 6 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] ∼ )
339	335, 338	r19.29vva 3203	. . . . 5 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
340	339	rgen 3052	. . . 4 ⊢ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼
341	17	fompt 7118	. . . 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 6548	. . 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 20460	. 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 1539 ⊤wtru 1540 ∈ wcel 2107 ≠ wne 2931 ∀wral 3050 ∃wrex 3059 Vcvv 3463 ∖ cdif 3928 {csn 4606 ⟨cop 4612 class class class wbr 5123 ↦ cmpt 5205 × cxp 5663 ⟶wf 6537 –1-1→wf1 6538 –onto→wfo 6539 –1-1-onto→wf1o 6540 ‘cfv 6541 (class class class)co 7413 [cec 8725 / cqs 8726 ℂcc 11135 0cc0 11137 1c1 11138 + caddc 11140 · cmul 11142 / cdiv 11902 ℕcn 12248 ℤcz 12596 ℚcq 12972 numercnumer 16752 denomcdenom 16753 Basecbs 17229 ↾_s cress 17252 +_gcplusg 17273 ._rcmulr 17274 Mndcmnd 18716 MndHom cmhm 18763 SubMndcsubmnd 18764 Grpcgrp 18920 -_gcsg 18922 GrpHom cghm 19199 mulGrpcmgp 20105 1_rcur 20146 Ringcrg 20198 CRingccrg 20199 RingHom crh 20437 RingIso crs 20438 NzRingcnzr 20480 RLRegcrlreg 20659 Domncdomn 20660 IDomncidom 20661 DivRingcdr 20697 ℂ_fldccnfld 21326 ℤ_ringczring 21419 ~_RL cerl 33196 RLocal crloc 33197 Frac cfrac 33244

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1794 ax-4 1808 ax-5 1909 ax-6 1966 ax-7 2006 ax-8 2109 ax-9 2117 ax-10 2140 ax-11 2156 ax-12 2176 ax-ext 2706 ax-rep 5259 ax-sep 5276 ax-nul 5286 ax-pow 5345 ax-pr 5412 ax-un 7737 ax-cnex 11193 ax-resscn 11194 ax-1cn 11195 ax-icn 11196 ax-addcl 11197 ax-addrcl 11198 ax-mulcl 11199 ax-mulrcl 11200 ax-mulcom 11201 ax-addass 11202 ax-mulass 11203 ax-distr 11204 ax-i2m1 11205 ax-1ne0 11206 ax-1rid 11207 ax-rnegex 11208 ax-rrecex 11209 ax-cnre 11210 ax-pre-lttri 11211 ax-pre-lttrn 11212 ax-pre-ltadd 11213 ax-pre-mulgt0 11214 ax-pre-sup 11215 ax-addf 11216 ax-mulf 11217

This theorem depends on definitions: df-bi 207 df-an 396 df-or 848 df-3or 1087 df-3an 1088 df-tru 1542 df-fal 1552 df-ex 1779 df-nf 1783 df-sb 2064 df-mo 2538 df-eu 2567 df-clab 2713 df-cleq 2726 df-clel 2808 df-nfc 2884 df-ne 2932 df-nel 3036 df-ral 3051 df-rex 3060 df-rmo 3363 df-reu 3364 df-rab 3420 df-v 3465 df-sbc 3771 df-csb 3880 df-dif 3934 df-un 3936 df-in 3938 df-ss 3948 df-pss 3951 df-nul 4314 df-if 4506 df-pw 4582 df-sn 4607 df-pr 4609 df-tp 4611 df-op 4613 df-uni 4888 df-iun 4973 df-br 5124 df-opab 5186 df-mpt 5206 df-tr 5240 df-id 5558 df-eprel 5564 df-po 5572 df-so 5573 df-fr 5617 df-we 5619 df-xp 5671 df-rel 5672 df-cnv 5673 df-co 5674 df-dm 5675 df-rn 5676 df-res 5677 df-ima 5678 df-pred 6301 df-ord 6366 df-on 6367 df-lim 6368 df-suc 6369 df-iota 6494 df-fun 6543 df-fn 6544 df-f 6545 df-f1 6546 df-fo 6547 df-f1o 6548 df-fv 6549 df-riota 7370 df-ov 7416 df-oprab 7417 df-mpo 7418 df-om 7870 df-1st 7996 df-2nd 7997 df-tpos 8233 df-frecs 8288 df-wrecs 8319 df-recs 8393 df-rdg 8432 df-1o 8488 df-er 8727 df-ec 8729 df-qs 8733 df-map 8850 df-en 8968 df-dom 8969 df-sdom 8970 df-fin 8971 df-sup 9464 df-inf 9465 df-pnf 11279 df-mnf 11280 df-xr 11281 df-ltxr 11282 df-le 11283 df-sub 11476 df-neg 11477 df-div 11903 df-nn 12249 df-2 12311 df-3 12312 df-4 12313 df-5 12314 df-6 12315 df-7 12316 df-8 12317 df-9 12318 df-n0 12510 df-z 12597 df-dec 12717 df-uz 12861 df-q 12973 df-rp 13017 df-fz 13530 df-fl 13814 df-mod 13892 df-seq 14025 df-exp 14085 df-cj 15120 df-re 15121 df-im 15122 df-sqrt 15256 df-abs 15257 df-dvds 16273 df-gcd 16514 df-numer 16754 df-denom 16755 df-struct 17166 df-sets 17183 df-slot 17201 df-ndx 17213 df-base 17230 df-ress 17253 df-plusg 17286 df-mulr 17287 df-starv 17288 df-sca 17289 df-vsca 17290 df-ip 17291 df-tset 17292 df-ple 17293 df-ds 17295 df-unif 17296 df-0g 17457 df-imas 17524 df-qus 17525 df-mgm 18622 df-sgrp 18701 df-mnd 18717 df-mhm 18765 df-submnd 18766 df-grp 18923 df-minusg 18924 df-sbg 18925 df-subg 19110 df-ghm 19200 df-cmn 19768 df-abl 19769 df-mgp 20106 df-rng 20118 df-ur 20147 df-ring 20200 df-cring 20201 df-oppr 20302 df-dvdsr 20325 df-unit 20326 df-invr 20356 df-dvr 20369 df-rhm 20440 df-rim 20441 df-nzr 20481 df-subrng 20514 df-subrg 20538 df-rlreg 20662 df-domn 20663 df-idom 20664 df-drng 20699 df-field 20700 df-cnfld 21327 df-zring 21420 df-erl 33198 df-rloc 33199 df-frac 33245

This theorem is referenced by: (None)

W3C validator