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 33965

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 27857	. . . . 5 ⊢ 𝑄 ∈ DivRing
3		drngring 20898	. . . . 5 ⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
4	2, 3	ax-mp 5	. . . 4 ⊢ 𝑄 ∈ Ring
5		zringidom 33962	. . . . 5 ⊢ ℤ_ring ∈ IDomn
6		id 23	. . . . . . . 8 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ IDomn)
7	6	fracfld 33750	. . . . . . 7 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ Field)
8	7	fldcrngd 20906	. . . . . 6 ⊢ (ℤ_ring ∈ IDomn → ( Frac ‘ℤ_ring) ∈ CRing)
9	8	crngringd 20386	. . . . 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 20378	. . . . . . 7 ⊢ (𝑄 ∈ Ring → 𝑄 ∈ Grp)
13	4, 12	ax-mp 5	. . . . . 6 ⊢ 𝑄 ∈ Grp
14		ringgrp 20378	. . . . . . 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 16832	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19		qdencl 16833	. . . . . . . . . . . 12 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
20	19	nnzd 12642	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
21	19	nnne0d 12311	. . . . . . . . . . 11 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
22	20, 21	eldifsnd 4750	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
23	18, 22	opelxpd 5694	. . . . . . . . 9 ⊢ (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24		zringfrac.2	. . . . . . . . . . 11 ⊢ ∼ = (ℤ_ring ~_RL (ℤ ∖ {0}))
25	24	ovexi 7448	. . . . . . . . . 10 ⊢ ∼ ∈ V
26	25	ecelqsi 8770	. . . . . . . . 9 ⊢ (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
27	23, 26	syl 18	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
28		zringbas 21667	. . . . . . . . . 10 ⊢ ℤ = (Base‘ℤ_ring)
29		zring0 21672	. . . . . . . . . 10 ⊢ 0 = (0_g‘ℤ_ring)
30		zringmulr 21671	. . . . . . . . . 10 ⊢ · = (._r‘ℤ_ring)
31		eqid 2760	. . . . . . . . . 10 ⊢ (-_g‘ℤ_ring) = (-_g‘ℤ_ring)
32		eqid 2760	. . . . . . . . . 10 ⊢ (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33		fracval 33746	. . . . . . . . . . 11 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
34	6	idomdomd 20888	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ∈ IDomn → ℤ_ring ∈ Domn)
35	5, 34	ax-mp 5	. . . . . . . . . . . . . 14 ⊢ ℤ_ring ∈ Domn
36		eqid 2760	. . . . . . . . . . . . . . 15 ⊢ (RLReg‘ℤ_ring) = (RLReg‘ℤ_ring)
37	28, 36, 29	isdomn6 20876	. . . . . . . . . . . . . 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 7425	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (RLReg‘ℤ_ring))
41	33, 40	eqtr4i 2786	. . . . . . . . . 10 ⊢ ( Frac ‘ℤ_ring) = (ℤ_ring RLocal (ℤ ∖ {0}))
42	5	a1i 11	. . . . . . . . . 10 ⊢ (⊤ → ℤ_ring ∈ IDomn)
43		difssd 4084	. . . . . . . . . 10 ⊢ (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
44	28, 29, 30, 31, 32, 41, 24, 42, 43	rlocbas 33709	. . . . . . . . 9 ⊢ (⊤ → ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring)))
45	44	mptru 1577	. . . . . . . 8 ⊢ ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘( Frac ‘ℤ_ring))
46	27, 45	eleqtrdi 2870	. . . . . . 7 ⊢ (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring)))
47	17, 46	fmpti 7106	. . . . . 6 ⊢ 𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring))
48		ecexg 8701	. . . . . . . . . . . 12 ⊢ ( ∼ ∈ V → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V)
49	25, 48	ax-mp 5	. . . . . . . . . . 11 ⊢ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V
50	17	fvmpt2 6999	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ V) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
51	49, 50	mpan2 704	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
52	51	adantr 486	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
53		fveq2 6879	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54		fveq2 6879	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
55	53, 54	opeq12d 4841	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
56	55	eceq1d 8738	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
57	56, 17, 27	fvmpt3 6992	. . . . . . . . . 10 ⊢ (𝑝 ∈ ℚ → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
58	57	adantl 487	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ )
59	52, 58	oveq12d 7432	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
60	41	fveq2i 6882	. . . . . . . . . 10 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
61	60	oveqi 7427	. . . . . . . . 9 ⊢ ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝))
62	61	a1i 11	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))(𝐹‘𝑝)))
63		fveq2 6879	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64		fveq2 6879	. . . . . . . . . . . . 13 ⊢ (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
65	63, 64	opeq12d 4841	. . . . . . . . . . . 12 ⊢ (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
66	65	eceq1d 8738	. . . . . . . . . . 11 ⊢ (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
67	66	cbvmptv 5209	. . . . . . . . . 10 ⊢ (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
68	17, 67	eqtri 2783	. . . . . . . . 9 ⊢ 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ )
69		zring1 21673	. . . . . . . . . . . . 13 ⊢ 1 = (1_r‘ℤ_ring)
70	5	a1i 11	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ IDomn)
71	70	idomcringd 20889	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ CRing)
72	35	a1i 11	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤ_ring ∈ Domn)
73		eqid 2760	. . . . . . . . . . . . . . . 16 ⊢ (mulGrp‘ℤ_ring) = (mulGrp‘ℤ_ring)
74	28, 29, 73	isdomn3 20877	. . . . . . . . . . . . . . 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 33706	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ∼ Er (ℤ × (ℤ ∖ {0})))
78		qcn 13013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
79	78	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80		qcn 13013	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
81	80	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
82	79, 81	addcld 11253	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83		qaddcl 13016	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84		qdencl 16833	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
85	83, 84	syl 18	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
86	85	nncnd 12274	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
87	19	adantr 486	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
88	87	nncnd 12274	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89		qdencl 16833	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
90	89	adantl 487	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
91	90	nncnd 12274	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
92	88, 91	mulcld 11254	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
93	82, 86, 92	mul32d 11445	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94		qmuldeneqnum 16839	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
95	83, 94	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
96	95	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
97	79, 88, 91	mulassd 11257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98		qmuldeneqnum 16839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
99	98	adantr 486	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
100	99	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
101	97, 100	eqtr3d 2797	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
102	81, 91, 88	mulassd 11257	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103		qmuldeneqnum 16839	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104	103	adantl 487	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105	104	oveq1d 7429	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
106	91, 88	mulcomd 11255	. . . . . . . . . . . . . . . . . . 19 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107	106	oveq2d 7430	. . . . . . . . . . . . . . . . . 18 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108	102, 105, 107	3eqtr3rd 2804	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109	101, 108	oveq12d 7432	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
110	79, 92, 81, 109	joinlmuladdmuld 11261	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111	110	oveq1d 7429	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
112	93, 96, 111	3eqtr3d 2803	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
113	39	oveq2i 7425	. . . . . . . . . . . . . . 15 ⊢ (ℤ_ring ~_RL (ℤ ∖ {0})) = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
114	24, 113	eqtri 2783	. . . . . . . . . . . . . 14 ⊢ ∼ = (ℤ_ring ~_RL (RLReg‘ℤ_ring))
115		qnumcl 16832	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
116	83, 115	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
117	18	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
118	89	nnzd 12642	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119	118	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120	117, 119	zmulcld 12732	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121		qnumcl 16832	. . . . . . . . . . . . . . . . 17 ⊢ (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122	121	adantl 487	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
123	20	adantr 486	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124	122, 123	zmulcld 12732	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125	120, 124	zaddcld 12730	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
126	85	nnzd 12642	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
127	85	nnne0d 12311	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128	126, 127	eldifsnd 4750	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129	128, 39	eleqtrdi 2870	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤ_ring))
130	123, 119	zmulcld 12732	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
131	87, 90	nnmulcld 12314	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132	131	nnne0d 12311	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133	130, 132	eldifsnd 4750	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134	133, 39	eleqtrdi 2870	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤ_ring))
135	28, 30, 114, 71, 116, 125, 129, 134	fracerl 33748	. . . . . . . . . . . . 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 8754	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
138	137	adantr 486	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
139		fveq2 6879	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140		fveq2 6879	. . . . . . . . . . . . 13 ⊢ (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141	139, 140	opeq12d 4841	. . . . . . . . . . . 12 ⊢ (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142	141	adantl 487	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143	142	eceq1d 8738	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] ∼ )
144		zringplusg 21668	. . . . . . . . . . 11 ⊢ + = (+_g‘ℤ_ring)
145		eqid 2760	. . . . . . . . . . 11 ⊢ (ℤ_ring RLocal (ℤ ∖ {0})) = (ℤ_ring RLocal (ℤ ∖ {0}))
146		zringcrng 21662	. . . . . . . . . . . 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 12311	. . . . . . . . . . . . . 14 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156	118, 155	eldifsnd 4750	. . . . . . . . . . . . 13 ⊢ (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157	156	adantl 487	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158	157	adantr 486	. . . . . . . . . . 11 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159		eqid 2760	. . . . . . . . . . 11 ⊢ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))
160	28, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159	rlocaddval 33710	. . . . . . . . . 10 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
161	138, 143, 160	3eqtr4d 2805	. . . . . . . . 9 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
162		ovexd 7449	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) ∈ V)
163	68, 161, 83, 162	fvmptd2 6996	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (+_g‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
164	59, 62, 163	3eqtr4rd 2806	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
165	164	rgen2 3202	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
166	47, 165	pm3.2i 476	. . . . 5 ⊢ (𝐹:ℚ⟶(Base‘( Frac ‘ℤ_ring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+_g‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
167	1	qrngbas 27856	. . . . . 6 ⊢ ℚ = (Base‘𝑄)
168		eqid 2760	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘( Frac ‘ℤ_ring))
169		qex 13011	. . . . . . 7 ⊢ ℚ ∈ V
170		cnfldadd 21592	. . . . . . . 8 ⊢ + = (+_g‘ℂ_fld)
171	1, 170	ressplusg 17377	. . . . . . 7 ⊢ (ℚ ∈ V → + = (+_g‘𝑄))
172	169, 171	ax-mp 5	. . . . . 6 ⊢ + = (+_g‘𝑄)
173		eqid 2760	. . . . . 6 ⊢ (+_g‘( Frac ‘ℤ_ring)) = (+_g‘( Frac ‘ℤ_ring))
174	167, 168, 172, 173	isghm 19344	. . . . 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 2760	. . . . . . . 8 ⊢ (mulGrp‘𝑄) = (mulGrp‘𝑄)
177	176	ringmgp 20379	. . . . . . 7 ⊢ (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
178	4, 177	ax-mp 5	. . . . . 6 ⊢ (mulGrp‘𝑄) ∈ Mnd
179		eqid 2760	. . . . . . . 8 ⊢ (mulGrp‘( Frac ‘ℤ_ring)) = (mulGrp‘( Frac ‘ℤ_ring))
180	179	ringmgp 20379	. . . . . . 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 2760	. . . . . . . . . 10 ⊢ (._r‘(ℤ_ring RLocal (ℤ ∖ {0}))) = (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))
184	28, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183	rlocmulval 33711	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ )
185	79, 81	mulcld 11254	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186		qmulcl 13018	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187		qdencl 16833	. . . . . . . . . . . . . . . 16 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188	186, 187	syl 18	. . . . . . . . . . . . . . 15 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189	188	nncnd 12274	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190	185, 189, 92	mul32d 11445	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
191	79, 81, 88, 91	mul4d 11447	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192	191	oveq1d 7429	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193	190, 192	eqtrd 2795	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194		qmuldeneqnum 16839	. . . . . . . . . . . . . 14 ⊢ ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195	186, 194	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196	195	oveq1d 7429	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
197	99, 104	oveq12d 7432	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198	197	oveq1d 7429	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199	193, 196, 198	3eqtr3rd 2804	. . . . . . . . . . 11 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200	117, 122	zmulcld 12732	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201		qnumcl 16832	. . . . . . . . . . . . 13 ⊢ ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202	186, 201	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203	188	nnzd 12642	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204	188	nnne0d 12311	. . . . . . . . . . . . . 14 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205	203, 204	eldifsnd 4750	. . . . . . . . . . . . 13 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206	205, 39	eleqtrdi 2870	. . . . . . . . . . . 12 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤ_ring))
207	28, 30, 114, 71, 200, 202, 134, 206	fracerl 33748	. . . . . . . . . . 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 8754	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
210	184, 209	eqtrd 2795	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
211	41	fveq2i 6882	. . . . . . . . . 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 7435	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ (._r‘(ℤ_ring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ))
214		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216	214, 215	opeq12d 4841	. . . . . . . . . 10 ⊢ (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217	216	eceq1d 8738	. . . . . . . . 9 ⊢ (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] ∼ = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
218		ecexg 8701	. . . . . . . . . 10 ⊢ ( ∼ ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
219	25, 218	mp1i 14	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ ∈ V)
220	68, 217, 186, 219	fvmptd3 7011	. . . . . . . 8 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∼ )
221	210, 213, 220	3eqtr4rd 2806	. . . . . . 7 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝)))
222	221	rgen2 3202	. . . . . 6 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(._r‘( Frac ‘ℤ_ring))(𝐹‘𝑝))
223		zssq 13006	. . . . . . . 8 ⊢ ℤ ⊆ ℚ
224		1z 12649	. . . . . . . 8 ⊢ 1 ∈ ℤ
225	223, 224	sselii 3928	. . . . . . 7 ⊢ 1 ∈ ℚ
226		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227		1zzd 12650	. . . . . . . . . . . . 13 ⊢ (ℤ_ring ∈ IDomn → 1 ∈ ℤ)
228	227	znumd 33284	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (numer‘1) = 1)
229	5, 228	ax-mp 5	. . . . . . . . . . 11 ⊢ (numer‘1) = 1
230	226, 229	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (numer‘𝑞) = 1)
231		fveq2 6879	. . . . . . . . . . 11 ⊢ (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232	227	zdend 33285	. . . . . . . . . . . 12 ⊢ (ℤ_ring ∈ IDomn → (denom‘1) = 1)
233	5, 232	ax-mp 5	. . . . . . . . . . 11 ⊢ (denom‘1) = 1
234	231, 233	eqtrdi 2811	. . . . . . . . . 10 ⊢ (𝑞 = 1 → (denom‘𝑞) = 1)
235	230, 234	opeq12d 4841	. . . . . . . . 9 ⊢ (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236	235	eceq1d 8738	. . . . . . . 8 ⊢ (𝑞 = 1 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨1, 1⟩] ∼ )
237	236, 17, 49	fvmpt3i 6993	. . . . . . 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 20279	. . . . . 6 ⊢ ℚ = (Base‘(mulGrp‘𝑄))
241	179, 168	mgpbas 20279	. . . . . 6 ⊢ (Base‘( Frac ‘ℤ_ring)) = (Base‘(mulGrp‘( Frac ‘ℤ_ring)))
242		cnfldmul 21594	. . . . . . . . 9 ⊢ · = (._r‘ℂ_fld)
243	1, 242	ressmulr 17393	. . . . . . . 8 ⊢ (ℚ ∈ V → · = (._r‘𝑄))
244	169, 243	ax-mp 5	. . . . . . 7 ⊢ · = (._r‘𝑄)
245	176, 244	mgpplusg 20278	. . . . . 6 ⊢ · = (+_g‘(mulGrp‘𝑄))
246		eqid 2760	. . . . . . 7 ⊢ (._r‘( Frac ‘ℤ_ring)) = (._r‘( Frac ‘ℤ_ring))
247	179, 246	mgpplusg 20278	. . . . . 6 ⊢ (._r‘( Frac ‘ℤ_ring)) = (+_g‘(mulGrp‘( Frac ‘ℤ_ring)))
248	1	qrng1 27859	. . . . . . 7 ⊢ 1 = (1_r‘𝑄)
249	176, 248	ringidval 20323	. . . . . 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 2760	. . . . . . . . 9 ⊢ [⟨1, 1⟩] ∼ = [⟨1, 1⟩] ∼
253	29, 69, 41, 24, 250, 251, 252	rloc1r 33714	. . . . . . . 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 20323	. . . . . 6 ⊢ [⟨1, 1⟩] ∼ = (0_g‘(mulGrp‘( Frac ‘ℤ_ring)))
256	240, 241, 245, 247, 249, 255	ismhm 18894	. . . . 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 20621	. . 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 3078	. . . 4 ⊢ ∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ∈ (Base‘( Frac ‘ℤ_ring))
262	117	zcnd 12727	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263	122	zcnd 12727	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
264	21	adantr 486	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265	155	adantl 487	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266	262, 88, 263, 91, 264, 265	divmuleqd 12062	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267	153, 39	eleqtrdi 2870	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤ_ring))
268	157, 39	eleqtrdi 2870	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤ_ring))
269	28, 30, 114, 71, 117, 122, 267, 268	fracerl 33748	. . . . . . . . 9 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∼ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
270	23	adantr 486	. . . . . . . . . 10 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
271	77, 270	erth 8752	. . . . . . . . 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 16838	. . . . . . . 8 ⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275	274	ad2antrr 739	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276		qeqnumdivden 16838	. . . . . . . 8 ⊢ (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277	276	ad2antlr 740	. . . . . . 7 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278	273, 275, 277	3eqtr4d 2805	. . . . . 6 ⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ ) → 𝑞 = 𝑝)
279	278	ex 418	. . . . 5 ⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝))
280	279	rgen2 3202	. . . 4 ⊢ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ∼ → 𝑞 = 𝑝)
281	17, 56	f1mpt 7259	. . . 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 6879	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284		fveq2 6879	. . . . . . . . . 10 ⊢ (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285	283, 284	opeq12d 4841	. . . . . . . . 9 ⊢ (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286	285	eceq1d 8738	. . . . . . . 8 ⊢ (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
287	286	eqeq2d 2771	. . . . . . 7 ⊢ (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ ↔ 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ ))
288		simpllr 788	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℤ)
289	223, 288	sselid 3929	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑎 ∈ ℚ)
290		simplr 781	. . . . . . . . . 10 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ (ℤ ∖ {0}))
291	290	eldifad 3911	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℤ)
292	223, 291	sselid 3929	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ∈ ℚ)
293		eldifsni 4753	. . . . . . . . 9 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294	290, 293	syl 18	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑏 ≠ 0)
295		qdivcl 13021	. . . . . . . 8 ⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296	289, 292, 294, 295	syl3anc 1398	. . . . . . 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 33706	. . . . . . . . 9 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∼ Er (ℤ × (ℤ ∖ {0})))
301		simpl 488	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302	301	zcnd 12727	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303		eldifi 4078	. . . . . . . . . . . . . . . 16 ⊢ (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304	303	adantl 487	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305	304	zcnd 12727	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306	293	adantl 487	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307	302, 305, 306	divcld 12016	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308	223, 301	sselid 3929	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309	223, 304	sselid 3929	. . . . . . . . . . . . . . . 16 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310	308, 309, 306, 295	syl3anc 1398	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311		qdencl 16833	. . . . . . . . . . . . . . 15 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312	310, 311	syl 18	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313	312	nncnd 12274	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314	307, 313, 305	mul32d 11445	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315		qmuldeneqnum 16839	. . . . . . . . . . . . . 14 ⊢ ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316	310, 315	syl 18	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317	316	oveq1d 7429	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318	302, 305, 306	divcan1d 12017	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319	318	oveq1d 7429	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320	314, 317, 319	3eqtr3rd 2804	. . . . . . . . . . 11 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321	146	a1i 11	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤ_ring ∈ CRing)
322		qnumcl 16832	. . . . . . . . . . . . 13 ⊢ ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323	310, 322	syl 18	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324		simpr 490	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325	324, 39	eleqtrdi 2870	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤ_ring))
326	312	nnzd 12642	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327	312	nnne0d 12311	. . . . . . . . . . . . . 14 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328	326, 327	eldifsnd 4750	. . . . . . . . . . . . 13 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329	328, 39	eleqtrdi 2870	. . . . . . . . . . . 12 ⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤ_ring))
330	28, 30, 114, 321, 301, 323, 325, 329	fracerl 33748	. . . . . . . . . . 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 8754	. . . . . . . 8 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → [⟨𝑎, 𝑏⟩] ∼ = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
334	297, 333	eqtrd 2795	. . . . . . 7 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ∼ )
335	287, 296, 334	rspcedvdw 3579	. . . . . 6 ⊢ ((((𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ∼ ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
336	45	eleq2i 2852	. . . . . . . 8 ⊢ (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤ_ring)))
337	336	biimpri 231	. . . . . . 7 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ∼ ))
338	337	elrlocbasi 33708	. . . . . 6 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] ∼ )
339	335, 338	r19.29vva 3222	. . . . 5 ⊢ (𝑧 ∈ (Base‘( Frac ‘ℤ_ring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼ )
340	339	rgen 3078	. . . 4 ⊢ ∀𝑧 ∈ (Base‘( Frac ‘ℤ_ring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∼
341	17	fompt 7112	. . . 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 6540	. . 3 ⊢ (𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring)) ↔ (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ–onto→(Base‘( Frac ‘ℤ_ring))))
344	282, 342, 343	mpbir2an 724	. 2 ⊢ 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤ_ring))
345	167, 168	isrim 20640	. 2 ⊢ (𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤ_ring)) ↔ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤ_ring)) ∧ 𝐹:ℚ–1-1-onto→(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 2145 ≠ wne 2955 ∀wral 3076 ∃wrex 3086 Vcvv 3450 ∖ cdif 3896 {csn 4584 ⟨cop 4590 class class class wbr 5103 ↦ cmpt 5186 × cxp 5653 ⟶wf 6529 –1-1→wf1 6530 –onto→wfo 6531 –1-1-onto→wf1o 6532 ‘cfv 6533 (class class class)co 7414 [cec 8695 / cqs 8696 ℂcc 11123 0cc0 11125 1c1 11126 + caddc 11128 · cmul 11130 / cdiv 11896 ℕcn 12258 ℤcz 12616 ℚcq 12998 numercnumer 16825 denomcdenom 16826 Basecbs 17302 ↾_s cress 17323 +_gcplusg 17343 ._rcmulr 17344 Mndcmnd 18837 MndHom cmhm 18890 SubMndcsubmnd 18891 Grpcgrp 19058 -_gcsg 19060 GrpHom cghm 19341 mulGrpcmgp 20274 1_rcur 20321 Ringcrg 20373 CRingccrg 20374 RingHom crh 20611 RingIso crs 20612 NzRingcnzr 20673 RLRegcrlreg 20854 Domncdomn 20855 IDomncidom 20856 DivRingcdr 20891 ℂ_fldccnfld 21586 ℤ_ringczring 21660 ~_RL cerl 33694 RLocal crloc 33695 Frac cfrac 33744

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 1943 ax-6 2000 ax-7 2041 ax-8 2147 ax-9 2155 ax-10 2178 ax-11 2194 ax-12 2213 ax-ext 2732 ax-rep 5232 ax-sep 5251 ax-nul 5263 ax-pow 5330 ax-pr 5398 ax-un 7737 ax-cnex 11181 ax-resscn 11182 ax-1cn 11183 ax-icn 11184 ax-addcl 11185 ax-addrcl 11186 ax-mulcl 11187 ax-mulrcl 11188 ax-mulcom 11189 ax-addass 11190 ax-mulass 11191 ax-distr 11192 ax-i2m1 11193 ax-1ne0 11194 ax-1rid 11195 ax-rnegex 11196 ax-rrecex 11197 ax-cnre 11198 ax-pre-lttri 11199 ax-pre-lttrn 11200 ax-pre-ltadd 11201 ax-pre-mulgt0 11202 ax-pre-sup 11203 ax-addf 11204 ax-mulf 11205

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 2100 df-mo 2564 df-eu 2594 df-clab 2739 df-cleq 2752 df-clel 2835 df-nfc 2909 df-ne 2956 df-nel 3062 df-ral 3077 df-rex 3087 df-rmo 3365 df-reu 3366 df-rab 3413 df-v 3452 df-sbc 3740 df-csb 3848 df-dif 3902 df-un 3904 df-in 3906 df-ss 3916 df-pss 3919 df-nul 4280 df-if 4483 df-pw 4559 df-sn 4585 df-pr 4587 df-tp 4589 df-op 4591 df-uni 4868 df-iun 4953 df-br 5104 df-opab 5168 df-mpt 5187 df-tr 5213 df-id 5550 df-eprel 5555 df-po 5563 df-so 5564 df-fr 5608 df-we 5610 df-xp 5661 df-rel 5662 df-cnv 5663 df-co 5664 df-dm 5665 df-rn 5666 df-res 5667 df-ima 5668 df-pred 6299 df-ord 6360 df-on 6361 df-lim 6362 df-suc 6363 df-iota 6489 df-fun 6535 df-fn 6536 df-f 6537 df-f1 6538 df-fo 6539 df-f1o 6540 df-fv 6541 df-riota 7371 df-ov 7417 df-oprab 7418 df-mpo 7419 df-om 7864 df-1st 7987 df-2nd 7988 df-tpos 8225 df-frecs 8281 df-wrecs 8312 df-recs 8361 df-rdg 8400 df-1o 8456 df-er 8697 df-ec 8699 df-qs 8703 df-map 8829 df-en 8954 df-dom 8955 df-sdom 8956 df-fin 8957 df-sup 9413 df-inf 9414 df-pnf 11270 df-mnf 11271 df-xr 11272 df-ltxr 11273 df-le 11274 df-sub 11468 df-neg 11469 df-div 11897 df-nn 12259 df-2 12328 df-3 12329 df-4 12330 df-5 12331 df-6 12332 df-7 12333 df-8 12334 df-9 12335 df-n0 12530 df-z 12617 df-dec 12738 df-uz 12889 df-q 12999 df-rp 13044 df-fz 13563 df-fl 13854 df-mod 13932 df-seq 14067 df-exp 14127 df-cj 15187 df-re 15188 df-im 15189 df-sqrt 15323 df-abs 15324 df-dvds 16344 df-gcd 16586 df-numer 16827 df-denom 16828 df-struct 17240 df-sets 17257 df-slot 17275 df-ndx 17287 df-base 17303 df-ress 17324 df-plusg 17356 df-mulr 17357 df-starv 17358 df-sca 17359 df-vsca 17360 df-ip 17361 df-tset 17362 df-ple 17363 df-ds 17365 df-unif 17366 df-0g 17527 df-imas 17595 df-qus 17596 df-mgm 18731 df-sgrp 18822 df-mnd 18838 df-mhm 18892 df-submnd 18893 df-grp 19061 df-minusg 19062 df-sbg 19063 df-subg 19247 df-ghm 19342 df-cmn 19910 df-abl 19911 df-mgp 20275 df-rng 20289 df-ur 20322 df-ring 20375 df-cring 20376 df-oppr 20479 df-dvdsr 20499 df-unit 20500 df-invr 20530 df-dvr 20543 df-rhm 20614 df-rim 20615 df-nzr 20674 df-subrng 20709 df-subrg 20733 df-rlreg 20857 df-domn 20858 df-idom 20859 df-drng 20893 df-field 20894 df-cnfld 21587 df-zring 21661 df-erl 33696 df-rloc 33697 df-frac 33745

This theorem is used by: (None)

W3C validator