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 33583
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 27665 . . . . 5 𝑄 ∈ DivRing
3 drngring 20737 . . . . 5 (𝑄 ∈ DivRing → 𝑄 ∈ Ring)
42, 3ax-mp 5 . . . 4 𝑄 ∈ Ring
5 zringidom 33580 . . . . 5 ring ∈ IDomn
6 id 22 . . . . . . . 8 (ℤring ∈ IDomn → ℤring ∈ IDomn)
76fracfld 33311 . . . . . . 7 (ℤring ∈ IDomn → ( Frac ‘ℤring) ∈ Field)
87fldcrngd 20743 . . . . . 6 (ℤring ∈ IDomn → ( Frac ‘ℤring) ∈ CRing)
98crngringd 20244 . . . . 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 20236 . . . . . . 7 (𝑄 ∈ Ring → 𝑄 ∈ Grp)
134, 12ax-mp 5 . . . . . 6 𝑄 ∈ Grp
14 ringgrp 20236 . . . . . . 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 16778 . . . . . . . . . 10 (𝑞 ∈ ℚ → (numer‘𝑞) ∈ ℤ)
19 qdencl 16779 . . . . . . . . . . . 12 (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℕ)
2019nnzd 12642 . . . . . . . . . . 11 (𝑞 ∈ ℚ → (denom‘𝑞) ∈ ℤ)
2119nnne0d 12317 . . . . . . . . . . 11 (𝑞 ∈ ℚ → (denom‘𝑞) ≠ 0)
2220, 21eldifsnd 4786 . . . . . . . . . 10 (𝑞 ∈ ℚ → (denom‘𝑞) ∈ (ℤ ∖ {0}))
2318, 22opelxpd 5723 . . . . . . . . 9 (𝑞 ∈ ℚ → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
24 zringfrac.2 . . . . . . . . . . 11 = (ℤring ~RL (ℤ ∖ {0}))
2524ovexi 7466 . . . . . . . . . 10 ∈ V
2625ecelqsi 8814 . . . . . . . . 9 (⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ ((ℤ × (ℤ ∖ {0})) / ))
2723, 26syl 17 . . . . . . . 8 (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ ((ℤ × (ℤ ∖ {0})) / ))
28 zringbas 21465 . . . . . . . . . 10 ℤ = (Base‘ℤring)
29 zring0 21470 . . . . . . . . . 10 0 = (0g‘ℤring)
30 zringmulr 21469 . . . . . . . . . 10 · = (.r‘ℤring)
31 eqid 2736 . . . . . . . . . 10 (-g‘ℤring) = (-g‘ℤring)
32 eqid 2736 . . . . . . . . . 10 (ℤ × (ℤ ∖ {0})) = (ℤ × (ℤ ∖ {0}))
33 fracval 33307 . . . . . . . . . . 11 ( Frac ‘ℤring) = (ℤring RLocal (RLReg‘ℤring))
346idomdomd 20727 . . . . . . . . . . . . . . 15 (ℤring ∈ IDomn → ℤring ∈ Domn)
355, 34ax-mp 5 . . . . . . . . . . . . . 14 ring ∈ Domn
36 eqid 2736 . . . . . . . . . . . . . . 15 (RLReg‘ℤring) = (RLReg‘ℤring)
3728, 36, 29isdomn6 20715 . . . . . . . . . . . . . 14 (ℤring ∈ Domn ↔ (ℤring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤring)))
3835, 37mpbi 230 . . . . . . . . . . . . 13 (ℤring ∈ NzRing ∧ (ℤ ∖ {0}) = (RLReg‘ℤring))
3938simpri 485 . . . . . . . . . . . 12 (ℤ ∖ {0}) = (RLReg‘ℤring)
4039oveq2i 7443 . . . . . . . . . . 11 (ℤring RLocal (ℤ ∖ {0})) = (ℤring RLocal (RLReg‘ℤring))
4133, 40eqtr4i 2767 . . . . . . . . . 10 ( Frac ‘ℤring) = (ℤring RLocal (ℤ ∖ {0}))
425a1i 11 . . . . . . . . . 10 (⊤ → ℤring ∈ IDomn)
43 difssd 4136 . . . . . . . . . 10 (⊤ → (ℤ ∖ {0}) ⊆ ℤ)
4428, 29, 30, 31, 32, 41, 24, 42, 43rlocbas 33272 . . . . . . . . 9 (⊤ → ((ℤ × (ℤ ∖ {0})) / ) = (Base‘( Frac ‘ℤring)))
4544mptru 1546 . . . . . . . 8 ((ℤ × (ℤ ∖ {0})) / ) = (Base‘( Frac ‘ℤring))
4627, 45eleqtrdi 2850 . . . . . . 7 (𝑞 ∈ ℚ → [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ (Base‘( Frac ‘ℤring)))
4717, 46fmpti 7131 . . . . . 6 𝐹:ℚ⟶(Base‘( Frac ‘ℤring))
48 ecexg 8750 . . . . . . . . . . . 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 6905 . . . . . . . . . . . . 13 (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝))
54 fveq2 6905 . . . . . . . . . . . . 13 (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝))
5553, 54opeq12d 4880 . . . . . . . . . . . 12 (𝑞 = 𝑝 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑝), (denom‘𝑝)⟩)
5655eceq1d 8786 . . . . . . . . . . 11 (𝑞 = 𝑝 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] )
5756, 17, 27fvmpt3 7019 . . . . . . . . . 10 (𝑝 ∈ ℚ → (𝐹𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] )
5857adantl 481 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹𝑝) = [⟨(numer‘𝑝), (denom‘𝑝)⟩] )
5952, 58oveq12d 7450 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹𝑞)(+g‘(ℤring RLocal (ℤ ∖ {0})))(𝐹𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
6041fveq2i 6908 . . . . . . . . . 10 (+g‘( Frac ‘ℤring)) = (+g‘(ℤring RLocal (ℤ ∖ {0})))
6160oveqi 7445 . . . . . . . . 9 ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)) = ((𝐹𝑞)(+g‘(ℤring RLocal (ℤ ∖ {0})))(𝐹𝑝))
6261a1i 11 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)) = ((𝐹𝑞)(+g‘(ℤring RLocal (ℤ ∖ {0})))(𝐹𝑝)))
63 fveq2 6905 . . . . . . . . . . . . 13 (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢))
64 fveq2 6905 . . . . . . . . . . . . 13 (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢))
6563, 64opeq12d 4880 . . . . . . . . . . . 12 (𝑞 = 𝑢 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘𝑢), (denom‘𝑢)⟩)
6665eceq1d 8786 . . . . . . . . . . 11 (𝑞 = 𝑢 → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑢), (denom‘𝑢)⟩] )
6766cbvmptv 5254 . . . . . . . . . 10 (𝑞 ∈ ℚ ↦ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ) = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] )
6817, 67eqtri 2764 . . . . . . . . 9 𝐹 = (𝑢 ∈ ℚ ↦ [⟨(numer‘𝑢), (denom‘𝑢)⟩] )
69 zring1 21471 . . . . . . . . . . . . 13 1 = (1r‘ℤring)
705a1i 11 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤring ∈ IDomn)
7170idomcringd 20728 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤring ∈ CRing)
7235a1i 11 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ℤring ∈ Domn)
73 eqid 2736 . . . . . . . . . . . . . . . 16 (mulGrp‘ℤring) = (mulGrp‘ℤring)
7428, 29, 73isdomn3 20716 . . . . . . . . . . . . . . 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 33270 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → Er (ℤ × (ℤ ∖ {0})))
78 qcn 13006 . . . . . . . . . . . . . . . . 17 (𝑞 ∈ ℚ → 𝑞 ∈ ℂ)
7978adantr 480 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈ ℂ)
80 qcn 13006 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℚ → 𝑝 ∈ ℂ)
8180adantl 481 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈ ℂ)
8279, 81addcld 11281 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ)
83 qaddcl 13008 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ)
84 qdencl 16779 . . . . . . . . . . . . . . . . 17 ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
8583, 84syl 17 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℕ)
8685nncnd 12283 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℂ)
8719adantr 480 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℕ)
8887nncnd 12283 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℂ)
89 qdencl 16779 . . . . . . . . . . . . . . . . . 18 (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℕ)
9089adantl 481 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℕ)
9190nncnd 12283 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℂ)
9288, 91mulcld 11282 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℂ)
9382, 86, 92mul32d 11472 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))))
94 qmuldeneqnum 16785 . . . . . . . . . . . . . . . 16 ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
9583, 94syl 17 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝)))
9695oveq1d 7447 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
9779, 88, 91mulassd 11285 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝))))
98 qmuldeneqnum 16785 . . . . . . . . . . . . . . . . . . . 20 (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
9998adantr 480 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞))
10099oveq1d 7447 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝)))
10197, 100eqtr3d 2778 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝)))
10281, 91, 88mulassd 11285 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞))))
103 qmuldeneqnum 16785 . . . . . . . . . . . . . . . . . . . 20 (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
104103adantl 481 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝))
105104oveq1d 7447 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞)))
10691, 88mulcomd 11283 . . . . . . . . . . . . . . . . . . 19 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑝) · (denom‘𝑞)) = ((denom‘𝑞) · (denom‘𝑝)))
107106oveq2d 7448 . . . . . . . . . . . . . . . . . 18 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝))))
108102, 105, 1073eqtr3rd 2785 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞)))
109101, 108oveq12d 7450 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
11079, 92, 81, 109joinlmuladdmuld 11289 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))))
111110oveq1d 7447 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
11293, 96, 1113eqtr3d 2784 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝))))
11339oveq2i 7443 . . . . . . . . . . . . . . 15 (ℤring ~RL (ℤ ∖ {0})) = (ℤring ~RL (RLReg‘ℤring))
11424, 113eqtri 2764 . . . . . . . . . . . . . 14 = (ℤring ~RL (RLReg‘ℤring))
115 qnumcl 16778 . . . . . . . . . . . . . . 15 ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
11683, 115syl 17 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 + 𝑝)) ∈ ℤ)
11718adantr 480 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℤ)
11889nnzd 12642 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℚ → (denom‘𝑝) ∈ ℤ)
119118adantl 481 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ ℤ)
120117, 119zmulcld 12730 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (denom‘𝑝)) ∈ ℤ)
121 qnumcl 16778 . . . . . . . . . . . . . . . . 17 (𝑝 ∈ ℚ → (numer‘𝑝) ∈ ℤ)
122121adantl 481 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℤ)
12320adantr 480 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ ℤ)
124122, 123zmulcld 12730 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑝) · (denom‘𝑞)) ∈ ℤ)
125120, 124zaddcld 12728 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) ∈ ℤ)
12685nnzd 12642 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ ℤ)
12785nnne0d 12317 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ≠ 0)
128126, 127eldifsnd 4786 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖ {0}))
129128, 39eleqtrdi 2850 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 + 𝑝)) ∈ (RLReg‘ℤring))
130123, 119zmulcld 12730 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℤ)
13187, 90nnmulcld 12320 . . . . . . . . . . . . . . . . 17 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ ℕ)
132131nnne0d 12317 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ≠ 0)
133130, 132eldifsnd 4786 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (ℤ ∖ {0}))
134133, 39eleqtrdi 2850 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((denom‘𝑞) · (denom‘𝑝)) ∈ (RLReg‘ℤring))
13528, 30, 114, 71, 116, 125, 129, 134fracerl 33309 . . . . . . . . . . . . 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 8799 . . . . . . . . . . 11 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] )
138137adantr 480 . . . . . . . . . 10 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] )
139 fveq2 6905 . . . . . . . . . . . . 13 (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝)))
140 fveq2 6905 . . . . . . . . . . . . 13 (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝)))
141139, 140opeq12d 4880 . . . . . . . . . . . 12 (𝑢 = (𝑞 + 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
142141adantl 481 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩)
143142eceq1d 8786 . . . . . . . . . 10 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] = [⟨(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))⟩] )
144 zringplusg 21466 . . . . . . . . . . 11 + = (+g‘ℤring)
145 eqid 2736 . . . . . . . . . . 11 (ℤring RLocal (ℤ ∖ {0})) = (ℤring RLocal (ℤ ∖ {0}))
146 zringcrng 21460 . . . . . . . . . . . 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 12317 . . . . . . . . . . . . . 14 (𝑝 ∈ ℚ → (denom‘𝑝) ≠ 0)
156118, 155eldifsnd 4786 . . . . . . . . . . . . 13 (𝑝 ∈ ℚ → (denom‘𝑝) ∈ (ℤ ∖ {0}))
157156adantl 481 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
158157adantr 480 . . . . . . . . . . 11 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖ {0}))
159 eqid 2736 . . . . . . . . . . 11 (+g‘(ℤring RLocal (ℤ ∖ {0}))) = (+g‘(ℤring RLocal (ℤ ∖ {0})))
16028, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159rlocaddval 33273 . . . . . . . . . 10 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) = [⟨(((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))), ((denom‘𝑞) · (denom‘𝑝))⟩] )
161138, 143, 1603eqtr4d 2786 . . . . . . . . 9 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (+g‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
162 ovexd 7467 . . . . . . . . 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 2787 . . . . . . 7 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)))
165164rgen2 3198 . . . . . 6 𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝))
16647, 165pm3.2i 470 . . . . 5 (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)))
1671qrngbas 27664 . . . . . 6 ℚ = (Base‘𝑄)
168 eqid 2736 . . . . . 6 (Base‘( Frac ‘ℤring)) = (Base‘( Frac ‘ℤring))
169 qex 13004 . . . . . . 7 ℚ ∈ V
170 cnfldadd 21371 . . . . . . . 8 + = (+g‘ℂfld)
1711, 170ressplusg 17335 . . . . . . 7 (ℚ ∈ V → + = (+g𝑄))
172169, 171ax-mp 5 . . . . . 6 + = (+g𝑄)
173 eqid 2736 . . . . . 6 (+g‘( Frac ‘ℤring)) = (+g‘( Frac ‘ℤring))
174167, 168, 172, 173isghm 19234 . . . . 5 (𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤring)) ↔ ((𝑄 ∈ Grp ∧ ( Frac ‘ℤring) ∈ Grp) ∧ (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹𝑞)(+g‘( Frac ‘ℤring))(𝐹𝑝)))))
17516, 166, 174mpbir2an 711 . . . 4 𝐹 ∈ (𝑄 GrpHom ( Frac ‘ℤring))
176 eqid 2736 . . . . . . . 8 (mulGrp‘𝑄) = (mulGrp‘𝑄)
177176ringmgp 20237 . . . . . . 7 (𝑄 ∈ Ring → (mulGrp‘𝑄) ∈ Mnd)
1784, 177ax-mp 5 . . . . . 6 (mulGrp‘𝑄) ∈ Mnd
179 eqid 2736 . . . . . . . 8 (mulGrp‘( Frac ‘ℤring)) = (mulGrp‘( Frac ‘ℤring))
180179ringmgp 20237 . . . . . . 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 2736 . . . . . . . . . 10 (.r‘(ℤring RLocal (ℤ ∖ {0}))) = (.r‘(ℤring RLocal (ℤ ∖ {0})))
18428, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183rlocmulval 33274 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (.r‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) = [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] )
18579, 81mulcld 11282 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ)
186 qmulcl 13010 . . . . . . . . . . . . . . . 16 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ)
187 qdencl 16779 . . . . . . . . . . . . . . . 16 ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
188186, 187syl 17 . . . . . . . . . . . . . . 15 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℕ)
189188nncnd 12283 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℂ)
190185, 189, 92mul32d 11472 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
19179, 81, 88, 91mul4d 11474 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))))
192191oveq1d 7447 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
193190, 192eqtrd 2776 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))))
194 qmuldeneqnum 16785 . . . . . . . . . . . . . 14 ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
195186, 194syl 17 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝)))
196195oveq1d 7447 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
19799, 104oveq12d 7450 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝)))
198197oveq1d 7447 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))))
199193, 196, 1983eqtr3rd 2785 . . . . . . . . . . 11 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))
200117, 122zmulcld 12730 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((numer‘𝑞) · (numer‘𝑝)) ∈ ℤ)
201 qnumcl 16778 . . . . . . . . . . . . 13 ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
202186, 201syl 17 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘(𝑞 · 𝑝)) ∈ ℤ)
203188nnzd 12642 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ ℤ)
204188nnne0d 12317 . . . . . . . . . . . . . 14 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ≠ 0)
205203, 204eldifsnd 4786 . . . . . . . . . . . . 13 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (ℤ ∖ {0}))
206205, 39eleqtrdi 2850 . . . . . . . . . . . 12 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘(𝑞 · 𝑝)) ∈ (RLReg‘ℤring))
20728, 30, 114, 71, 200, 202, 134, 206fracerl 33309 . . . . . . . . . . 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 8799 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨((numer‘𝑞) · (numer‘𝑝)), ((denom‘𝑞) · (denom‘𝑝))⟩] = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
210184, 209eqtrd 2776 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (.r‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
21141fveq2i 6908 . . . . . . . . . 10 (.r‘( Frac ‘ℤring)) = (.r‘(ℤring RLocal (ℤ ∖ {0})))
212211a1i 11 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (.r‘( Frac ‘ℤring)) = (.r‘(ℤring RLocal (ℤ ∖ {0}))))
213212, 52, 58oveq123d 7453 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)) = ([⟨(numer‘𝑞), (denom‘𝑞)⟩] (.r‘(ℤring RLocal (ℤ ∖ {0})))[⟨(numer‘𝑝), (denom‘𝑝)⟩] ))
214 fveq2 6905 . . . . . . . . . . 11 (𝑢 = (𝑞 · 𝑝) → (numer‘𝑢) = (numer‘(𝑞 · 𝑝)))
215 fveq2 6905 . . . . . . . . . . 11 (𝑢 = (𝑞 · 𝑝) → (denom‘𝑢) = (denom‘(𝑞 · 𝑝)))
216214, 215opeq12d 4880 . . . . . . . . . 10 (𝑢 = (𝑞 · 𝑝) → ⟨(numer‘𝑢), (denom‘𝑢)⟩ = ⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩)
217216eceq1d 8786 . . . . . . . . 9 (𝑢 = (𝑞 · 𝑝) → [⟨(numer‘𝑢), (denom‘𝑢)⟩] = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
218 ecexg 8750 . . . . . . . . . 10 ( ∈ V → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∈ V)
21925, 218mp1i 13 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] ∈ V)
22068, 217, 186, 219fvmptd3 7038 . . . . . . . 8 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [⟨(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))⟩] )
221210, 213, 2203eqtr4rd 2787 . . . . . . 7 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)))
222221rgen2 3198 . . . . . 6 𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝))
223 zssq 12999 . . . . . . . 8 ℤ ⊆ ℚ
224 1z 12649 . . . . . . . 8 1 ∈ ℤ
225223, 224sselii 3979 . . . . . . 7 1 ∈ ℚ
226 fveq2 6905 . . . . . . . . . . 11 (𝑞 = 1 → (numer‘𝑞) = (numer‘1))
227 1zzd 12650 . . . . . . . . . . . . 13 (ℤring ∈ IDomn → 1 ∈ ℤ)
228227znumd 32815 . . . . . . . . . . . 12 (ℤring ∈ IDomn → (numer‘1) = 1)
2295, 228ax-mp 5 . . . . . . . . . . 11 (numer‘1) = 1
230226, 229eqtrdi 2792 . . . . . . . . . 10 (𝑞 = 1 → (numer‘𝑞) = 1)
231 fveq2 6905 . . . . . . . . . . 11 (𝑞 = 1 → (denom‘𝑞) = (denom‘1))
232227zdend 32816 . . . . . . . . . . . 12 (ℤring ∈ IDomn → (denom‘1) = 1)
2335, 232ax-mp 5 . . . . . . . . . . 11 (denom‘1) = 1
234231, 233eqtrdi 2792 . . . . . . . . . 10 (𝑞 = 1 → (denom‘𝑞) = 1)
235230, 234opeq12d 4880 . . . . . . . . 9 (𝑞 = 1 → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨1, 1⟩)
236235eceq1d 8786 . . . . . . . 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 1339 . . . . 5 (𝐹:ℚ⟶(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹𝑞)(.r‘( Frac ‘ℤring))(𝐹𝑝)) ∧ (𝐹‘1) = [⟨1, 1⟩] )
240176, 167mgpbas 20143 . . . . . 6 ℚ = (Base‘(mulGrp‘𝑄))
241179, 168mgpbas 20143 . . . . . 6 (Base‘( Frac ‘ℤring)) = (Base‘(mulGrp‘( Frac ‘ℤring)))
242 cnfldmul 21373 . . . . . . . . 9 · = (.r‘ℂfld)
2431, 242ressmulr 17352 . . . . . . . 8 (ℚ ∈ V → · = (.r𝑄))
244169, 243ax-mp 5 . . . . . . 7 · = (.r𝑄)
245176, 244mgpplusg 20142 . . . . . 6 · = (+g‘(mulGrp‘𝑄))
246 eqid 2736 . . . . . . 7 (.r‘( Frac ‘ℤring)) = (.r‘( Frac ‘ℤring))
247179, 246mgpplusg 20142 . . . . . 6 (.r‘( Frac ‘ℤring)) = (+g‘(mulGrp‘( Frac ‘ℤring)))
2481qrng1 27667 . . . . . . 7 1 = (1r𝑄)
249176, 248ringidval 20181 . . . . . 6 1 = (0g‘(mulGrp‘𝑄))
250146a1i 11 . . . . . . . . 9 (ℤring ∈ IDomn → ℤring ∈ CRing)
251149a1i 11 . . . . . . . . 9 (ℤring ∈ IDomn → (ℤ ∖ {0}) ∈ (SubMnd‘(mulGrp‘ℤring)))
252 eqid 2736 . . . . . . . . 9 [⟨1, 1⟩] = [⟨1, 1⟩]
25329, 69, 41, 24, 250, 251, 252rloc1r 33277 . . . . . . . 8 (ℤring ∈ IDomn → [⟨1, 1⟩] = (1r‘( Frac ‘ℤring)))
2545, 253ax-mp 5 . . . . . . 7 [⟨1, 1⟩] = (1r‘( Frac ‘ℤring))
255179, 254ringidval 20181 . . . . . 6 [⟨1, 1⟩] = (0g‘(mulGrp‘( Frac ‘ℤring)))
256240, 241, 245, 247, 249, 255ismhm 18799 . . . . 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 20479 . . 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 3062 . . . 4 𝑞 ∈ ℚ [⟨(numer‘𝑞), (denom‘𝑞)⟩] ∈ (Base‘( Frac ‘ℤring))
262117zcnd 12725 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑞) ∈ ℂ)
263122zcnd 12725 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (numer‘𝑝) ∈ ℂ)
26421adantr 480 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ≠ 0)
265155adantl 481 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ≠ 0)
266262, 88, 263, 91, 264, 265divmuleqd 12090 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((numer‘𝑞) / (denom‘𝑞)) = ((numer‘𝑝) / (denom‘𝑝)) ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
267153, 39eleqtrdi 2850 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑞) ∈ (RLReg‘ℤring))
268157, 39eleqtrdi 2850 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (denom‘𝑝) ∈ (RLReg‘ℤring))
26928, 30, 114, 71, 117, 122, 267, 268fracerl 33309 . . . . . . . . 9 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (⟨(numer‘𝑞), (denom‘𝑞)⟩ ⟨(numer‘𝑝), (denom‘𝑝)⟩ ↔ ((numer‘𝑞) · (denom‘𝑝)) = ((numer‘𝑝) · (denom‘𝑞))))
27023adantr 480 . . . . . . . . . 10 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ ∈ (ℤ × (ℤ ∖ {0})))
27177, 270erth 8797 . . . . . . . . 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 16784 . . . . . . . 8 (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
275274ad2antrr 726 . . . . . . 7 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → 𝑞 = ((numer‘𝑞) / (denom‘𝑞)))
276 qeqnumdivden 16784 . . . . . . . 8 (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
277276ad2antlr 727 . . . . . . 7 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → 𝑝 = ((numer‘𝑝) / (denom‘𝑝)))
278273, 275, 2773eqtr4d 2786 . . . . . 6 (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] ) → 𝑞 = 𝑝)
279278ex 412 . . . . 5 ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ([⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] 𝑞 = 𝑝))
280279rgen2 3198 . . . 4 𝑞 ∈ ℚ ∀𝑝 ∈ ℚ ([⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘𝑝), (denom‘𝑝)⟩] 𝑞 = 𝑝)
28117, 56f1mpt 7282 . . . 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 6905 . . . . . . . . . 10 (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏)))
284 fveq2 6905 . . . . . . . . . 10 (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏)))
285283, 284opeq12d 4880 . . . . . . . . 9 (𝑞 = (𝑎 / 𝑏) → ⟨(numer‘𝑞), (denom‘𝑞)⟩ = ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
286285eceq1d 8786 . . . . . . . 8 (𝑞 = (𝑎 / 𝑏) → [⟨(numer‘𝑞), (denom‘𝑞)⟩] = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] )
287286eqeq2d 2747 . . . . . . 7 (𝑞 = (𝑎 / 𝑏) → (𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] ))
288 simpllr 775 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑎 ∈ ℤ)
289223, 288sselid 3980 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑎 ∈ ℚ)
290 simplr 768 . . . . . . . . . 10 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ∈ (ℤ ∖ {0}))
291290eldifad 3962 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ∈ ℤ)
292223, 291sselid 3980 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ∈ ℚ)
293 eldifsni 4789 . . . . . . . . 9 (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ≠ 0)
294290, 293syl 17 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑏 ≠ 0)
295 qdivcl 13013 . . . . . . . 8 ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ)
296289, 292, 294, 295syl3anc 1372 . . . . . . 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 33270 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → Er (ℤ × (ℤ ∖ {0})))
301 simpl 482 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℤ)
302301zcnd 12725 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℂ)
303 eldifi 4130 . . . . . . . . . . . . . . . 16 (𝑏 ∈ (ℤ ∖ {0}) → 𝑏 ∈ ℤ)
304303adantl 481 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℤ)
305304zcnd 12725 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℂ)
306293adantl 481 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ≠ 0)
307302, 305, 306divcld 12044 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℂ)
308223, 301sselid 3980 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑎 ∈ ℚ)
309223, 304sselid 3980 . . . . . . . . . . . . . . . 16 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ ℚ)
310308, 309, 306, 295syl3anc 1372 . . . . . . . . . . . . . . 15 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 / 𝑏) ∈ ℚ)
311 qdencl 16779 . . . . . . . . . . . . . . 15 ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
312310, 311syl 17 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℕ)
313312nncnd 12283 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℂ)
314307, 313, 305mul32d 11472 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))))
315 qmuldeneqnum 16785 . . . . . . . . . . . . . 14 ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
316310, 315syl 17 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏)))
317316oveq1d 7447 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
318302, 305, 306divcan1d 12045 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ((𝑎 / 𝑏) · 𝑏) = 𝑎)
319318oveq1d 7447 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏))))
320314, 317, 3193eqtr3rd 2785 . . . . . . . . . . 11 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))
321146a1i 11 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ℤring ∈ CRing)
322 qnumcl 16778 . . . . . . . . . . . . 13 ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
323310, 322syl 17 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (numer‘(𝑎 / 𝑏)) ∈ ℤ)
324 simpr 484 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (ℤ ∖ {0}))
325324, 39eleqtrdi 2850 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → 𝑏 ∈ (RLReg‘ℤring))
326312nnzd 12642 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ ℤ)
327312nnne0d 12317 . . . . . . . . . . . . . 14 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ≠ 0)
328326, 327eldifsnd 4786 . . . . . . . . . . . . 13 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (ℤ ∖ {0}))
329328, 39eleqtrdi 2850 . . . . . . . . . . . 12 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (denom‘(𝑎 / 𝑏)) ∈ (RLReg‘ℤring))
33028, 30, 114, 321, 301, 323, 325, 329fracerl 33309 . . . . . . . . . . 11 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → (⟨𝑎, 𝑏 ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩ ↔ (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏)))
331320, 330mpbird 257 . . . . . . . . . 10 ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0})) → ⟨𝑎, 𝑏 ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
332331ad4ant23 753 . . . . . . . . 9 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → ⟨𝑎, 𝑏 ⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩)
333300, 332erthi 8799 . . . . . . . 8 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → [⟨𝑎, 𝑏⟩] = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] )
334297, 333eqtrd 2776 . . . . . . 7 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → 𝑧 = [⟨(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))⟩] )
335287, 296, 334rspcedvdw 3624 . . . . . 6 ((((𝑧 ∈ (Base‘( Frac ‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [⟨𝑎, 𝑏⟩] ) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
33645eleq2i 2832 . . . . . . . 8 (𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ) ↔ 𝑧 ∈ (Base‘( Frac ‘ℤring)))
337336biimpri 228 . . . . . . 7 (𝑧 ∈ (Base‘( Frac ‘ℤring)) → 𝑧 ∈ ((ℤ × (ℤ ∖ {0})) / ))
338337elrlocbasi 33271 . . . . . 6 (𝑧 ∈ (Base‘( Frac ‘ℤring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [⟨𝑎, 𝑏⟩] )
339335, 338r19.29vva 3215 . . . . 5 (𝑧 ∈ (Base‘( Frac ‘ℤring)) → ∃𝑞 ∈ ℚ 𝑧 = [⟨(numer‘𝑞), (denom‘𝑞)⟩] )
340339rgen 3062 . . . 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 6567 . . 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 20493 . 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 1539  wtru 1540  wcel 2107  wne 2939  wral 3060  wrex 3069  Vcvv 3479  cdif 3947  {csn 4625  cop 4631   class class class wbr 5142  cmpt 5224   × cxp 5682  wf 6556  1-1wf1 6557  ontowfo 6558  1-1-ontowf1o 6559  cfv 6560  (class class class)co 7432  [cec 8744   / cqs 8745  cc 11154  0cc0 11156  1c1 11157   + caddc 11159   · cmul 11161   / cdiv 11921  cn 12267  cz 12615  cq 12991  numercnumer 16771  denomcdenom 16772  Basecbs 17248  s cress 17275  +gcplusg 17298  .rcmulr 17299  Mndcmnd 18748   MndHom cmhm 18795  SubMndcsubmnd 18796  Grpcgrp 18952  -gcsg 18954   GrpHom cghm 19231  mulGrpcmgp 20138  1rcur 20179  Ringcrg 20231  CRingccrg 20232   RingHom crh 20470   RingIso crs 20471  NzRingcnzr 20513  RLRegcrlreg 20692  Domncdomn 20693  IDomncidom 20694  DivRingcdr 20730  fldccnfld 21365  ringczring 21458   ~RL cerl 33258   RLocal crloc 33259   Frac cfrac 33305
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 2707  ax-rep 5278  ax-sep 5295  ax-nul 5305  ax-pow 5364  ax-pr 5431  ax-un 7756  ax-cnex 11212  ax-resscn 11213  ax-1cn 11214  ax-icn 11215  ax-addcl 11216  ax-addrcl 11217  ax-mulcl 11218  ax-mulrcl 11219  ax-mulcom 11220  ax-addass 11221  ax-mulass 11222  ax-distr 11223  ax-i2m1 11224  ax-1ne0 11225  ax-1rid 11226  ax-rnegex 11227  ax-rrecex 11228  ax-cnre 11229  ax-pre-lttri 11230  ax-pre-lttrn 11231  ax-pre-ltadd 11232  ax-pre-mulgt0 11233  ax-pre-sup 11234  ax-addf 11235  ax-mulf 11236
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 2539  df-eu 2568  df-clab 2714  df-cleq 2728  df-clel 2815  df-nfc 2891  df-ne 2940  df-nel 3046  df-ral 3061  df-rex 3070  df-rmo 3379  df-reu 3380  df-rab 3436  df-v 3481  df-sbc 3788  df-csb 3899  df-dif 3953  df-un 3955  df-in 3957  df-ss 3967  df-pss 3970  df-nul 4333  df-if 4525  df-pw 4601  df-sn 4626  df-pr 4628  df-tp 4630  df-op 4632  df-uni 4907  df-iun 4992  df-br 5143  df-opab 5205  df-mpt 5225  df-tr 5259  df-id 5577  df-eprel 5583  df-po 5591  df-so 5592  df-fr 5636  df-we 5638  df-xp 5690  df-rel 5691  df-cnv 5692  df-co 5693  df-dm 5694  df-rn 5695  df-res 5696  df-ima 5697  df-pred 6320  df-ord 6386  df-on 6387  df-lim 6388  df-suc 6389  df-iota 6513  df-fun 6562  df-fn 6563  df-f 6564  df-f1 6565  df-fo 6566  df-f1o 6567  df-fv 6568  df-riota 7389  df-ov 7435  df-oprab 7436  df-mpo 7437  df-om 7889  df-1st 8015  df-2nd 8016  df-tpos 8252  df-frecs 8307  df-wrecs 8338  df-recs 8412  df-rdg 8451  df-1o 8507  df-er 8746  df-ec 8748  df-qs 8752  df-map 8869  df-en 8987  df-dom 8988  df-sdom 8989  df-fin 8990  df-sup 9483  df-inf 9484  df-pnf 11298  df-mnf 11299  df-xr 11300  df-ltxr 11301  df-le 11302  df-sub 11495  df-neg 11496  df-div 11922  df-nn 12268  df-2 12330  df-3 12331  df-4 12332  df-5 12333  df-6 12334  df-7 12335  df-8 12336  df-9 12337  df-n0 12529  df-z 12616  df-dec 12736  df-uz 12880  df-q 12992  df-rp 13036  df-fz 13549  df-fl 13833  df-mod 13911  df-seq 14044  df-exp 14104  df-cj 15139  df-re 15140  df-im 15141  df-sqrt 15275  df-abs 15276  df-dvds 16292  df-gcd 16533  df-numer 16773  df-denom 16774  df-struct 17185  df-sets 17202  df-slot 17220  df-ndx 17232  df-base 17249  df-ress 17276  df-plusg 17311  df-mulr 17312  df-starv 17313  df-sca 17314  df-vsca 17315  df-ip 17316  df-tset 17317  df-ple 17318  df-ds 17320  df-unif 17321  df-0g 17487  df-imas 17554  df-qus 17555  df-mgm 18654  df-sgrp 18733  df-mnd 18749  df-mhm 18797  df-submnd 18798  df-grp 18955  df-minusg 18956  df-sbg 18957  df-subg 19142  df-ghm 19232  df-cmn 19801  df-abl 19802  df-mgp 20139  df-rng 20151  df-ur 20180  df-ring 20233  df-cring 20234  df-oppr 20335  df-dvdsr 20358  df-unit 20359  df-invr 20389  df-dvr 20402  df-rhm 20473  df-rim 20474  df-nzr 20514  df-subrng 20547  df-subrg 20571  df-rlreg 20695  df-domn 20696  df-idom 20697  df-drng 20732  df-field 20733  df-cnfld 21366  df-zring 21459  df-erl 33260  df-rloc 33261  df-frac 33306
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator