| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | zringfrac.1 | . . . . . 6
⊢ 𝑄 = (ℂfld
↾s ℚ) | 
| 2 | 1 | qdrng 27665 | . . . . 5
⊢ 𝑄 ∈ DivRing | 
| 3 |  | drngring 20737 | . . . . 5
⊢ (𝑄 ∈ DivRing → 𝑄 ∈ Ring) | 
| 4 | 2, 3 | ax-mp 5 | . . . 4
⊢ 𝑄 ∈ Ring | 
| 5 |  | zringidom 33580 | . . . . 5
⊢
ℤring ∈ IDomn | 
| 6 |  | id 22 | . . . . . . . 8
⊢
(ℤring ∈ IDomn → ℤring
∈ IDomn) | 
| 7 | 6 | fracfld 33311 | . . . . . . 7
⊢
(ℤring ∈ IDomn → ( Frac
‘ℤring) ∈ Field) | 
| 8 | 7 | fldcrngd 20743 | . . . . . 6
⊢
(ℤring ∈ IDomn → ( Frac
‘ℤring) ∈ CRing) | 
| 9 | 8 | crngringd 20244 | . . . . 5
⊢
(ℤring ∈ IDomn → ( Frac
‘ℤring) ∈ Ring) | 
| 10 | 5, 9 | ax-mp 5 | . . . 4
⊢ ( Frac
‘ℤring) ∈ Ring | 
| 11 | 4, 10 | pm3.2i 470 | . . 3
⊢ (𝑄 ∈ Ring ∧ ( Frac
‘ℤring) ∈ Ring) | 
| 12 |  | ringgrp 20236 | . . . . . . 7
⊢ (𝑄 ∈ Ring → 𝑄 ∈ Grp) | 
| 13 | 4, 12 | ax-mp 5 | . . . . . 6
⊢ 𝑄 ∈ Grp | 
| 14 |  | ringgrp 20236 | . . . . . . 7
⊢ (( Frac
‘ℤring) ∈ Ring → ( Frac
‘ℤring) ∈ Grp) | 
| 15 | 10, 14 | ax-mp 5 | . . . . . 6
⊢ ( Frac
‘ℤring) ∈ Grp | 
| 16 | 13, 15 | pm3.2i 470 | . . . . 5
⊢ (𝑄 ∈ Grp ∧ ( Frac
‘ℤring) ∈ Grp) | 
| 17 |  | zringfrac.3 | . . . . . . 7
⊢ 𝐹 = (𝑞 ∈ ℚ ↦
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
) | 
| 18 |  | qnumcl 16778 | . . . . . . . . . 10
⊢ (𝑞 ∈ ℚ →
(numer‘𝑞) ∈
ℤ) | 
| 19 |  | qdencl 16779 | . . . . . . . . . . . 12
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℕ) | 
| 20 | 19 | nnzd 12642 | . . . . . . . . . . 11
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
ℤ) | 
| 21 | 19 | nnne0d 12317 | . . . . . . . . . . 11
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ≠
0) | 
| 22 | 20, 21 | eldifsnd 4786 | . . . . . . . . . 10
⊢ (𝑞 ∈ ℚ →
(denom‘𝑞) ∈
(ℤ ∖ {0})) | 
| 23 | 18, 22 | opelxpd 5723 | . . . . . . . . 9
⊢ (𝑞 ∈ ℚ →
〈(numer‘𝑞),
(denom‘𝑞)〉
∈ (ℤ × (ℤ ∖ {0}))) | 
| 24 |  | zringfrac.2 | . . . . . . . . . . 11
⊢  ∼ =
(ℤring ~RL (ℤ ∖
{0})) | 
| 25 | 24 | ovexi 7466 | . . . . . . . . . 10
⊢  ∼ ∈
V | 
| 26 | 25 | ecelqsi 8814 | . . . . . . . . 9
⊢
(〈(numer‘𝑞), (denom‘𝑞)〉 ∈ (ℤ × (ℤ
∖ {0})) → [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ∈ ((ℤ
× (ℤ ∖ {0})) / ∼ )) | 
| 27 | 23, 26 | syl 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)) | 
| 34 | 6 | idomdomd 20727 | . . . . . . . . . . . . . . 15
⊢
(ℤring ∈ IDomn → ℤring
∈ Domn) | 
| 35 | 5, 34 | ax-mp 5 | . . . . . . . . . . . . . 14
⊢
ℤring ∈ Domn | 
| 36 |  | eqid 2736 | . . . . . . . . . . . . . . 15
⊢
(RLReg‘ℤring) =
(RLReg‘ℤring) | 
| 37 | 28, 36, 29 | isdomn6 20715 | . . . . . . . . . . . . . 14
⊢
(ℤring ∈ Domn ↔ (ℤring
∈ NzRing ∧ (ℤ ∖ {0}) =
(RLReg‘ℤring))) | 
| 38 | 35, 37 | mpbi 230 | . . . . . . . . . . . . 13
⊢
(ℤring ∈ NzRing ∧ (ℤ ∖ {0}) =
(RLReg‘ℤring)) | 
| 39 | 38 | simpri 485 | . . . . . . . . . . . 12
⊢ (ℤ
∖ {0}) = (RLReg‘ℤring) | 
| 40 | 39 | oveq2i 7443 | . . . . . . . . . . 11
⊢
(ℤring RLocal (ℤ ∖ {0})) =
(ℤring RLocal
(RLReg‘ℤring)) | 
| 41 | 33, 40 | eqtr4i 2767 | . . . . . . . . . 10
⊢ ( Frac
‘ℤring) = (ℤring RLocal (ℤ
∖ {0})) | 
| 42 | 5 | a1i 11 | . . . . . . . . . 10
⊢ (⊤
→ ℤring ∈ IDomn) | 
| 43 |  | difssd 4136 | . . . . . . . . . 10
⊢ (⊤
→ (ℤ ∖ {0}) ⊆ ℤ) | 
| 44 | 28, 29, 30, 31, 32, 41, 24, 42, 43 | rlocbas 33272 | . . . . . . . . 9
⊢ (⊤
→ ((ℤ × (ℤ ∖ {0})) / ∼ ) = (Base‘(
Frac ‘ℤring))) | 
| 45 | 44 | mptru 1546 | . . . . . . . 8
⊢ ((ℤ
× (ℤ ∖ {0})) / ∼ ) = (Base‘(
Frac ‘ℤring)) | 
| 46 | 27, 45 | eleqtrdi 2850 | . . . . . . 7
⊢ (𝑞 ∈ ℚ →
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
∈ (Base‘( Frac ‘ℤring))) | 
| 47 | 17, 46 | fmpti 7131 | . . . . . 6
⊢ 𝐹:ℚ⟶(Base‘(
Frac ‘ℤring)) | 
| 48 |  | ecexg 8750 | . . . . . . . . . . . 12
⊢ ( ∼ ∈
V → [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ∈
V) | 
| 49 | 25, 48 | ax-mp 5 | . . . . . . . . . . 11
⊢
[〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ∈
V | 
| 50 | 17 | fvmpt2 7026 | . . . . . . . . . . 11
⊢ ((𝑞 ∈ ℚ ∧
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
∈ V) → (𝐹‘𝑞) = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ) | 
| 51 | 49, 50 | mpan2 691 | . . . . . . . . . 10
⊢ (𝑞 ∈ ℚ → (𝐹‘𝑞) = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ) | 
| 52 | 51 | adantr 480 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑞) = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ) | 
| 53 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑝 → (numer‘𝑞) = (numer‘𝑝)) | 
| 54 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑝 → (denom‘𝑞) = (denom‘𝑝)) | 
| 55 | 53, 54 | opeq12d 4880 | . . . . . . . . . . . 12
⊢ (𝑞 = 𝑝 → 〈(numer‘𝑞), (denom‘𝑞)〉 = 〈(numer‘𝑝), (denom‘𝑝)〉) | 
| 56 | 55 | eceq1d 8786 | . . . . . . . . . . 11
⊢ (𝑞 = 𝑝 → [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ =
[〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
) | 
| 57 | 56, 17, 27 | fvmpt3 7019 | . . . . . . . . . 10
⊢ (𝑝 ∈ ℚ → (𝐹‘𝑝) = [〈(numer‘𝑝), (denom‘𝑝)〉] ∼ ) | 
| 58 | 57 | adantl 481 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘𝑝) = [〈(numer‘𝑝), (denom‘𝑝)〉] ∼ ) | 
| 59 | 52, 58 | oveq12d 7450 | . . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+g‘(ℤring
RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) = ([〈(numer‘𝑞), (denom‘𝑞)〉] ∼
(+g‘(ℤring RLocal (ℤ ∖
{0})))[〈(numer‘𝑝), (denom‘𝑝)〉] ∼ )) | 
| 60 | 41 | fveq2i 6908 | . . . . . . . . . 10
⊢
(+g‘( Frac ‘ℤring)) =
(+g‘(ℤring RLocal (ℤ ∖
{0}))) | 
| 61 | 60 | oveqi 7445 | . . . . . . . . 9
⊢ ((𝐹‘𝑞)(+g‘( Frac
‘ℤring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+g‘(ℤring
RLocal (ℤ ∖ {0})))(𝐹‘𝑝)) | 
| 62 | 61 | a1i 11 | . . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝐹‘𝑞)(+g‘( Frac
‘ℤring))(𝐹‘𝑝)) = ((𝐹‘𝑞)(+g‘(ℤring
RLocal (ℤ ∖ {0})))(𝐹‘𝑝))) | 
| 63 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑢 → (numer‘𝑞) = (numer‘𝑢)) | 
| 64 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑞 = 𝑢 → (denom‘𝑞) = (denom‘𝑢)) | 
| 65 | 63, 64 | opeq12d 4880 | . . . . . . . . . . . 12
⊢ (𝑞 = 𝑢 → 〈(numer‘𝑞), (denom‘𝑞)〉 = 〈(numer‘𝑢), (denom‘𝑢)〉) | 
| 66 | 65 | eceq1d 8786 | . . . . . . . . . . 11
⊢ (𝑞 = 𝑢 → [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ =
[〈(numer‘𝑢),
(denom‘𝑢)〉]
∼
) | 
| 67 | 66 | cbvmptv 5254 | . . . . . . . . . 10
⊢ (𝑞 ∈ ℚ ↦
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
) = (𝑢 ∈ ℚ
↦ [〈(numer‘𝑢), (denom‘𝑢)〉] ∼ ) | 
| 68 | 17, 67 | eqtri 2764 | . . . . . . . . 9
⊢ 𝐹 = (𝑢 ∈ ℚ ↦
[〈(numer‘𝑢),
(denom‘𝑢)〉]
∼
) | 
| 69 |  | zring1 21471 | . . . . . . . . . . . . 13
⊢ 1 =
(1r‘ℤring) | 
| 70 | 5 | a1i 11 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
ℤring ∈ IDomn) | 
| 71 | 70 | idomcringd 20728 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
ℤring ∈ CRing) | 
| 72 | 35 | a1i 11 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
ℤring ∈ Domn) | 
| 73 |  | eqid 2736 | . . . . . . . . . . . . . . . 16
⊢
(mulGrp‘ℤring) =
(mulGrp‘ℤring) | 
| 74 | 28, 29, 73 | isdomn3 20716 | . . . . . . . . . . . . . . 15
⊢
(ℤring ∈ Domn ↔ (ℤring
∈ Ring ∧ (ℤ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring)))) | 
| 75 | 72, 74 | sylib 218 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(ℤring ∈ Ring ∧ (ℤ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring)))) | 
| 76 | 75 | simprd 495 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (ℤ
∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring))) | 
| 77 | 28, 29, 69, 30, 31, 32, 24, 71, 76 | erler 33270 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ∼ Er
(ℤ × (ℤ ∖ {0}))) | 
| 78 |  | qcn 13006 | . . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ℚ → 𝑞 ∈
ℂ) | 
| 79 | 78 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑞 ∈
ℂ) | 
| 80 |  | qcn 13006 | . . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℚ → 𝑝 ∈
ℂ) | 
| 81 | 80 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → 𝑝 ∈
ℂ) | 
| 82 | 79, 81 | addcld 11281 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℂ) | 
| 83 |  | qaddcl 13008 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 + 𝑝) ∈ ℚ) | 
| 84 |  | qdencl 16779 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 + 𝑝) ∈ ℚ → (denom‘(𝑞 + 𝑝)) ∈ ℕ) | 
| 85 | 83, 84 | syl 17 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 + 𝑝)) ∈
ℕ) | 
| 86 | 85 | nncnd 12283 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 + 𝑝)) ∈
ℂ) | 
| 87 | 19 | adantr 480 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑞) ∈
ℕ) | 
| 88 | 87 | nncnd 12283 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑞) ∈
ℂ) | 
| 89 |  | qdencl 16779 | . . . . . . . . . . . . . . . . . 18
⊢ (𝑝 ∈ ℚ →
(denom‘𝑝) ∈
ℕ) | 
| 90 | 89 | adantl 481 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑝) ∈
ℕ) | 
| 91 | 90 | nncnd 12283 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑝) ∈
ℂ) | 
| 92 | 88, 91 | mulcld 11282 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑞) ·
(denom‘𝑝)) ∈
ℂ) | 
| 93 | 82, 86, 92 | mul32d 11472 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝)))) | 
| 94 |  | qmuldeneqnum 16785 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 + 𝑝) ∈ ℚ → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝))) | 
| 95 | 83, 94 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) = (numer‘(𝑞 + 𝑝))) | 
| 96 | 95 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · (denom‘(𝑞 + 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))) | 
| 97 | 79, 88, 91 | mulassd 11285 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = (𝑞 · ((denom‘𝑞) · (denom‘𝑝)))) | 
| 98 |  | qmuldeneqnum 16785 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ ℚ → (𝑞 · (denom‘𝑞)) = (numer‘𝑞)) | 
| 99 | 98 | adantr 480 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · (denom‘𝑞)) = (numer‘𝑞)) | 
| 100 | 99 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (denom‘𝑝)) = ((numer‘𝑞) · (denom‘𝑝))) | 
| 101 | 97, 100 | eqtr3d 2778 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑞) · (denom‘𝑝))) | 
| 102 | 81, 91, 88 | mulassd 11285 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = (𝑝 · ((denom‘𝑝) · (denom‘𝑞)))) | 
| 103 |  | qmuldeneqnum 16785 | . . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 ∈ ℚ → (𝑝 · (denom‘𝑝)) = (numer‘𝑝)) | 
| 104 | 103 | adantl 481 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · (denom‘𝑝)) = (numer‘𝑝)) | 
| 105 | 104 | oveq1d 7447 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑝 · (denom‘𝑝)) · (denom‘𝑞)) = ((numer‘𝑝) · (denom‘𝑞))) | 
| 106 | 91, 88 | mulcomd 11283 | . . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑝) ·
(denom‘𝑞)) =
((denom‘𝑞) ·
(denom‘𝑝))) | 
| 107 | 106 | oveq2d 7448 | . . . . . . . . . . . . . . . . . 18
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑝) · (denom‘𝑞))) = (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) | 
| 108 | 102, 105,
107 | 3eqtr3rd 2785 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑝 · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘𝑝) · (denom‘𝑞))) | 
| 109 | 101, 108 | oveq12d 7450 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · ((denom‘𝑞) · (denom‘𝑝))) + (𝑝 · ((denom‘𝑞) · (denom‘𝑝)))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞)))) | 
| 110 | 79, 92, 81, 109 | joinlmuladdmuld 11289 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = (((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞)))) | 
| 111 | 110 | oveq1d 7447 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 + 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 + 𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝)))) | 
| 112 | 93, 96, 111 | 3eqtr3d 2784 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((numer‘(𝑞 + 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))) = ((((numer‘𝑞) · (denom‘𝑝)) + ((numer‘𝑝) · (denom‘𝑞))) · (denom‘(𝑞 + 𝑝)))) | 
| 113 | 39 | oveq2i 7443 | . . . . . . . . . . . . . . 15
⊢
(ℤring ~RL (ℤ ∖ {0})) =
(ℤring ~RL
(RLReg‘ℤring)) | 
| 114 | 24, 113 | eqtri 2764 | . . . . . . . . . . . . . 14
⊢  ∼ =
(ℤring ~RL
(RLReg‘ℤring)) | 
| 115 |  | qnumcl 16778 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 + 𝑝) ∈ ℚ → (numer‘(𝑞 + 𝑝)) ∈ ℤ) | 
| 116 | 83, 115 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(numer‘(𝑞 + 𝑝)) ∈
ℤ) | 
| 117 | 18 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(numer‘𝑞) ∈
ℤ) | 
| 118 | 89 | nnzd 12642 | . . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℚ →
(denom‘𝑝) ∈
ℤ) | 
| 119 | 118 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑝) ∈
ℤ) | 
| 120 | 117, 119 | zmulcld 12730 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((numer‘𝑞) ·
(denom‘𝑝)) ∈
ℤ) | 
| 121 |  | qnumcl 16778 | . . . . . . . . . . . . . . . . 17
⊢ (𝑝 ∈ ℚ →
(numer‘𝑝) ∈
ℤ) | 
| 122 | 121 | adantl 481 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(numer‘𝑝) ∈
ℤ) | 
| 123 | 20 | adantr 480 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑞) ∈
ℤ) | 
| 124 | 122, 123 | zmulcld 12730 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((numer‘𝑝) ·
(denom‘𝑞)) ∈
ℤ) | 
| 125 | 120, 124 | zaddcld 12728 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(((numer‘𝑞) ·
(denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))) ∈
ℤ) | 
| 126 | 85 | nnzd 12642 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 + 𝑝)) ∈
ℤ) | 
| 127 | 85 | nnne0d 12317 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 + 𝑝)) ≠ 0) | 
| 128 | 126, 127 | eldifsnd 4786 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 + 𝑝)) ∈ (ℤ ∖
{0})) | 
| 129 | 128, 39 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 + 𝑝)) ∈
(RLReg‘ℤring)) | 
| 130 | 123, 119 | zmulcld 12730 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑞) ·
(denom‘𝑝)) ∈
ℤ) | 
| 131 | 87, 90 | nnmulcld 12320 | . . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑞) ·
(denom‘𝑝)) ∈
ℕ) | 
| 132 | 131 | nnne0d 12317 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑞) ·
(denom‘𝑝)) ≠
0) | 
| 133 | 130, 132 | eldifsnd 4786 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑞) ·
(denom‘𝑝)) ∈
(ℤ ∖ {0})) | 
| 134 | 133, 39 | eleqtrdi 2850 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((denom‘𝑞) ·
(denom‘𝑝)) ∈
(RLReg‘ℤring)) | 
| 135 | 28, 30, 114, 71, 116, 125, 129, 134 | fracerl 33309 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(〈(numer‘(𝑞 +
𝑝)), (denom‘(𝑞 + 𝑝))〉 ∼
〈(((numer‘𝑞)
· (denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))),
((denom‘𝑞) ·
(denom‘𝑝))〉
↔ ((numer‘(𝑞 +
𝑝)) ·
((denom‘𝑞) ·
(denom‘𝑝))) =
((((numer‘𝑞) ·
(denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))) ·
(denom‘(𝑞 + 𝑝))))) | 
| 136 | 112, 135 | mpbird 257 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
〈(numer‘(𝑞 +
𝑝)), (denom‘(𝑞 + 𝑝))〉 ∼
〈(((numer‘𝑞)
· (denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))),
((denom‘𝑞) ·
(denom‘𝑝))〉) | 
| 137 | 77, 136 | erthi 8799 | . . . . . . . . . . 11
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
[〈(numer‘(𝑞 +
𝑝)), (denom‘(𝑞 + 𝑝))〉] ∼ =
[〈(((numer‘𝑞)
· (denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))),
((denom‘𝑞) ·
(denom‘𝑝))〉]
∼
) | 
| 138 | 137 | adantr 480 | . . . . . . . . . 10
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → [〈(numer‘(𝑞 + 𝑝)), (denom‘(𝑞 + 𝑝))〉] ∼ =
[〈(((numer‘𝑞)
· (denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))),
((denom‘𝑞) ·
(denom‘𝑝))〉]
∼
) | 
| 139 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑢 = (𝑞 + 𝑝) → (numer‘𝑢) = (numer‘(𝑞 + 𝑝))) | 
| 140 |  | fveq2 6905 | . . . . . . . . . . . . 13
⊢ (𝑢 = (𝑞 + 𝑝) → (denom‘𝑢) = (denom‘(𝑞 + 𝑝))) | 
| 141 | 139, 140 | opeq12d 4880 | . . . . . . . . . . . 12
⊢ (𝑢 = (𝑞 + 𝑝) → 〈(numer‘𝑢), (denom‘𝑢)〉 =
〈(numer‘(𝑞 +
𝑝)), (denom‘(𝑞 + 𝑝))〉) | 
| 142 | 141 | adantl 481 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → 〈(numer‘𝑢), (denom‘𝑢)〉 =
〈(numer‘(𝑞 +
𝑝)), (denom‘(𝑞 + 𝑝))〉) | 
| 143 | 142 | eceq1d 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 | 
| 147 | 146 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ℤring ∈
CRing) | 
| 148 | 35, 74 | mpbi 230 | . . . . . . . . . . . . 13
⊢
(ℤring ∈ Ring ∧ (ℤ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring))) | 
| 149 | 148 | simpri 485 | . . . . . . . . . . . 12
⊢ (ℤ
∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring)) | 
| 150 | 149 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (ℤ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring))) | 
| 151 | 117 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑞) ∈ ℤ) | 
| 152 | 122 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (numer‘𝑝) ∈ ℤ) | 
| 153 | 22 | adantr 480 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑞) ∈
(ℤ ∖ {0})) | 
| 154 | 153 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑞) ∈ (ℤ ∖
{0})) | 
| 155 | 89 | nnne0d 12317 | . . . . . . . . . . . . . 14
⊢ (𝑝 ∈ ℚ →
(denom‘𝑝) ≠
0) | 
| 156 | 118, 155 | eldifsnd 4786 | . . . . . . . . . . . . 13
⊢ (𝑝 ∈ ℚ →
(denom‘𝑝) ∈
(ℤ ∖ {0})) | 
| 157 | 156 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑝) ∈
(ℤ ∖ {0})) | 
| 158 | 157 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → (denom‘𝑝) ∈ (ℤ ∖
{0})) | 
| 159 |  | eqid 2736 | . . . . . . . . . . 11
⊢
(+g‘(ℤring RLocal (ℤ ∖
{0}))) = (+g‘(ℤring RLocal (ℤ ∖
{0}))) | 
| 160 | 28, 30, 144, 145, 24, 147, 150, 151, 152, 154, 158, 159 | rlocaddval 33273 | . . . . . . . . . 10
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧ 𝑢 = (𝑞 + 𝑝)) → ([〈(numer‘𝑞), (denom‘𝑞)〉] ∼
(+g‘(ℤring RLocal (ℤ ∖
{0})))[〈(numer‘𝑝), (denom‘𝑝)〉] ∼ ) =
[〈(((numer‘𝑞)
· (denom‘𝑝)) +
((numer‘𝑝) ·
(denom‘𝑞))),
((denom‘𝑞) ·
(denom‘𝑝))〉]
∼
) | 
| 161 | 138, 143,
160 | 3eqtr4d 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) | 
| 163 | 68, 161, 83, 162 | fvmptd2 7023 | . . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ([〈(numer‘𝑞), (denom‘𝑞)〉] ∼
(+g‘(ℤring RLocal (ℤ ∖
{0})))[〈(numer‘𝑝), (denom‘𝑝)〉] ∼ )) | 
| 164 | 59, 62, 163 | 3eqtr4rd 2787 | . . . . . . 7
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+g‘( Frac
‘ℤring))(𝐹‘𝑝))) | 
| 165 | 164 | rgen2 3198 | . . . . . 6
⊢
∀𝑞 ∈
ℚ ∀𝑝 ∈
ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+g‘( Frac
‘ℤring))(𝐹‘𝑝)) | 
| 166 | 47, 165 | pm3.2i 470 | . . . . 5
⊢ (𝐹:ℚ⟶(Base‘(
Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+g‘( Frac
‘ℤring))(𝐹‘𝑝))) | 
| 167 | 1 | qrngbas 27664 | . . . . . 6
⊢ ℚ =
(Base‘𝑄) | 
| 168 |  | eqid 2736 | . . . . . 6
⊢
(Base‘( Frac ‘ℤring)) = (Base‘( Frac
‘ℤring)) | 
| 169 |  | qex 13004 | . . . . . . 7
⊢ ℚ
∈ V | 
| 170 |  | cnfldadd 21371 | . . . . . . . 8
⊢  + =
(+g‘ℂfld) | 
| 171 | 1, 170 | ressplusg 17335 | . . . . . . 7
⊢ (ℚ
∈ V → + = (+g‘𝑄)) | 
| 172 | 169, 171 | ax-mp 5 | . . . . . 6
⊢  + =
(+g‘𝑄) | 
| 173 |  | eqid 2736 | . . . . . 6
⊢
(+g‘( Frac ‘ℤring)) =
(+g‘( Frac ‘ℤring)) | 
| 174 | 167, 168,
172, 173 | isghm 19234 | . . . . 5
⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac
‘ℤring)) ↔ ((𝑄 ∈ Grp ∧ ( Frac
‘ℤring) ∈ Grp) ∧ (𝐹:ℚ⟶(Base‘( Frac
‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 + 𝑝)) = ((𝐹‘𝑞)(+g‘( Frac
‘ℤring))(𝐹‘𝑝))))) | 
| 175 | 16, 166, 174 | mpbir2an 711 | . . . 4
⊢ 𝐹 ∈ (𝑄 GrpHom ( Frac
‘ℤring)) | 
| 176 |  | eqid 2736 | . . . . . . . 8
⊢
(mulGrp‘𝑄) =
(mulGrp‘𝑄) | 
| 177 | 176 | ringmgp 20237 | . . . . . . 7
⊢ (𝑄 ∈ Ring →
(mulGrp‘𝑄) ∈
Mnd) | 
| 178 | 4, 177 | ax-mp 5 | . . . . . 6
⊢
(mulGrp‘𝑄)
∈ Mnd | 
| 179 |  | eqid 2736 | . . . . . . . 8
⊢
(mulGrp‘( Frac ‘ℤring)) = (mulGrp‘(
Frac ‘ℤring)) | 
| 180 | 179 | ringmgp 20237 | . . . . . . 7
⊢ (( Frac
‘ℤring) ∈ Ring → (mulGrp‘( Frac
‘ℤring)) ∈ Mnd) | 
| 181 | 10, 180 | ax-mp 5 | . . . . . 6
⊢
(mulGrp‘( Frac ‘ℤring)) ∈
Mnd | 
| 182 | 178, 181 | pm3.2i 470 | . . . . 5
⊢
((mulGrp‘𝑄)
∈ Mnd ∧ (mulGrp‘( Frac ‘ℤring)) ∈
Mnd) | 
| 183 |  | eqid 2736 | . . . . . . . . . 10
⊢
(.r‘(ℤring RLocal (ℤ ∖
{0}))) = (.r‘(ℤring RLocal (ℤ ∖
{0}))) | 
| 184 | 28, 30, 144, 145, 24, 71, 76, 117, 122, 153, 157, 183 | rlocmulval 33274 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
([〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
(.r‘(ℤring RLocal (ℤ ∖
{0})))[〈(numer‘𝑝), (denom‘𝑝)〉] ∼ ) =
[〈((numer‘𝑞)
· (numer‘𝑝)),
((denom‘𝑞) ·
(denom‘𝑝))〉]
∼
) | 
| 185 | 79, 81 | mulcld 11282 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℂ) | 
| 186 |  | qmulcl 13010 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝑞 · 𝑝) ∈ ℚ) | 
| 187 |  | qdencl 16779 | . . . . . . . . . . . . . . . 16
⊢ ((𝑞 · 𝑝) ∈ ℚ → (denom‘(𝑞 · 𝑝)) ∈ ℕ) | 
| 188 | 186, 187 | syl 17 | . . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 ·
𝑝)) ∈
ℕ) | 
| 189 | 188 | nncnd 12283 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 ·
𝑝)) ∈
ℂ) | 
| 190 | 185, 189,
92 | mul32d 11472 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝)))) | 
| 191 | 79, 81, 88, 91 | mul4d 11474 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) = ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝)))) | 
| 192 | 191 | oveq1d 7447 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · ((denom‘𝑞) · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝)))) | 
| 193 | 190, 192 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝)))) | 
| 194 |  | qmuldeneqnum 16785 | . . . . . . . . . . . . . 14
⊢ ((𝑞 · 𝑝) ∈ ℚ → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝))) | 
| 195 | 186, 194 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) = (numer‘(𝑞 · 𝑝))) | 
| 196 | 195 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · 𝑝) · (denom‘(𝑞 · 𝑝))) · ((denom‘𝑞) · (denom‘𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))) | 
| 197 | 99, 104 | oveq12d 7450 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → ((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) = ((numer‘𝑞) · (numer‘𝑝))) | 
| 198 | 197 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (((𝑞 · (denom‘𝑞)) · (𝑝 · (denom‘𝑝))) · (denom‘(𝑞 · 𝑝))) = (((numer‘𝑞) · (numer‘𝑝)) · (denom‘(𝑞 · 𝑝)))) | 
| 199 | 193, 196,
198 | 3eqtr3rd 2785 | . . . . . . . . . . 11
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(((numer‘𝑞) ·
(numer‘𝑝)) ·
(denom‘(𝑞 ·
𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝)))) | 
| 200 | 117, 122 | zmulcld 12730 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
((numer‘𝑞) ·
(numer‘𝑝)) ∈
ℤ) | 
| 201 |  | qnumcl 16778 | . . . . . . . . . . . . 13
⊢ ((𝑞 · 𝑝) ∈ ℚ → (numer‘(𝑞 · 𝑝)) ∈ ℤ) | 
| 202 | 186, 201 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(numer‘(𝑞 ·
𝑝)) ∈
ℤ) | 
| 203 | 188 | nnzd 12642 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 ·
𝑝)) ∈
ℤ) | 
| 204 | 188 | nnne0d 12317 | . . . . . . . . . . . . . 14
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 ·
𝑝)) ≠
0) | 
| 205 | 203, 204 | eldifsnd 4786 | . . . . . . . . . . . . 13
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 ·
𝑝)) ∈ (ℤ ∖
{0})) | 
| 206 | 205, 39 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘(𝑞 ·
𝑝)) ∈
(RLReg‘ℤring)) | 
| 207 | 28, 30, 114, 71, 200, 202, 134, 206 | fracerl 33309 | . . . . . . . . . . 11
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(〈((numer‘𝑞)
· (numer‘𝑝)),
((denom‘𝑞) ·
(denom‘𝑝))〉
∼
〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉 ↔
(((numer‘𝑞) ·
(numer‘𝑝)) ·
(denom‘(𝑞 ·
𝑝))) = ((numer‘(𝑞 · 𝑝)) · ((denom‘𝑞) · (denom‘𝑝))))) | 
| 208 | 199, 207 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
〈((numer‘𝑞)
· (numer‘𝑝)),
((denom‘𝑞) ·
(denom‘𝑝))〉
∼
〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉) | 
| 209 | 77, 208 | erthi 8799 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
[〈((numer‘𝑞)
· (numer‘𝑝)),
((denom‘𝑞) ·
(denom‘𝑝))〉]
∼
= [〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉] ∼
) | 
| 210 | 184, 209 | eqtrd 2776 | . . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
([〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
(.r‘(ℤring RLocal (ℤ ∖
{0})))[〈(numer‘𝑝), (denom‘𝑝)〉] ∼ ) =
[〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉] ∼
) | 
| 211 | 41 | fveq2i 6908 | . . . . . . . . . 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 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‘(𝑞 · 𝑝))) | 
| 216 | 214, 215 | opeq12d 4880 | . . . . . . . . . 10
⊢ (𝑢 = (𝑞 · 𝑝) → 〈(numer‘𝑢), (denom‘𝑢)〉 =
〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉) | 
| 217 | 216 | eceq1d 8786 | . . . . . . . . 9
⊢ (𝑢 = (𝑞 · 𝑝) → [〈(numer‘𝑢), (denom‘𝑢)〉] ∼ =
[〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉] ∼
) | 
| 218 |  | ecexg 8750 | . . . . . . . . . 10
⊢ ( ∼ ∈
V → [〈(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))〉] ∼ ∈
V) | 
| 219 | 25, 218 | mp1i 13 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
[〈(numer‘(𝑞
· 𝑝)),
(denom‘(𝑞 ·
𝑝))〉] ∼ ∈
V) | 
| 220 | 68, 217, 186, 219 | fvmptd3 7038 | . . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = [〈(numer‘(𝑞 · 𝑝)), (denom‘(𝑞 · 𝑝))〉] ∼ ) | 
| 221 | 210, 213,
220 | 3eqtr4rd 2787 | . . . . . . 7
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) → (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(.r‘( Frac
‘ℤring))(𝐹‘𝑝))) | 
| 222 | 221 | rgen2 3198 | . . . . . 6
⊢
∀𝑞 ∈
ℚ ∀𝑝 ∈
ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(.r‘( Frac
‘ℤring))(𝐹‘𝑝)) | 
| 223 |  | zssq 12999 | . . . . . . . 8
⊢ ℤ
⊆ ℚ | 
| 224 |  | 1z 12649 | . . . . . . . 8
⊢ 1 ∈
ℤ | 
| 225 | 223, 224 | sselii 3979 | . . . . . . 7
⊢ 1 ∈
ℚ | 
| 226 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑞 = 1 → (numer‘𝑞) =
(numer‘1)) | 
| 227 |  | 1zzd 12650 | . . . . . . . . . . . . 13
⊢
(ℤring ∈ IDomn → 1 ∈
ℤ) | 
| 228 | 227 | znumd 32815 | . . . . . . . . . . . 12
⊢
(ℤring ∈ IDomn → (numer‘1) =
1) | 
| 229 | 5, 228 | ax-mp 5 | . . . . . . . . . . 11
⊢
(numer‘1) = 1 | 
| 230 | 226, 229 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑞 = 1 → (numer‘𝑞) = 1) | 
| 231 |  | fveq2 6905 | . . . . . . . . . . 11
⊢ (𝑞 = 1 → (denom‘𝑞) =
(denom‘1)) | 
| 232 | 227 | zdend 32816 | . . . . . . . . . . . 12
⊢
(ℤring ∈ IDomn → (denom‘1) =
1) | 
| 233 | 5, 232 | ax-mp 5 | . . . . . . . . . . 11
⊢
(denom‘1) = 1 | 
| 234 | 231, 233 | eqtrdi 2792 | . . . . . . . . . 10
⊢ (𝑞 = 1 → (denom‘𝑞) = 1) | 
| 235 | 230, 234 | opeq12d 4880 | . . . . . . . . 9
⊢ (𝑞 = 1 →
〈(numer‘𝑞),
(denom‘𝑞)〉 =
〈1, 1〉) | 
| 236 | 235 | eceq1d 8786 | . . . . . . . 8
⊢ (𝑞 = 1 →
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈1, 1〉] ∼ ) | 
| 237 | 236, 17, 49 | fvmpt3i 7020 | . . . . . . 7
⊢ (1 ∈
ℚ → (𝐹‘1)
= [〈1, 1〉] ∼ ) | 
| 238 | 225, 237 | ax-mp 5 | . . . . . 6
⊢ (𝐹‘1) = [〈1, 1〉]
∼ | 
| 239 | 47, 222, 238 | 3pm3.2i 1339 | . . . . 5
⊢ (𝐹:ℚ⟶(Base‘(
Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(.r‘( Frac
‘ℤring))(𝐹‘𝑝)) ∧ (𝐹‘1) = [〈1, 1〉] ∼
) | 
| 240 | 176, 167 | mgpbas 20143 | . . . . . 6
⊢ ℚ =
(Base‘(mulGrp‘𝑄)) | 
| 241 | 179, 168 | mgpbas 20143 | . . . . . 6
⊢
(Base‘( Frac ‘ℤring)) =
(Base‘(mulGrp‘( Frac
‘ℤring))) | 
| 242 |  | cnfldmul 21373 | . . . . . . . . 9
⊢  ·
= (.r‘ℂfld) | 
| 243 | 1, 242 | ressmulr 17352 | . . . . . . . 8
⊢ (ℚ
∈ V → · = (.r‘𝑄)) | 
| 244 | 169, 243 | ax-mp 5 | . . . . . . 7
⊢  ·
= (.r‘𝑄) | 
| 245 | 176, 244 | mgpplusg 20142 | . . . . . 6
⊢  ·
= (+g‘(mulGrp‘𝑄)) | 
| 246 |  | eqid 2736 | . . . . . . 7
⊢
(.r‘( Frac ‘ℤring)) =
(.r‘( Frac ‘ℤring)) | 
| 247 | 179, 246 | mgpplusg 20142 | . . . . . 6
⊢
(.r‘( Frac ‘ℤring)) =
(+g‘(mulGrp‘( Frac
‘ℤring))) | 
| 248 | 1 | qrng1 27667 | . . . . . . 7
⊢ 1 =
(1r‘𝑄) | 
| 249 | 176, 248 | ringidval 20181 | . . . . . 6
⊢ 1 =
(0g‘(mulGrp‘𝑄)) | 
| 250 | 146 | a1i 11 | . . . . . . . . 9
⊢
(ℤring ∈ IDomn → ℤring
∈ CRing) | 
| 251 | 149 | a1i 11 | . . . . . . . . 9
⊢
(ℤring ∈ IDomn → (ℤ ∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring))) | 
| 252 |  | eqid 2736 | . . . . . . . . 9
⊢ [〈1,
1〉] ∼ = [〈1,
1〉] ∼ | 
| 253 | 29, 69, 41, 24, 250, 251, 252 | rloc1r 33277 | . . . . . . . 8
⊢
(ℤring ∈ IDomn → [〈1, 1〉] ∼ =
(1r‘( Frac ‘ℤring))) | 
| 254 | 5, 253 | ax-mp 5 | . . . . . . 7
⊢ [〈1,
1〉] ∼ =
(1r‘( Frac ‘ℤring)) | 
| 255 | 179, 254 | ringidval 20181 | . . . . . 6
⊢ [〈1,
1〉] ∼ =
(0g‘(mulGrp‘( Frac
‘ℤring))) | 
| 256 | 240, 241,
245, 247, 249, 255 | ismhm 18799 | . . . . 5
⊢ (𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac
‘ℤring))) ↔ (((mulGrp‘𝑄) ∈ Mnd ∧ (mulGrp‘( Frac
‘ℤring)) ∈ Mnd) ∧ (𝐹:ℚ⟶(Base‘( Frac
‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ (𝐹‘(𝑞 · 𝑝)) = ((𝐹‘𝑞)(.r‘( Frac
‘ℤring))(𝐹‘𝑝)) ∧ (𝐹‘1) = [〈1, 1〉] ∼
))) | 
| 257 | 182, 239,
256 | mpbir2an 711 | . . . 4
⊢ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac
‘ℤring))) | 
| 258 | 175, 257 | pm3.2i 470 | . . 3
⊢ (𝐹 ∈ (𝑄 GrpHom ( Frac
‘ℤring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac
‘ℤring)))) | 
| 259 | 176, 179 | isrhm 20479 | . . 3
⊢ (𝐹 ∈ (𝑄 RingHom ( Frac
‘ℤring)) ↔ ((𝑄 ∈ Ring ∧ ( Frac
‘ℤring) ∈ Ring) ∧ (𝐹 ∈ (𝑄 GrpHom ( Frac
‘ℤring)) ∧ 𝐹 ∈ ((mulGrp‘𝑄) MndHom (mulGrp‘( Frac
‘ℤring)))))) | 
| 260 | 11, 258, 259 | mpbir2an 711 | . 2
⊢ 𝐹 ∈ (𝑄 RingHom ( Frac
‘ℤring)) | 
| 261 | 46 | rgen 3062 | . . . 4
⊢
∀𝑞 ∈
ℚ [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ∈
(Base‘( Frac ‘ℤring)) | 
| 262 | 117 | zcnd 12725 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(numer‘𝑞) ∈
ℂ) | 
| 263 | 122 | zcnd 12725 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(numer‘𝑝) ∈
ℂ) | 
| 264 | 21 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑞) ≠
0) | 
| 265 | 155 | adantl 481 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑝) ≠
0) | 
| 266 | 262, 88, 263, 91, 264, 265 | divmuleqd 12090 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(((numer‘𝑞) /
(denom‘𝑞)) =
((numer‘𝑝) /
(denom‘𝑝)) ↔
((numer‘𝑞) ·
(denom‘𝑝)) =
((numer‘𝑝) ·
(denom‘𝑞)))) | 
| 267 | 153, 39 | eleqtrdi 2850 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑞) ∈
(RLReg‘ℤring)) | 
| 268 | 157, 39 | eleqtrdi 2850 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(denom‘𝑝) ∈
(RLReg‘ℤring)) | 
| 269 | 28, 30, 114, 71, 117, 122, 267, 268 | fracerl 33309 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(〈(numer‘𝑞),
(denom‘𝑞)〉 ∼
〈(numer‘𝑝),
(denom‘𝑝)〉
↔ ((numer‘𝑞)
· (denom‘𝑝)) =
((numer‘𝑝) ·
(denom‘𝑞)))) | 
| 270 | 23 | adantr 480 | . . . . . . . . . 10
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
〈(numer‘𝑞),
(denom‘𝑞)〉
∈ (ℤ × (ℤ ∖ {0}))) | 
| 271 | 77, 270 | erth 8797 | . . . . . . . . 9
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
(〈(numer‘𝑞),
(denom‘𝑞)〉 ∼
〈(numer‘𝑝),
(denom‘𝑝)〉
↔ [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ =
[〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
)) | 
| 272 | 266, 269,
271 | 3bitr2rd 308 | . . . . . . . 8
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
([〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
↔ ((numer‘𝑞) /
(denom‘𝑞)) =
((numer‘𝑝) /
(denom‘𝑝)))) | 
| 273 | 272 | biimpa 476 | . . . . . . 7
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
) → ((numer‘𝑞) /
(denom‘𝑞)) =
((numer‘𝑝) /
(denom‘𝑝))) | 
| 274 |  | qeqnumdivden 16784 | . . . . . . . 8
⊢ (𝑞 ∈ ℚ → 𝑞 = ((numer‘𝑞) / (denom‘𝑞))) | 
| 275 | 274 | ad2antrr 726 | . . . . . . 7
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
) → 𝑞 =
((numer‘𝑞) /
(denom‘𝑞))) | 
| 276 |  | qeqnumdivden 16784 | . . . . . . . 8
⊢ (𝑝 ∈ ℚ → 𝑝 = ((numer‘𝑝) / (denom‘𝑝))) | 
| 277 | 276 | ad2antlr 727 | . . . . . . 7
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
) → 𝑝 =
((numer‘𝑝) /
(denom‘𝑝))) | 
| 278 | 273, 275,
277 | 3eqtr4d 2786 | . . . . . 6
⊢ (((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) ∧
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
) → 𝑞 = 𝑝) | 
| 279 | 278 | ex 412 | . . . . 5
⊢ ((𝑞 ∈ ℚ ∧ 𝑝 ∈ ℚ) →
([〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
→ 𝑞 = 𝑝)) | 
| 280 | 279 | rgen2 3198 | . . . 4
⊢
∀𝑞 ∈
ℚ ∀𝑝 ∈
ℚ ([〈(numer‘𝑞), (denom‘𝑞)〉] ∼ =
[〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
→ 𝑞 = 𝑝) | 
| 281 | 17, 56 | f1mpt 7282 | . . . 4
⊢ (𝐹:ℚ–1-1→(Base‘( Frac
‘ℤring)) ↔ (∀𝑞 ∈ ℚ [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ∈
(Base‘( Frac ‘ℤring)) ∧ ∀𝑞 ∈ ℚ ∀𝑝 ∈ ℚ
([〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
= [〈(numer‘𝑝),
(denom‘𝑝)〉]
∼
→ 𝑞 = 𝑝))) | 
| 282 | 261, 280,
281 | mpbir2an 711 | . . 3
⊢ 𝐹:ℚ–1-1→(Base‘( Frac
‘ℤring)) | 
| 283 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑞 = (𝑎 / 𝑏) → (numer‘𝑞) = (numer‘(𝑎 / 𝑏))) | 
| 284 |  | fveq2 6905 | . . . . . . . . . 10
⊢ (𝑞 = (𝑎 / 𝑏) → (denom‘𝑞) = (denom‘(𝑎 / 𝑏))) | 
| 285 | 283, 284 | opeq12d 4880 | . . . . . . . . 9
⊢ (𝑞 = (𝑎 / 𝑏) → 〈(numer‘𝑞), (denom‘𝑞)〉 =
〈(numer‘(𝑎 /
𝑏)), (denom‘(𝑎 / 𝑏))〉) | 
| 286 | 285 | eceq1d 8786 | . . . . . . . 8
⊢ (𝑞 = (𝑎 / 𝑏) → [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ =
[〈(numer‘(𝑎 /
𝑏)), (denom‘(𝑎 / 𝑏))〉] ∼ ) | 
| 287 | 286 | eqeq2d 2747 | . . . . . . 7
⊢ (𝑞 = (𝑎 / 𝑏) → (𝑧 = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ↔ 𝑧 = [〈(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))〉] ∼ )) | 
| 288 |  | simpllr 775 | . . . . . . . . 9
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑎 ∈
ℤ) | 
| 289 | 223, 288 | sselid 3980 | . . . . . . . 8
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑎 ∈
ℚ) | 
| 290 |  | simplr 768 | . . . . . . . . . 10
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑏 ∈ (ℤ ∖
{0})) | 
| 291 | 290 | eldifad 3962 | . . . . . . . . 9
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑏 ∈
ℤ) | 
| 292 | 223, 291 | sselid 3980 | . . . . . . . 8
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑏 ∈
ℚ) | 
| 293 |  | eldifsni 4789 | . . . . . . . . 9
⊢ (𝑏 ∈ (ℤ ∖ {0})
→ 𝑏 ≠
0) | 
| 294 | 290, 293 | syl 17 | . . . . . . . 8
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑏 ≠ 0) | 
| 295 |  | qdivcl 13013 | . . . . . . . 8
⊢ ((𝑎 ∈ ℚ ∧ 𝑏 ∈ ℚ ∧ 𝑏 ≠ 0) → (𝑎 / 𝑏) ∈ ℚ) | 
| 296 | 289, 292,
294, 295 | syl3anc 1372 | . . . . . . 7
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → (𝑎 / 𝑏) ∈ ℚ) | 
| 297 |  | simpr 484 | . . . . . . . 8
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑧 = [〈𝑎, 𝑏〉] ∼ ) | 
| 298 | 146 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) →
ℤring ∈ CRing) | 
| 299 | 149 | a1i 11 | . . . . . . . . . 10
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → (ℤ
∖ {0}) ∈
(SubMnd‘(mulGrp‘ℤring))) | 
| 300 | 28, 29, 69, 30, 31, 32, 24, 298, 299 | erler 33270 | . . . . . . . . 9
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → ∼ Er
(ℤ × (ℤ ∖ {0}))) | 
| 301 |  | simpl 482 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑎 ∈
ℤ) | 
| 302 | 301 | zcnd 12725 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑎 ∈
ℂ) | 
| 303 |  | eldifi 4130 | . . . . . . . . . . . . . . . 16
⊢ (𝑏 ∈ (ℤ ∖ {0})
→ 𝑏 ∈
ℤ) | 
| 304 | 303 | adantl 481 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑏 ∈
ℤ) | 
| 305 | 304 | zcnd 12725 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑏 ∈
ℂ) | 
| 306 | 293 | adantl 481 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑏 ≠
0) | 
| 307 | 302, 305,
306 | divcld 12044 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (𝑎 / 𝑏) ∈
ℂ) | 
| 308 | 223, 301 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑎 ∈
ℚ) | 
| 309 | 223, 304 | sselid 3980 | . . . . . . . . . . . . . . . 16
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑏 ∈
ℚ) | 
| 310 | 308, 309,
306, 295 | syl3anc 1372 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (𝑎 / 𝑏) ∈
ℚ) | 
| 311 |  | qdencl 16779 | . . . . . . . . . . . . . . 15
⊢ ((𝑎 / 𝑏) ∈ ℚ → (denom‘(𝑎 / 𝑏)) ∈ ℕ) | 
| 312 | 310, 311 | syl 17 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (denom‘(𝑎 /
𝑏)) ∈
ℕ) | 
| 313 | 312 | nncnd 12283 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (denom‘(𝑎 /
𝑏)) ∈
ℂ) | 
| 314 | 307, 313,
305 | mul32d 11472 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏)))) | 
| 315 |  | qmuldeneqnum 16785 | . . . . . . . . . . . . . 14
⊢ ((𝑎 / 𝑏) ∈ ℚ → ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏))) | 
| 316 | 310, 315 | syl 17 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ ((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) = (numer‘(𝑎 / 𝑏))) | 
| 317 | 316 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (((𝑎 / 𝑏) · (denom‘(𝑎 / 𝑏))) · 𝑏) = ((numer‘(𝑎 / 𝑏)) · 𝑏)) | 
| 318 | 302, 305,
306 | divcan1d 12045 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ ((𝑎 / 𝑏) · 𝑏) = 𝑎) | 
| 319 | 318 | oveq1d 7447 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (((𝑎 / 𝑏) · 𝑏) · (denom‘(𝑎 / 𝑏))) = (𝑎 · (denom‘(𝑎 / 𝑏)))) | 
| 320 | 314, 317,
319 | 3eqtr3rd 2785 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (𝑎 ·
(denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏)) | 
| 321 | 146 | a1i 11 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ ℤring ∈ CRing) | 
| 322 |  | qnumcl 16778 | . . . . . . . . . . . . 13
⊢ ((𝑎 / 𝑏) ∈ ℚ → (numer‘(𝑎 / 𝑏)) ∈ ℤ) | 
| 323 | 310, 322 | syl 17 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (numer‘(𝑎 /
𝑏)) ∈
ℤ) | 
| 324 |  | simpr 484 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑏 ∈ (ℤ
∖ {0})) | 
| 325 | 324, 39 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 𝑏 ∈
(RLReg‘ℤring)) | 
| 326 | 312 | nnzd 12642 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (denom‘(𝑎 /
𝑏)) ∈
ℤ) | 
| 327 | 312 | nnne0d 12317 | . . . . . . . . . . . . . 14
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (denom‘(𝑎 /
𝑏)) ≠
0) | 
| 328 | 326, 327 | eldifsnd 4786 | . . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (denom‘(𝑎 /
𝑏)) ∈ (ℤ ∖
{0})) | 
| 329 | 328, 39 | eleqtrdi 2850 | . . . . . . . . . . . 12
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (denom‘(𝑎 /
𝑏)) ∈
(RLReg‘ℤring)) | 
| 330 | 28, 30, 114, 321, 301, 323, 325, 329 | fracerl 33309 | . . . . . . . . . . 11
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ (〈𝑎, 𝑏〉 ∼
〈(numer‘(𝑎 /
𝑏)), (denom‘(𝑎 / 𝑏))〉 ↔ (𝑎 · (denom‘(𝑎 / 𝑏))) = ((numer‘(𝑎 / 𝑏)) · 𝑏))) | 
| 331 | 320, 330 | mpbird 257 | . . . . . . . . . 10
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ (ℤ ∖ {0}))
→ 〈𝑎, 𝑏〉 ∼
〈(numer‘(𝑎 /
𝑏)), (denom‘(𝑎 / 𝑏))〉) | 
| 332 | 331 | ad4ant23 753 | . . . . . . . . 9
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) →
〈𝑎, 𝑏〉 ∼
〈(numer‘(𝑎 /
𝑏)), (denom‘(𝑎 / 𝑏))〉) | 
| 333 | 300, 332 | erthi 8799 | . . . . . . . 8
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) →
[〈𝑎, 𝑏〉] ∼ =
[〈(numer‘(𝑎 /
𝑏)), (denom‘(𝑎 / 𝑏))〉] ∼ ) | 
| 334 | 297, 333 | eqtrd 2776 | . . . . . . 7
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) → 𝑧 = [〈(numer‘(𝑎 / 𝑏)), (denom‘(𝑎 / 𝑏))〉] ∼ ) | 
| 335 | 287, 296,
334 | rspcedvdw 3624 | . . . . . 6
⊢ ((((𝑧 ∈ (Base‘( Frac
‘ℤring)) ∧ 𝑎 ∈ ℤ) ∧ 𝑏 ∈ (ℤ ∖ {0})) ∧ 𝑧 = [〈𝑎, 𝑏〉] ∼ ) →
∃𝑞 ∈ ℚ
𝑧 =
[〈(numer‘𝑞),
(denom‘𝑞)〉]
∼
) | 
| 336 | 45 | eleq2i 2832 | . . . . . . . 8
⊢ (𝑧 ∈ ((ℤ ×
(ℤ ∖ {0})) / ∼ ) ↔ 𝑧 ∈ (Base‘( Frac
‘ℤring))) | 
| 337 | 336 | biimpri 228 | . . . . . . 7
⊢ (𝑧 ∈ (Base‘( Frac
‘ℤring)) → 𝑧 ∈ ((ℤ × (ℤ ∖
{0})) / ∼ )) | 
| 338 | 337 | elrlocbasi 33271 | . . . . . 6
⊢ (𝑧 ∈ (Base‘( Frac
‘ℤring)) → ∃𝑎 ∈ ℤ ∃𝑏 ∈ (ℤ ∖ {0})𝑧 = [〈𝑎, 𝑏〉] ∼ ) | 
| 339 | 335, 338 | r19.29vva 3215 | . . . . 5
⊢ (𝑧 ∈ (Base‘( Frac
‘ℤring)) → ∃𝑞 ∈ ℚ 𝑧 = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ) | 
| 340 | 339 | rgen 3062 | . . . 4
⊢
∀𝑧 ∈
(Base‘( Frac ‘ℤring))∃𝑞 ∈ ℚ 𝑧 = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ | 
| 341 | 17 | fompt 7137 | . . . 4
⊢ (𝐹:ℚ–onto→(Base‘( Frac
‘ℤring)) ↔ (∀𝑞 ∈ ℚ [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ ∈
(Base‘( Frac ‘ℤring)) ∧ ∀𝑧 ∈ (Base‘( Frac
‘ℤring))∃𝑞 ∈ ℚ 𝑧 = [〈(numer‘𝑞), (denom‘𝑞)〉] ∼ )) | 
| 342 | 261, 340,
341 | mpbir2an 711 | . . 3
⊢ 𝐹:ℚ–onto→(Base‘( Frac
‘ℤring)) | 
| 343 |  | df-f1o 6567 | . . 3
⊢ (𝐹:ℚ–1-1-onto→(Base‘( Frac
‘ℤring)) ↔ (𝐹:ℚ–1-1→(Base‘( Frac
‘ℤring)) ∧ 𝐹:ℚ–onto→(Base‘( Frac
‘ℤring)))) | 
| 344 | 282, 342,
343 | mpbir2an 711 | . 2
⊢ 𝐹:ℚ–1-1-onto→(Base‘( Frac
‘ℤring)) | 
| 345 | 167, 168 | isrim 20493 | . 2
⊢ (𝐹 ∈ (𝑄 RingIso ( Frac
‘ℤring)) ↔ (𝐹 ∈ (𝑄 RingHom ( Frac
‘ℤring)) ∧ 𝐹:ℚ–1-1-onto→(Base‘( Frac
‘ℤring)))) | 
| 346 | 260, 344,
345 | mpbir2an 711 | 1
⊢ 𝐹 ∈ (𝑄 RingIso ( Frac
‘ℤring)) |