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

Theorem zringfrac 33561
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 𝑄 = (ℂflds ℚ)
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.
StepHypRef Expression
1 zringfrac.1 . . . . . 6 𝑄 = (ℂflds ℚ)
21qdrng 27678 . . . . 5 𝑄 ∈ DivRing
3 drngring 20752 . . . . 5 (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
42, 3ax-mp 5 . . . 4 𝑄 ∈ Ring
5 zringidom 33558 . . . . 5 ring ∈ IDomn
6 id 22 . . . . . . . 8 (ℤring ∈ IDomn → ℤring ∈ IDomn)
76fracfld 33289 . . . . . . 7 (ℤring ∈ IDomn → ( Frac ‘ℤring) ∈ Field)
87fldcrngd 20758 . . . . . 6 (ℤring ∈ IDomn → ( Frac ‘ℤring) ∈ CRing)
98crngringd 20263 . . . . 5 (ℤring ∈ IDomn → ( Frac ‘ℤring) ∈ Ring)
105, 9ax-mp 5 . . . 4 ( Frac ‘ℤring) ∈ Ring
114, 10pm3.2i 470 . . 3 (𝑄 ∈ Ring ∧ ( Frac ‘ℤring) ∈ Ring)
12 ringgrp 20255 . . . . . . 7 (𝑄 ∈ Ring → 𝑄 ∈ Grp)
134, 12ax-mp 5 . . . . . 6 𝑄 ∈ Grp
14 ringgrp 20255 . . . . . . 7 (( Frac ‘ℤring) ∈ Ring → ( Frac ‘ℤring) ∈ Grp)
1510, 14ax-mp 5 . . . . . 6 ( Frac ‘ℤring) ∈ Grp
1613, 15pm3.2i 470 . . . . 5 (𝑄 ∈ Grp ∧ ( Frac ‘ℤring) ∈ Grp)
17 zringfrac.3 . . . . . . 7 𝐹 = (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
18 qnumcl 16773 . . . . . . . . . 10 (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19 qdencl 16774 . . . . . . . . . . . 12 (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
2019nnzd 12637 . . . . . . . . . . 11 (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
2119nnne0d 12313 . . . . . . . . . . 11 (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
2220, 21eldifsnd 4791 . . . . . . . . . 10 (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
2318, 22opelxpd 5727 . . . . . . . . 9 (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24 zringfrac.2 . . . . . . . . . . 11 = (ℤring ~RL (ℤ ∖ {0}))
2524ovexi 7464 . . . . . . . . . 10 ∈ V
2625ecelqsi 8811 . . . . . . . . 9 (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ ((ℤ × (ℤ ∖ {0})) / ))
2723, 26syl 17 . . . . . . . 8 (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ ((ℤ × (ℤ ∖ {0})) / ))
28 zringbas 21481 . . . . . . . . . 10 ℤ = (Base‘ℤring)
29 zring0 21486 . . . . . . . . . 10 0 = (0g‘ℤring)
30 zringmulr 21485 . . . . . . . . . 10 · = (.r‘ℤring)
31 eqid 2734 . . . . . . . . . 10 (-g‘ℤring) = (-g‘ℤring)
32 eqid 2734 . . . . . . . . . 10 (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33 fracval 33285 . . . . . . . . . . 11 ( Frac ‘ℤring) = (ℤring RLocal (RLReg‘ℤring))
346idomdomd 20742 . . . . . . . . . . . . . . 15 (ℤring ∈ IDomn → ℤring ∈ Domn)
355, 34ax-mp 5 . . . . . . . . . . . . . 14 ring ∈ Domn
36 eqid 2734 . . . . . . . . . . . . . . 15 (RLReg‘ℤring) = (RLReg‘ℤring)
3728, 36, 29isdomn6 20730 . . . . . . . . . . . . . 14 (ℤring ∈ Domn ↔ (ℤring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤring)))
3835, 37mpbi 230 . . . . . . . . . . . . 13 (ℤring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤring))
3938simpri 485 . . . . . . . . . . . 12 (ℤ ∖ {0}) = (RLReg‘ℤring)
4039oveq2i 7441 . . . . . . . . . . 11 (ℤring RLocal (ℤ ∖ {0})) = (ℤring RLocal (RLReg‘ℤring))
4133, 40eqtr4i 2765 . . . . . . . . . 10 ( Frac ‘ℤring) = (ℤring RLocal (ℤ ∖ {0}))
425a1i 11 . . . . . . . . . 10 (⊤ → ℤring ∈ IDomn)
43 difssd 4146 . . . . . . . . . 10 (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
4428, 29, 30, 31, 32, 41, 24, 42, 43rlocbas 33253 . . . . . . . . 9 (⊤ → ((ℤ × (ℤ ∖ {0})) / ) = (Base‘( Frac ‘ℤring)))
4544mptru 1543 . . . . . . . 8 ((ℤ × (ℤ ∖ {0})) / ) = (Base‘( Frac ‘ℤring))
4627, 45eleqtrdi 2848 . . . . . . 7 (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ (Base‘( Frac ‘ℤring)))
4717, 46fmpti 7131 . . . . . 6 𝐹:ℚ⟶(Base‘( Frac ‘ℤring))
48 ecexg 8747 . . . . . . . . . . . 12 ( ∈ V → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ V)
4925, 48ax-mp 5 . . . . . . . . . . 11 [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ V
5017fvmpt2 7026 . . . . . . . . . . 11 ((𝑞 ∈ ℚ ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ V) → (𝐹𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
5149, 50mpan2 691 . . . . . . . . . 10 (𝑞 ∈ ℚ → (𝐹𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
5251adantr 480 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹𝑞) = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
53 fveq2 6906 . . . . . . . . . . . . 13 (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54 fveq2 6906 . . . . . . . . . . . . 13 (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
5553, 54opeq12d 4885 . . . . . . . . . . . 12 (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
5655eceq1d 8783 . . . . . . . . . . 11 (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] )
5756, 17, 27fvmpt3 7019 . . . . . . . . . 10 (𝑝 ∈ ℚ → (𝐹𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] )
5857adantl 481 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] )
5952, 58oveq12d 7448 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹𝑞)(+g‘(ℤring RLocal (ℤ ∖ {0})))(𝐹𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
6041fveq2i 6909 . . . . . . . . . 10 (+g‘( Frac ‘ℤring)) = (+g‘(ℤring RLocal (ℤ ∖ {0})))
6160oveqi 7443 . . . . . . . . 9 ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)) = ((𝐹𝑞)(+g‘(ℤring RLocal (ℤ ∖ {0})))(𝐹𝑝))
6261a1i 11 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)) = ((𝐹𝑞)(+g‘(ℤring RLocal (ℤ ∖ {0})))(𝐹𝑝)))
63 fveq2 6906 . . . . . . . . . . . . 13 (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64 fveq2 6906 . . . . . . . . . . . . 13 (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
6563, 64opeq12d 4885 . . . . . . . . . . . 12 (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
6665eceq1d 8783 . . . . . . . . . . 11 (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑢), (denom‘𝑢)⟩] )
6766cbvmptv 5260 . . . . . . . . . 10 (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] )
6817, 67eqtri 2762 . . . . . . . . 9 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] )
69 zring1 21487 . . . . . . . . . . . . 13 1 = (1r‘ℤring)
705a1i 11 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤring ∈ IDomn)
7170idomcringd 20743 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤring ∈ CRing)
7235a1i 11 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤring ∈ Domn)
73 eqid 2734 . . . . . . . . . . . . . . . 16 (mulGrp‘ℤring) = (mulGrp‘ℤring)
7428, 29, 73isdomn3 20731 . . . . . . . . . . . . . . 15 (ℤring ∈ Domn ↔ (ℤring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring))))
7572, 74sylib 218 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring))))
7675simprd 495 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring)))
7728, 29, 69, 30, 31, 32, 24, 71, 76erler 33251 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → Er (ℤ × (ℤ ∖ {0})))
78 qcn 13002 . . . . . . . . . . . . . . . . 17 (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
7978adantr 480 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80 qcn 13002 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
8180adantl 481 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
8279, 81addcld 11277 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83 qaddcl 13004 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84 qdencl 16774 . . . . . . . . . . . . . . . . 17 ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
8583, 84syl 17 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
8685nncnd 12279 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
8719adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
8887nncnd 12279 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89 qdencl 16774 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
9089adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
9190nncnd 12279 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
9288, 91mulcld 11278 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
9382, 86, 92mul32d 11468 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94 qmuldeneqnum 16780 . . . . . . . . . . . . . . . 16 ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
9583, 94syl 17 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
9695oveq1d 7445 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
9779, 88, 91mulassd 11281 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98 qmuldeneqnum 16780 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
9998adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
10099oveq1d 7445 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
10197, 100eqtr3d 2776 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
10281, 91, 88mulassd 11281 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103 qmuldeneqnum 16780 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104103adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105104oveq1d 7445 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
10691, 88mulcomd 11279 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107106oveq2d 7446 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108102, 105, 1073eqtr3rd 2783 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109101, 108oveq12d 7448 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
11079, 92, 81, 109joinlmuladdmuld 11285 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111110oveq1d 7445 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
11293, 96, 1113eqtr3d 2782 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
11339oveq2i 7441 . . . . . . . . . . . . . . 15 (ℤring ~RL (ℤ ∖ {0})) = (ℤring ~RL (RLReg‘ℤring))
11424, 113eqtri 2762 . . . . . . . . . . . . . 14 = (ℤring ~RL (RLReg‘ℤring))
115 qnumcl 16773 . . . . . . . . . . . . . . 15 ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
11683, 115syl 17 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
11718adantr 480 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
11889nnzd 12637 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119118adantl 481 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120117, 119zmulcld 12725 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121 qnumcl 16773 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122121adantl 481 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
12320adantr 480 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124122, 123zmulcld 12725 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125120, 124zaddcld 12723 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
12685nnzd 12637 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
12785nnne0d 12313 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128126, 127eldifsnd 4791 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129128, 39eleqtrdi 2848 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤring))
130123, 119zmulcld 12725 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
13187, 90nnmulcld 12316 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132131nnne0d 12313 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133130, 132eldifsnd 4791 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134133, 39eleqtrdi 2848 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤring))
13528, 30, 114, 71, 116, 125, 129, 134fracerl 33287 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩ ↔ ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝)))))
136112, 135mpbird 257 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩ ⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩)
13777, 136erthi 8796 . . . . . . . . . . 11 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] )
138137adantr 480 . . . . . . . . . 10 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] )
139 fveq2 6906 . . . . . . . . . . . . 13 (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140 fveq2 6906 . . . . . . . . . . . . 13 (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141139, 140opeq12d 4885 . . . . . . . . . . . 12 (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142141adantl 481 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143142eceq1d 8783 . . . . . . . . . 10 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] )
144 zringplusg 21482 . . . . . . . . . . 11 + = (+g‘ℤring)
145 eqid 2734 . . . . . . . . . . 11 (ℤring RLocal (ℤ ∖ {0})) = (ℤring RLocal (ℤ ∖ {0}))
146 zringcrng 21476 . . . . . . . . . . . 12 ring ∈ CRing
147146a1i 11 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ℤring ∈ CRing)
14835, 74mpbi 230 . . . . . . . . . . . . 13 (ℤring ∈ Ring ∧ (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring)))
149148simpri 485 . . . . . . . . . . . 12 (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring))
150149a1i 11 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring)))
151117adantr 480 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑞) ∈ ℤ)
152122adantr 480 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑝) ∈ ℤ)
15322adantr 480 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
154153adantr 480 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑞) ∈ (ℤ ∖ {0}))
15589nnne0d 12313 . . . . . . . . . . . . . 14 (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156118, 155eldifsnd 4791 . . . . . . . . . . . . 13 (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157156adantl 481 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158157adantr 480 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159 eqid 2734 . . . . . . . . . . 11 (+g‘(ℤring RLocal (ℤ ∖ {0}))) = (+g‘(ℤring RLocal (ℤ ∖ {0})))
16028, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159rlocaddval 33254 . . . . . . . . . 10 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] )
161138, 143, 1603eqtr4d 2784 . . . . . . . . 9 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
162 ovexd 7465 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) ∈ V)
16368, 161, 83, 162fvmptd2 7023 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
16459, 62, 1633eqtr4rd 2785 . . . . . . 7 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)))
165164rgen2 3196 . . . . . 6 𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝))
16647, 165pm3.2i 470 . . . . 5 (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)))
1671qrngbas 27677 . . . . . 6 ℚ = (Base‘𝑄)
168 eqid 2734 . . . . . 6 (Base‘( Frac ‘ℤring)) = (Base‘( Frac ‘ℤring))
169 qex 13000 . . . . . . 7 ℚ ∈ V
170 cnfldadd 21387 . . . . . . . 8 + = (+g‘ℂfld)
1711, 170ressplusg 17335 . . . . . . 7 (ℚ ∈ V → + = (+g𝑄))
172169, 171ax-mp 5 . . . . . 6 + = (+g𝑄)
173 eqid 2734 . . . . . 6 (+g‘( Frac ‘ℤring)) = (+g‘( Frac ‘ℤring))
174167, 168, 172, 173isghm 19245 . . . . 5 (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤring)) ↔ ((𝑄 ∈ Grp ∧ ( Frac ‘ℤring) ∈ Grp) ∧ (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)))))
17516, 166, 174mpbir2an 711 . . . 4 𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤring))
176 eqid 2734 . . . . . . . 8 (mulGrp‘𝑄) = (mulGrp‘𝑄)
177176ringmgp 20256 . . . . . . 7 (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
1784, 177ax-mp 5 . . . . . 6 (mulGrp‘𝑄) ∈ Mnd
179 eqid 2734 . . . . . . . 8 (mulGrp‘( Frac ‘ℤring)) = (mulGrp‘( Frac ‘ℤring))
180179ringmgp 20256 . . . . . . 7 (( Frac ‘ℤring) ∈ Ring → (mulGrp‘( Frac ‘ℤring)) ∈ Mnd)
18110, 180ax-mp 5 . . . . . 6 (mulGrp‘( Frac ‘ℤring)) ∈ Mnd
182178, 181pm3.2i 470 . . . . 5 ((mulGrp‘𝑄) ∈ Mnd ∧ (mulGrp‘( Frac ‘ℤring)) ∈ Mnd)
183 eqid 2734 . . . . . . . . . 10 (.r‘(ℤring RLocal (ℤ ∖ {0}))) = (.r‘(ℤring RLocal (ℤ ∖ {0})))
18428, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183rlocmulval 33255 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (.r‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] )
18579, 81mulcld 11278 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186 qmulcl 13006 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187 qdencl 16774 . . . . . . . . . . . . . . . 16 ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188186, 187syl 17 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189188nncnd 12279 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190185, 189, 92mul32d 11468 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
19179, 81, 88, 91mul4d 11470 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192191oveq1d 7445 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193190, 192eqtrd 2774 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194 qmuldeneqnum 16780 . . . . . . . . . . . . . 14 ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195186, 194syl 17 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196195oveq1d 7445 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
19799, 104oveq12d 7448 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198197oveq1d 7445 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199193, 196, 1983eqtr3rd 2783 . . . . . . . . . . 11 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200117, 122zmulcld 12725 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201 qnumcl 16773 . . . . . . . . . . . . 13 ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202186, 201syl 17 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203188nnzd 12637 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204188nnne0d 12313 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205203, 204eldifsnd 4791 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206205, 39eleqtrdi 2848 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤring))
20728, 30, 114, 71, 200, 202, 134, 206fracerl 33287 . . . . . . . . . . 11 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩ ↔ (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))))
208199, 207mpbird 257 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩ ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
20977, 208erthi 8796 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
210184, 209eqtrd 2774 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (.r‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
21141fveq2i 6909 . . . . . . . . . 10 (.r‘( Frac ‘ℤring)) = (.r‘(ℤring RLocal (ℤ ∖ {0})))
212211a1i 11 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (.r‘( Frac ‘ℤring)) = (.r‘(ℤring RLocal (ℤ ∖ {0}))))
213212, 52, 58oveq123d 7451 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (.r‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
214 fveq2 6906 . . . . . . . . . . 11 (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215 fveq2 6906 . . . . . . . . . . 11 (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216214, 215opeq12d 4885 . . . . . . . . . 10 (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217216eceq1d 8783 . . . . . . . . 9 (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
218 ecexg 8747 . . . . . . . . . 10 ( ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∈ V)
21925, 218mp1i 13 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∈ V)
22068, 217, 186, 219fvmptd3 7038 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
221210, 213, 2203eqtr4rd 2785 . . . . . . 7 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)))
222221rgen2 3196 . . . . . 6 𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝))
223 zssq 12995 . . . . . . . 8 ℤ ⊆ ℚ
224 1z 12644 . . . . . . . 8 1 ∈ ℤ
225223, 224sselii 3991 . . . . . . 7 1 ∈ ℚ
226 fveq2 6906 . . . . . . . . . . 11 (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227 1zzd 12645 . . . . . . . . . . . . 13 (ℤring ∈ IDomn → 1 ∈ ℤ)
228227znumd 32818 . . . . . . . . . . . 12 (ℤring ∈ IDomn → (numer‘1) = 1)
2295, 228ax-mp 5 . . . . . . . . . . 11 (numer‘1) = 1
230226, 229eqtrdi 2790 . . . . . . . . . 10 (𝑞 = 1 → (numer‘𝑞) = 1)
231 fveq2 6906 . . . . . . . . . . 11 (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232227zdend 32819 . . . . . . . . . . . 12 (ℤring ∈ IDomn → (denom‘1) = 1)
2335, 232ax-mp 5 . . . . . . . . . . 11 (denom‘1) = 1
234231, 233eqtrdi 2790 . . . . . . . . . 10 (𝑞 = 1 → (denom‘𝑞) = 1)
235230, 234opeq12d 4885 . . . . . . . . 9 (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236235eceq1d 8783 . . . . . . . 8 (𝑞 = 1 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨1, 1⟩] )
237236, 17, 49fvmpt3i 7020 . . . . . . 7 (1 ∈ ℚ → (𝐹‘1) = [⟨1, 1⟩] )
238225, 237ax-mp 5 . . . . . 6 (𝐹‘1) = [⟨1, 1⟩]
23947, 222, 2383pm3.2i 1338 . . . . 5 (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] )
240176, 167mgpbas 20157 . . . . . 6 ℚ = (Base‘(mulGrp‘𝑄))
241179, 168mgpbas 20157 . . . . . 6 (Base‘( Frac ‘ℤring)) = (Base‘(mulGrp‘( Frac ‘ℤring)))
242 cnfldmul 21389 . . . . . . . . 9 · = (.r‘ℂfld)
2431, 242ressmulr 17352 . . . . . . . 8 (ℚ ∈ V → · = (.r𝑄))
244169, 243ax-mp 5 . . . . . . 7 · = (.r𝑄)
245176, 244mgpplusg 20155 . . . . . 6 · = (+g‘(mulGrp‘𝑄))
246 eqid 2734 . . . . . . 7 (.r‘( Frac ‘ℤring)) = (.r‘( Frac ‘ℤring))
247179, 246mgpplusg 20155 . . . . . 6 (.r‘( Frac ‘ℤring)) = (+g‘(mulGrp‘( Frac ‘ℤring)))
2481qrng1 27680 . . . . . . 7 1 = (1r𝑄)
249176, 248ringidval 20200 . . . . . 6 1 = (0g‘(mulGrp‘𝑄))
250146a1i 11 . . . . . . . . 9 (ℤring ∈ IDomn → ℤring ∈ CRing)
251149a1i 11 . . . . . . . . 9 (ℤring ∈ IDomn → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring)))
252 eqid 2734 . . . . . . . . 9 [⟨1, 1⟩] = [⟨1, 1⟩]
25329, 69, 41, 24, 250, 251, 252rloc1r 33258 . . . . . . . 8 (ℤring ∈ IDomn → [⟨1, 1⟩] = (1r‘( Frac ‘ℤring)))
2545, 253ax-mp 5 . . . . . . 7 [⟨1, 1⟩] = (1r‘( Frac ‘ℤring))
255179, 254ringidval 20200 . . . . . 6 [⟨1, 1⟩] = (0g‘(mulGrp‘( Frac ‘ℤring)))
256240, 241, 245, 247, 249, 255ismhm 18810 . . . . 5 (𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤring))) ↔ (((mulGrp‘𝑄) ∈ Mnd ∧ (mulGrp‘( Frac ‘ℤring)) ∈ Mnd) ∧ (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] )))
257182, 239, 256mpbir2an 711 . . . 4 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤring)))
258175, 257pm3.2i 470 . . 3 (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤring))))
259176, 179isrhm 20494 . . 3 (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤring)) ↔ ((𝑄 ∈ Ring ∧ ( Frac ‘ℤring) ∈ Ring) ∧ (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac ‘ℤring))))))
26011, 258, 259mpbir2an 711 . 2 𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤring))
26146rgen 3060 . . . 4 𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ (Base‘( Frac ‘ℤring))
262117zcnd 12720 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263122zcnd 12720 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
26421adantr 480 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265155adantl 481 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266262, 88, 263, 91, 264, 265divmuleqd 12086 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267153, 39eleqtrdi 2848 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤring))
268157, 39eleqtrdi 2848 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤring))
26928, 30, 114, 71, 117, 122, 267, 268fracerl 33287 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
27023adantr 480 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
27177, 270erth 8794 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
272266, 269, 2713bitr2rd 308 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ↔ ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝))))
273272biimpa 476 . . . . . . 7 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → ((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)))
274 qeqnumdivden 16779 . . . . . . . 8 (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275274ad2antrr 726 . . . . . . 7 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276 qeqnumdivden 16779 . . . . . . . 8 (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277276ad2antlr 727 . . . . . . 7 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278273, 275, 2773eqtr4d 2784 . . . . . 6 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → 𝑞 = 𝑝)
279278ex 412 . . . . 5 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] 𝑞 = 𝑝))
280279rgen2 3196 . . . 4 𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] 𝑞 = 𝑝)
28117, 56f1mpt 7280 . . . 4 (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ (Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] 𝑞 = 𝑝)))
282261, 280, 281mpbir2an 711 . . 3 𝐹:ℚ–1-1→(Base‘( Frac ‘ℤring))
283 fveq2 6906 . . . . . . . . . 10 (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284 fveq2 6906 . . . . . . . . . 10 (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285283, 284opeq12d 4885 . . . . . . . . 9 (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286285eceq1d 8783 . . . . . . . 8 (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] )
287286eqeq2d 2745 . . . . . . 7 (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ))
288 simpllr 776 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑎 ∈ ℤ)
289223, 288sselid 3992 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑎 ∈ ℚ)
290 simplr 769 . . . . . . . . . 10 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ∈ (ℤ ∖ {0}))
291290eldifad 3974 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ∈ ℤ)
292223, 291sselid 3992 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ∈ ℚ)
293 eldifsni 4794 . . . . . . . . 9 (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294290, 293syl 17 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ≠ 0)
295 qdivcl 13009 . . . . . . . 8 ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296289, 292, 294, 295syl3anc 1370 . . . . . . 7 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → (𝑎 / 𝑏) ∈ ℚ)
297 simpr 484 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑧 = [⟨𝑎, 𝑏⟩] )
298146a1i 11 . . . . . . . . . 10 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → ℤring ∈ CRing)
299149a1i 11 . . . . . . . . . 10 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring)))
30028, 29, 69, 30, 31, 32, 24, 298, 299erler 33251 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → Er (ℤ × (ℤ ∖ {0})))
301 simpl 482 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302301zcnd 12720 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303 eldifi 4140 . . . . . . . . . . . . . . . 16 (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304303adantl 481 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305304zcnd 12720 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306293adantl 481 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307302, 305, 306divcld 12040 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308223, 301sselid 3992 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309223, 304sselid 3992 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310308, 309, 306, 295syl3anc 1370 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311 qdencl 16774 . . . . . . . . . . . . . . 15 ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312310, 311syl 17 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313312nncnd 12279 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314307, 313, 305mul32d 11468 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315 qmuldeneqnum 16780 . . . . . . . . . . . . . 14 ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316310, 315syl 17 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317316oveq1d 7445 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318302, 305, 306divcan1d 12041 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319318oveq1d 7445 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320314, 317, 3193eqtr3rd 2783 . . . . . . . . . . 11 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321146a1i 11 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤring ∈ CRing)
322 qnumcl 16773 . . . . . . . . . . . . 13 ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323310, 322syl 17 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324 simpr 484 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325324, 39eleqtrdi 2848 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤring))
326312nnzd 12637 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327312nnne0d 12313 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328326, 327eldifsnd 4791 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329328, 39eleqtrdi 2848 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤring))
33028, 30, 114, 321, 301, 323, 325, 329fracerl 33287 . . . . . . . . . . 11 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (⟨𝑎, 𝑏 ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩ ↔ (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏)))
331320, 330mpbird 257 . . . . . . . . . 10 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ⟨𝑎, 𝑏 ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
332331ad4ant23 753 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏 ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
333300, 332erthi 8796 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] )
334297, 333eqtrd 2774 . . . . . . 7 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] )
335287, 296, 334rspcedvdw 3624 . . . . . 6 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
33645eleq2i 2830 . . . . . . . 8 (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤring)))
337336biimpri 228 . . . . . . 7 (𝑧 ∈ (Base‘( Frac ‘ℤring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ))
338337elrlocbasi 33252 . . . . . 6 (𝑧 ∈ (Base‘( Frac ‘ℤring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] )
339335, 338r19.29vva 3213 . . . . 5 (𝑧 ∈ (Base‘( Frac ‘ℤring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
340339rgen 3060 . . . 4 𝑧 ∈ (Base‘( Frac ‘ℤring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩]
34117fompt 7137 . . . 4 (𝐹:ℚ–onto→(Base‘( Frac ‘ℤring)) ↔ (∀𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ (Base‘( Frac ‘ℤring)) ∧ ∀𝑧 ∈ (Base‘( Frac ‘ℤring))∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] ))
342261, 340, 341mpbir2an 711 . . 3 𝐹:ℚ–onto→(Base‘( Frac ‘ℤring))
343 df-f1o 6569 . . 3 (𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤring)) ↔ (𝐹:ℚ–1-1→(Base‘( Frac ‘ℤring)) ∧ 𝐹:ℚ–onto→(Base‘( Frac ‘ℤring))))
344282, 342, 343mpbir2an 711 . 2 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤring))
345167, 168isrim 20508 . 2 (𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤring)) ↔ (𝐹 ∈ (𝑄 RingHom ( Frac ‘ℤring)) ∧ 𝐹:ℚ–1-1-onto→(Base‘( Frac ‘ℤring))))
346260, 344, 345mpbir2an 711 1 𝐹 ∈ (𝑄 RingIso ( Frac ‘ℤring))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 395  w3a 1086   = wceq 1536  wtru 1537  wcel 2105  wne 2937  wral 3058  wrex 3067  Vcvv 3477  cdif 3959  {csn 4630  cop 4636   class class class wbr 5147  cmpt 5230   × cxp 5686  wf 6558  1-1wf1 6559  ontowfo 6560  1-1-ontowf1o 6561  cfv 6562  (class class class)co 7430  [cec 8741   / cqs 8742  cc 11150  0cc0 11152  1c1 11153   + caddc 11155   · cmul 11157   / cdiv 11917  cn 12263  cz 12610  cq 12987  numercnumer 16766  denomcdenom 16767  Basecbs 17244  s cress 17273  +gcplusg 17297  .rcmulr 17298  Mndcmnd 18759   MndHom cmhm 18806  SubMndcsubmnd 18807  Grpcgrp 18963  -gcsg 18965   GrpHom cghm 19242  mulGrpcmgp 20151  1rcur 20198  Ringcrg 20250  CRingccrg 20251   RingHom crh 20485   RingIso crs 20486  NzRingcnzr 20528  RLRegcrlreg 20707  Domncdomn 20708  IDomncidom 20709  DivRingcdr 20745  fldccnfld 21381  ringczring 21474   ~RL cerl 33239   RLocal crloc 33240   Frac cfrac 33283
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1791  ax-4 1805  ax-5 1907  ax-6 1964  ax-7 2004  ax-8 2107  ax-9 2115  ax-10 2138  ax-11 2154  ax-12 2174  ax-ext 2705  ax-rep 5284  ax-sep 5301  ax-nul 5311  ax-pow 5370  ax-pr 5437  ax-un 7753  ax-cnex 11208  ax-resscn 11209  ax-1cn 11210  ax-icn 11211  ax-addcl 11212  ax-addrcl 11213  ax-mulcl 11214  ax-mulrcl 11215  ax-mulcom 11216  ax-addass 11217  ax-mulass 11218  ax-distr 11219  ax-i2m1 11220  ax-1ne0 11221  ax-1rid 11222  ax-rnegex 11223  ax-rrecex 11224  ax-cnre 11225  ax-pre-lttri 11226  ax-pre-lttrn 11227  ax-pre-ltadd 11228  ax-pre-mulgt0 11229  ax-pre-sup 11230  ax-addf 11231  ax-mulf 11232
This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3or 1087  df-3an 1088  df-tru 1539  df-fal 1549  df-ex 1776  df-nf 1780  df-sb 2062  df-mo 2537  df-eu 2566  df-clab 2712  df-cleq 2726  df-clel 2813  df-nfc 2889  df-ne 2938  df-nel 3044  df-ral 3059  df-rex 3068  df-rmo 3377  df-reu 3378  df-rab 3433  df-v 3479  df-sbc 3791  df-csb 3908  df-dif 3965  df-un 3967  df-in 3969  df-ss 3979  df-pss 3982  df-nul 4339  df-if 4531  df-pw 4606  df-sn 4631  df-pr 4633  df-tp 4635  df-op 4637  df-uni 4912  df-iun 4997  df-br 5148  df-opab 5210  df-mpt 5231  df-tr 5265  df-id 5582  df-eprel 5588  df-po 5596  df-so 5597  df-fr 5640  df-we 5642  df-xp 5694  df-rel 5695  df-cnv 5696  df-co 5697  df-dm 5698  df-rn 5699  df-res 5700  df-ima 5701  df-pred 6322  df-ord 6388  df-on 6389  df-lim 6390  df-suc 6391  df-iota 6515  df-fun 6564  df-fn 6565  df-f 6566  df-f1 6567  df-fo 6568  df-f1o 6569  df-fv 6570  df-riota 7387  df-ov 7433  df-oprab 7434  df-mpo 7435  df-om 7887  df-1st 8012  df-2nd 8013  df-tpos 8249  df-frecs 8304  df-wrecs 8335  df-recs 8409  df-rdg 8448  df-1o 8504  df-er 8743  df-ec 8745  df-qs 8749  df-map 8866  df-en 8984  df-dom 8985  df-sdom 8986  df-fin 8987  df-sup 9479  df-inf 9480  df-pnf 11294  df-mnf 11295  df-xr 11296  df-ltxr 11297  df-le 11298  df-sub 11491  df-neg 11492  df-div 11918  df-nn 12264  df-2 12326  df-3 12327  df-4 12328  df-5 12329  df-6 12330  df-7 12331  df-8 12332  df-9 12333  df-n0 12524  df-z 12611  df-dec 12731  df-uz 12876  df-q 12988  df-rp 13032  df-fz 13544  df-fl 13828  df-mod 13906  df-seq 14039  df-exp 14099  df-cj 15134  df-re 15135  df-im 15136  df-sqrt 15270  df-abs 15271  df-dvds 16287  df-gcd 16528  df-numer 16768  df-denom 16769  df-struct 17180  df-sets 17197  df-slot 17215  df-ndx 17227  df-base 17245  df-ress 17274  df-plusg 17310  df-mulr 17311  df-starv 17312  df-sca 17313  df-vsca 17314  df-ip 17315  df-tset 17316  df-ple 17317  df-ds 17319  df-unif 17320  df-0g 17487  df-imas 17554  df-qus 17555  df-mgm 18665  df-sgrp 18744  df-mnd 18760  df-mhm 18808  df-submnd 18809  df-grp 18966  df-minusg 18967  df-sbg 18968  df-subg 19153  df-ghm 19243  df-cmn 19814  df-abl 19815  df-mgp 20152  df-rng 20170  df-ur 20199  df-ring 20252  df-cring 20253  df-oppr 20350  df-dvdsr 20373  df-unit 20374  df-invr 20404  df-dvr 20417  df-rhm 20488  df-rim 20489  df-nzr 20529  df-subrng 20562  df-subrg 20586  df-rlreg 20710  df-domn 20711  df-idom 20712  df-drng 20747  df-field 20748  df-cnfld 21382  df-zring 21475  df-erl 33241  df-rloc 33242  df-frac 33284
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator