Step | Hyp | Ref
| Expression |
1 | | pzriprng.r |
. . . . 5
⊢ 𝑅 = (ℤring
×s ℤring) |
2 | 1 | pzriprnglem1 21387 |
. . . 4
⊢ 𝑅 ∈ Rng |
3 | | rnggrp 20082 |
. . . 4
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
4 | 2, 3 | ax-mp 5 |
. . 3
⊢ 𝑅 ∈ Grp |
5 | | pzriprng.i |
. . . . 5
⊢ 𝐼 = (ℤ ×
{0}) |
6 | | 0z 12585 |
. . . . . 6
⊢ 0 ∈
ℤ |
7 | | snssi 4807 |
. . . . . 6
⊢ (0 ∈
ℤ → {0} ⊆ ℤ) |
8 | | xpss2 5692 |
. . . . . 6
⊢ ({0}
⊆ ℤ → (ℤ × {0}) ⊆ (ℤ ×
ℤ)) |
9 | 6, 7, 8 | mp2b 10 |
. . . . 5
⊢ (ℤ
× {0}) ⊆ (ℤ × ℤ) |
10 | 5, 9 | eqsstri 4012 |
. . . 4
⊢ 𝐼 ⊆ (ℤ ×
ℤ) |
11 | 10 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝐼 ⊆ (ℤ ×
ℤ)) |
12 | | opelxpi 5709 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
⟨𝑋, 𝑌⟩ ∈ (ℤ ×
ℤ)) |
13 | 1 | pzriprnglem2 21388 |
. . . . 5
⊢
(Base‘𝑅) =
(ℤ × ℤ) |
14 | 13 | eqcomi 2736 |
. . . 4
⊢ (ℤ
× ℤ) = (Base‘𝑅) |
15 | | pzriprng.g |
. . . 4
⊢ ∼ =
(𝑅 ~QG
𝐼) |
16 | | eqid 2727 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
17 | 14, 15, 16 | eqglact 19118 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ⊆ (ℤ ×
ℤ) ∧ ⟨𝑋,
𝑌⟩ ∈ (ℤ
× ℤ)) → [⟨𝑋, 𝑌⟩] ∼ = ((𝑥 ∈ (ℤ ×
ℤ) ↦ (⟨𝑋,
𝑌⟩(+g‘𝑅)𝑥)) “ 𝐼)) |
18 | 4, 11, 12, 17 | mp3an2i 1463 |
. 2
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
[⟨𝑋, 𝑌⟩] ∼ = ((𝑥 ∈ (ℤ ×
ℤ) ↦ (⟨𝑋,
𝑌⟩(+g‘𝑅)𝑥)) “ 𝐼)) |
19 | 11 | mptimass 6070 |
. 2
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑥 ∈ (ℤ ×
ℤ) ↦ (⟨𝑋,
𝑌⟩(+g‘𝑅)𝑥)) “ 𝐼) = ran (𝑥 ∈ 𝐼 ↦ (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥))) |
20 | | eqid 2727 |
. . . . 5
⊢ (𝑥 ∈ 𝐼 ↦ (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)) = (𝑥 ∈ 𝐼 ↦ (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)) |
21 | 20 | rnmpt 5951 |
. . . 4
⊢ ran
(𝑥 ∈ 𝐼 ↦ (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)) = {𝑒 ∣ ∃𝑥 ∈ 𝐼 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)} |
22 | 21 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ran
(𝑥 ∈ 𝐼 ↦ (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)) = {𝑒 ∣ ∃𝑥 ∈ 𝐼 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)}) |
23 | 5 | rexeqi 3319 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐼 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥) ↔ ∃𝑥 ∈ (ℤ × {0})𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)) |
24 | | oveq2 7422 |
. . . . . . . 8
⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥) = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩)) |
25 | 24 | eqeq2d 2738 |
. . . . . . 7
⊢ (𝑥 = ⟨𝑎, 𝑏⟩ → (𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥) ↔ 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩))) |
26 | 25 | rexxp 5839 |
. . . . . 6
⊢
(∃𝑥 ∈
(ℤ × {0})𝑒 =
(⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩)) |
27 | 23, 26 | bitri 275 |
. . . . 5
⊢
(∃𝑥 ∈
𝐼 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩)) |
28 | 27 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑥 ∈ 𝐼 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥) ↔ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩))) |
29 | 28 | abbidv 2796 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑥 ∈ 𝐼 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)} = {𝑒 ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩)}) |
30 | | c0ex 11224 |
. . . . . . . 8
⊢ 0 ∈
V |
31 | | opeq2 4870 |
. . . . . . . . . 10
⊢ (𝑏 = 0 → ⟨𝑎, 𝑏⟩ = ⟨𝑎, 0⟩) |
32 | 31 | oveq2d 7430 |
. . . . . . . . 9
⊢ (𝑏 = 0 → (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩) = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 0⟩)) |
33 | 32 | eqeq2d 2738 |
. . . . . . . 8
⊢ (𝑏 = 0 → (𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩) ↔ 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 0⟩))) |
34 | 30, 33 | rexsn 4682 |
. . . . . . 7
⊢
(∃𝑏 ∈
{0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩) ↔ 𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 0⟩)) |
35 | | zringbas 21359 |
. . . . . . . . 9
⊢ ℤ =
(Base‘ℤring) |
36 | | zringring 21355 |
. . . . . . . . . 10
⊢
ℤring ∈ Ring |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) →
ℤring ∈ Ring) |
38 | | simpll 766 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 𝑋 ∈
ℤ) |
39 | | simplr 768 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 𝑌 ∈
ℤ) |
40 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 𝑎 ∈
ℤ) |
41 | | 0zd 12586 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 0 ∈
ℤ) |
42 | 38, 40 | zaddcld 12686 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑋 + 𝑎) ∈ ℤ) |
43 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝑌 ∈
ℤ) |
44 | | 0zd 12586 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 0 ∈
ℤ) |
45 | 43, 44 | zaddcld 12686 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 + 0) ∈
ℤ) |
46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑌 + 0) ∈
ℤ) |
47 | | zringplusg 21360 |
. . . . . . . . 9
⊢ + =
(+g‘ℤring) |
48 | 1, 35, 35, 37, 37, 38, 39, 40, 41, 42, 46, 47, 47, 16 | xpsadd 17541 |
. . . . . . . 8
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) →
(⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 0⟩) = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩) |
49 | 48 | eqeq2d 2738 |
. . . . . . 7
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 0⟩) ↔ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩)) |
50 | 34, 49 | bitrid 283 |
. . . . . 6
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) →
(∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩) ↔ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩)) |
51 | 50 | rexbidva 3171 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩) ↔ ∃𝑎 ∈ ℤ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩)) |
52 | 51 | abbidv 2796 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩)} = {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩}) |
53 | | iunab 5048 |
. . . . . 6
⊢ ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} = {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} |
54 | 53 | eqcomi 2736 |
. . . . 5
⊢ {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} = ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} |
55 | 54 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} = ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩}) |
56 | | zcn 12579 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℤ → 𝑌 ∈
ℂ) |
57 | 56 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝑌 ∈
ℂ) |
58 | 57 | addridd 11430 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 + 0) = 𝑌) |
59 | 58 | opeq2d 4876 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
⟨(𝑋 + 𝑎), (𝑌 + 0)⟩ = ⟨(𝑋 + 𝑎), 𝑌⟩) |
60 | 59 | eqeq2d 2738 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩ ↔ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩)) |
61 | 60 | abbidv 2796 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} = {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩}) |
62 | 61 | iuneq2d 5020 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} = ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩}) |
63 | | df-sn 4625 |
. . . . . . . . 9
⊢
{⟨(𝑋 + 𝑎), 𝑌⟩} = {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩} |
64 | 63 | eqcomi 2736 |
. . . . . . . 8
⊢ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩} = {⟨(𝑋 + 𝑎), 𝑌⟩} |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩} = {⟨(𝑋 + 𝑎), 𝑌⟩}) |
66 | 65 | iuneq2i 5012 |
. . . . . 6
⊢ ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩} = ∪ 𝑎 ∈ ℤ {⟨(𝑋 + 𝑎), 𝑌⟩} |
67 | 66 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), 𝑌⟩} = ∪ 𝑎 ∈ ℤ {⟨(𝑋 + 𝑎), 𝑌⟩}) |
68 | | velsn 4640 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {⟨(𝑋 + 𝑎), 𝑌⟩} ↔ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) |
69 | 68 | rexbii 3089 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
ℤ 𝑦 ∈
{⟨(𝑋 + 𝑎), 𝑌⟩} ↔ ∃𝑎 ∈ ℤ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) |
70 | 42 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) ∧ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) → (𝑋 + 𝑎) ∈ ℤ) |
71 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑎 ∈
ℤ) ∧ 𝑦 =
⟨(𝑋 + 𝑎), 𝑌⟩) ∧ 𝑏 = (𝑋 + 𝑎)) → 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) |
72 | | opeq1 4869 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑋 + 𝑎) → ⟨𝑏, 𝑌⟩ = ⟨(𝑋 + 𝑎), 𝑌⟩) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑎 ∈
ℤ) ∧ 𝑦 =
⟨(𝑋 + 𝑎), 𝑌⟩) ∧ 𝑏 = (𝑋 + 𝑎)) → ⟨𝑏, 𝑌⟩ = ⟨(𝑋 + 𝑎), 𝑌⟩) |
74 | 71, 73 | eqeq12d 2743 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑎 ∈
ℤ) ∧ 𝑦 =
⟨(𝑋 + 𝑎), 𝑌⟩) ∧ 𝑏 = (𝑋 + 𝑎)) → (𝑦 = ⟨𝑏, 𝑌⟩ ↔ ⟨(𝑋 + 𝑎), 𝑌⟩ = ⟨(𝑋 + 𝑎), 𝑌⟩)) |
75 | | eqidd 2728 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) ∧ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) → ⟨(𝑋 + 𝑎), 𝑌⟩ = ⟨(𝑋 + 𝑎), 𝑌⟩) |
76 | 70, 74, 75 | rspcedvd 3609 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) ∧ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) → ∃𝑏 ∈ ℤ 𝑦 = ⟨𝑏, 𝑌⟩) |
77 | 76 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩ → ∃𝑏 ∈ ℤ 𝑦 = ⟨𝑏, 𝑌⟩)) |
78 | 77 | rexlimdva 3150 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩ → ∃𝑏 ∈ ℤ 𝑦 = ⟨𝑏, 𝑌⟩)) |
79 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
80 | | simpll 766 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈
ℤ) |
81 | 79, 80 | zsubcld 12687 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑏 − 𝑋) ∈ ℤ) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = ⟨𝑏, 𝑌⟩) → (𝑏 − 𝑋) ∈ ℤ) |
83 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
⟨𝑏, 𝑌⟩) ∧ 𝑎 = (𝑏 − 𝑋)) → 𝑦 = ⟨𝑏, 𝑌⟩) |
84 | | oveq2 7422 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑏 − 𝑋) → (𝑋 + 𝑎) = (𝑋 + (𝑏 − 𝑋))) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
⟨𝑏, 𝑌⟩) ∧ 𝑎 = (𝑏 − 𝑋)) → (𝑋 + 𝑎) = (𝑋 + (𝑏 − 𝑋))) |
86 | 85 | opeq1d 4875 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
⟨𝑏, 𝑌⟩) ∧ 𝑎 = (𝑏 − 𝑋)) → ⟨(𝑋 + 𝑎), 𝑌⟩ = ⟨(𝑋 + (𝑏 − 𝑋)), 𝑌⟩) |
87 | 83, 86 | eqeq12d 2743 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
⟨𝑏, 𝑌⟩) ∧ 𝑎 = (𝑏 − 𝑋)) → (𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩ ↔ ⟨𝑏, 𝑌⟩ = ⟨(𝑋 + (𝑏 − 𝑋)), 𝑌⟩)) |
88 | | zcn 12579 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ ℤ → 𝑋 ∈
ℂ) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝑋 ∈
ℂ) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈
ℂ) |
91 | | zcn 12579 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℂ) |
93 | 90, 92 | pncan3d 11590 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑋 + (𝑏 − 𝑋)) = 𝑏) |
94 | 93 | eqcomd 2733 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 = (𝑋 + (𝑏 − 𝑋))) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = ⟨𝑏, 𝑌⟩) → 𝑏 = (𝑋 + (𝑏 − 𝑋))) |
96 | 95 | opeq1d 4875 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = ⟨𝑏, 𝑌⟩) → ⟨𝑏, 𝑌⟩ = ⟨(𝑋 + (𝑏 − 𝑋)), 𝑌⟩) |
97 | 82, 87, 96 | rspcedvd 3609 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = ⟨𝑏, 𝑌⟩) → ∃𝑎 ∈ ℤ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩) |
98 | 97 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑦 = ⟨𝑏, 𝑌⟩ → ∃𝑎 ∈ ℤ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩)) |
99 | 98 | rexlimdva 3150 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑏 ∈ ℤ
𝑦 = ⟨𝑏, 𝑌⟩ → ∃𝑎 ∈ ℤ 𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩)) |
100 | 78, 99 | impbid 211 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 = ⟨(𝑋 + 𝑎), 𝑌⟩ ↔ ∃𝑏 ∈ ℤ 𝑦 = ⟨𝑏, 𝑌⟩)) |
101 | 69, 100 | bitrid 283 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 ∈ {⟨(𝑋 + 𝑎), 𝑌⟩} ↔ ∃𝑏 ∈ ℤ 𝑦 = ⟨𝑏, 𝑌⟩)) |
102 | | opeq2 4870 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑌 → ⟨𝑏, 𝑐⟩ = ⟨𝑏, 𝑌⟩) |
103 | 102 | eqeq2d 2738 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑌 → (𝑦 = ⟨𝑏, 𝑐⟩ ↔ 𝑦 = ⟨𝑏, 𝑌⟩)) |
104 | 103 | rexsng 4674 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℤ →
(∃𝑐 ∈ {𝑌}𝑦 = ⟨𝑏, 𝑐⟩ ↔ 𝑦 = ⟨𝑏, 𝑌⟩)) |
105 | 104 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑐 ∈ {𝑌}𝑦 = ⟨𝑏, 𝑐⟩ ↔ 𝑦 = ⟨𝑏, 𝑌⟩)) |
106 | 105 | bicomd 222 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑦 = ⟨𝑏, 𝑌⟩ ↔ ∃𝑐 ∈ {𝑌}𝑦 = ⟨𝑏, 𝑐⟩)) |
107 | 106 | rexbidv 3173 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑏 ∈ ℤ
𝑦 = ⟨𝑏, 𝑌⟩ ↔ ∃𝑏 ∈ ℤ ∃𝑐 ∈ {𝑌}𝑦 = ⟨𝑏, 𝑐⟩)) |
108 | 101, 107 | bitrd 279 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 ∈ {⟨(𝑋 + 𝑎), 𝑌⟩} ↔ ∃𝑏 ∈ ℤ ∃𝑐 ∈ {𝑌}𝑦 = ⟨𝑏, 𝑐⟩)) |
109 | | eliun 4995 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝑎 ∈ ℤ {⟨(𝑋 + 𝑎), 𝑌⟩} ↔ ∃𝑎 ∈ ℤ 𝑦 ∈ {⟨(𝑋 + 𝑎), 𝑌⟩}) |
110 | | elxp2 5696 |
. . . . . . 7
⊢ (𝑦 ∈ (ℤ × {𝑌}) ↔ ∃𝑏 ∈ ℤ ∃𝑐 ∈ {𝑌}𝑦 = ⟨𝑏, 𝑐⟩) |
111 | 108, 109,
110 | 3bitr4g 314 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑦 ∈ ∪ 𝑎 ∈ ℤ {⟨(𝑋 + 𝑎), 𝑌⟩} ↔ 𝑦 ∈ (ℤ × {𝑌}))) |
112 | 111 | eqrdv 2725 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {⟨(𝑋 + 𝑎), 𝑌⟩} = (ℤ × {𝑌})) |
113 | 62, 67, 112 | 3eqtrd 2771 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = ⟨(𝑋 + 𝑎), (𝑌 + 0)⟩} = (ℤ × {𝑌})) |
114 | 52, 55, 113 | 3eqtrd 2771 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (⟨𝑋, 𝑌⟩(+g‘𝑅)⟨𝑎, 𝑏⟩)} = (ℤ × {𝑌})) |
115 | 22, 29, 114 | 3eqtrd 2771 |
. 2
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ran
(𝑥 ∈ 𝐼 ↦ (⟨𝑋, 𝑌⟩(+g‘𝑅)𝑥)) = (ℤ × {𝑌})) |
116 | 18, 19, 115 | 3eqtrd 2771 |
1
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
[⟨𝑋, 𝑌⟩] ∼ = (ℤ ×
{𝑌})) |