Step | Hyp | Ref
| Expression |
1 | | pzriprng.r |
. . . . 5
⊢ 𝑅 = (ℤring
×s ℤring) |
2 | 1 | pzriprnglem1 21406 |
. . . 4
⊢ 𝑅 ∈ Rng |
3 | | rnggrp 20097 |
. . . 4
⊢ (𝑅 ∈ Rng → 𝑅 ∈ Grp) |
4 | 2, 3 | ax-mp 5 |
. . 3
⊢ 𝑅 ∈ Grp |
5 | | pzriprng.i |
. . . . 5
⊢ 𝐼 = (ℤ ×
{0}) |
6 | | 0z 12599 |
. . . . . 6
⊢ 0 ∈
ℤ |
7 | | snssi 4812 |
. . . . . 6
⊢ (0 ∈
ℤ → {0} ⊆ ℤ) |
8 | | xpss2 5698 |
. . . . . 6
⊢ ({0}
⊆ ℤ → (ℤ × {0}) ⊆ (ℤ ×
ℤ)) |
9 | 6, 7, 8 | mp2b 10 |
. . . . 5
⊢ (ℤ
× {0}) ⊆ (ℤ × ℤ) |
10 | 5, 9 | eqsstri 4014 |
. . . 4
⊢ 𝐼 ⊆ (ℤ ×
ℤ) |
11 | 10 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝐼 ⊆ (ℤ ×
ℤ)) |
12 | | opelxpi 5715 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
〈𝑋, 𝑌〉 ∈ (ℤ ×
ℤ)) |
13 | 1 | pzriprnglem2 21407 |
. . . . 5
⊢
(Base‘𝑅) =
(ℤ × ℤ) |
14 | 13 | eqcomi 2737 |
. . . 4
⊢ (ℤ
× ℤ) = (Base‘𝑅) |
15 | | pzriprng.g |
. . . 4
⊢ ∼ =
(𝑅 ~QG
𝐼) |
16 | | eqid 2728 |
. . . 4
⊢
(+g‘𝑅) = (+g‘𝑅) |
17 | 14, 15, 16 | eqglact 19133 |
. . 3
⊢ ((𝑅 ∈ Grp ∧ 𝐼 ⊆ (ℤ ×
ℤ) ∧ 〈𝑋,
𝑌〉 ∈ (ℤ
× ℤ)) → [〈𝑋, 𝑌〉] ∼ = ((𝑥 ∈ (ℤ ×
ℤ) ↦ (〈𝑋,
𝑌〉(+g‘𝑅)𝑥)) “ 𝐼)) |
18 | 4, 11, 12, 17 | mp3an2i 1463 |
. 2
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
[〈𝑋, 𝑌〉] ∼ = ((𝑥 ∈ (ℤ ×
ℤ) ↦ (〈𝑋,
𝑌〉(+g‘𝑅)𝑥)) “ 𝐼)) |
19 | 11 | mptimass 6076 |
. 2
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ((𝑥 ∈ (ℤ ×
ℤ) ↦ (〈𝑋,
𝑌〉(+g‘𝑅)𝑥)) “ 𝐼) = ran (𝑥 ∈ 𝐼 ↦ (〈𝑋, 𝑌〉(+g‘𝑅)𝑥))) |
20 | | eqid 2728 |
. . . . 5
⊢ (𝑥 ∈ 𝐼 ↦ (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)) = (𝑥 ∈ 𝐼 ↦ (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)) |
21 | 20 | rnmpt 5957 |
. . . 4
⊢ ran
(𝑥 ∈ 𝐼 ↦ (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)) = {𝑒 ∣ ∃𝑥 ∈ 𝐼 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)} |
22 | 21 | a1i 11 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ran
(𝑥 ∈ 𝐼 ↦ (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)) = {𝑒 ∣ ∃𝑥 ∈ 𝐼 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)}) |
23 | 5 | rexeqi 3321 |
. . . . . 6
⊢
(∃𝑥 ∈
𝐼 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)𝑥) ↔ ∃𝑥 ∈ (ℤ × {0})𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)) |
24 | | oveq2 7428 |
. . . . . . . 8
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (〈𝑋, 𝑌〉(+g‘𝑅)𝑥) = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉)) |
25 | 24 | eqeq2d 2739 |
. . . . . . 7
⊢ (𝑥 = 〈𝑎, 𝑏〉 → (𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)𝑥) ↔ 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉))) |
26 | 25 | rexxp 5845 |
. . . . . 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 2797 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑥 ∈ 𝐼 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)} = {𝑒 ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉)}) |
30 | | c0ex 11238 |
. . . . . . . 8
⊢ 0 ∈
V |
31 | | opeq2 4875 |
. . . . . . . . . 10
⊢ (𝑏 = 0 → 〈𝑎, 𝑏〉 = 〈𝑎, 0〉) |
32 | 31 | oveq2d 7436 |
. . . . . . . . 9
⊢ (𝑏 = 0 → (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉) = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 0〉)) |
33 | 32 | eqeq2d 2739 |
. . . . . . . 8
⊢ (𝑏 = 0 → (𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉) ↔ 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 0〉))) |
34 | 30, 33 | rexsn 4687 |
. . . . . . 7
⊢
(∃𝑏 ∈
{0}𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉) ↔ 𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 0〉)) |
35 | | zringbas 21378 |
. . . . . . . . 9
⊢ ℤ =
(Base‘ℤring) |
36 | | zringring 21374 |
. . . . . . . . . 10
⊢
ℤring ∈ Ring |
37 | 36 | a1i 11 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) →
ℤring ∈ Ring) |
38 | | simpll 766 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 𝑋 ∈
ℤ) |
39 | | simplr 768 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 𝑌 ∈
ℤ) |
40 | | simpr 484 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 𝑎 ∈
ℤ) |
41 | | 0zd 12600 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → 0 ∈
ℤ) |
42 | 38, 40 | zaddcld 12700 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑋 + 𝑎) ∈ ℤ) |
43 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝑌 ∈
ℤ) |
44 | | 0zd 12600 |
. . . . . . . . . . 11
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 0 ∈
ℤ) |
45 | 43, 44 | zaddcld 12700 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 + 0) ∈
ℤ) |
46 | 45 | adantr 480 |
. . . . . . . . 9
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑌 + 0) ∈
ℤ) |
47 | | zringplusg 21379 |
. . . . . . . . 9
⊢ + =
(+g‘ℤring) |
48 | 1, 35, 35, 37, 37, 38, 39, 40, 41, 42, 46, 47, 47, 16 | xpsadd 17555 |
. . . . . . . 8
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) →
(〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 0〉) = 〈(𝑋 + 𝑎), (𝑌 + 0)〉) |
49 | 48 | eqeq2d 2739 |
. . . . . . 7
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 0〉) ↔ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉)) |
50 | 34, 49 | bitrid 283 |
. . . . . 6
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) →
(∃𝑏 ∈ {0}𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉) ↔ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉)) |
51 | 50 | rexbidva 3173 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
∃𝑏 ∈ {0}𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉) ↔ ∃𝑎 ∈ ℤ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉)) |
52 | 51 | abbidv 2797 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉)} = {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉}) |
53 | | iunab 5054 |
. . . . . 6
⊢ ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} = {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} |
54 | 53 | eqcomi 2737 |
. . . . 5
⊢ {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} = ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} |
55 | 54 | a1i 11 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑎 ∈ ℤ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} = ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉}) |
56 | | zcn 12593 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℤ → 𝑌 ∈
ℂ) |
57 | 56 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝑌 ∈
ℂ) |
58 | 57 | addridd 11444 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑌 + 0) = 𝑌) |
59 | 58 | opeq2d 4881 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
〈(𝑋 + 𝑎), (𝑌 + 0)〉 = 〈(𝑋 + 𝑎), 𝑌〉) |
60 | 59 | eqeq2d 2739 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉 ↔ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉)) |
61 | 60 | abbidv 2797 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} = {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉}) |
62 | 61 | iuneq2d 5025 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} = ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉}) |
63 | | df-sn 4630 |
. . . . . . . . 9
⊢
{〈(𝑋 + 𝑎), 𝑌〉} = {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉} |
64 | 63 | eqcomi 2737 |
. . . . . . . 8
⊢ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉} = {〈(𝑋 + 𝑎), 𝑌〉} |
65 | 64 | a1i 11 |
. . . . . . 7
⊢ (𝑎 ∈ ℤ → {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉} = {〈(𝑋 + 𝑎), 𝑌〉}) |
66 | 65 | iuneq2i 5017 |
. . . . . 6
⊢ ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉} = ∪ 𝑎 ∈ ℤ {〈(𝑋 + 𝑎), 𝑌〉} |
67 | 66 | a1i 11 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), 𝑌〉} = ∪ 𝑎 ∈ ℤ {〈(𝑋 + 𝑎), 𝑌〉}) |
68 | | velsn 4645 |
. . . . . . . . . 10
⊢ (𝑦 ∈ {〈(𝑋 + 𝑎), 𝑌〉} ↔ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) |
69 | 68 | rexbii 3091 |
. . . . . . . . 9
⊢
(∃𝑎 ∈
ℤ 𝑦 ∈
{〈(𝑋 + 𝑎), 𝑌〉} ↔ ∃𝑎 ∈ ℤ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) |
70 | 42 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) ∧ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) → (𝑋 + 𝑎) ∈ ℤ) |
71 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑎 ∈
ℤ) ∧ 𝑦 =
〈(𝑋 + 𝑎), 𝑌〉) ∧ 𝑏 = (𝑋 + 𝑎)) → 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) |
72 | | opeq1 4874 |
. . . . . . . . . . . . . . 15
⊢ (𝑏 = (𝑋 + 𝑎) → 〈𝑏, 𝑌〉 = 〈(𝑋 + 𝑎), 𝑌〉) |
73 | 72 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑎 ∈
ℤ) ∧ 𝑦 =
〈(𝑋 + 𝑎), 𝑌〉) ∧ 𝑏 = (𝑋 + 𝑎)) → 〈𝑏, 𝑌〉 = 〈(𝑋 + 𝑎), 𝑌〉) |
74 | 71, 73 | eqeq12d 2744 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑎 ∈
ℤ) ∧ 𝑦 =
〈(𝑋 + 𝑎), 𝑌〉) ∧ 𝑏 = (𝑋 + 𝑎)) → (𝑦 = 〈𝑏, 𝑌〉 ↔ 〈(𝑋 + 𝑎), 𝑌〉 = 〈(𝑋 + 𝑎), 𝑌〉)) |
75 | | eqidd 2729 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) ∧ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) → 〈(𝑋 + 𝑎), 𝑌〉 = 〈(𝑋 + 𝑎), 𝑌〉) |
76 | 70, 74, 75 | rspcedvd 3611 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) ∧ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) → ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 𝑌〉) |
77 | 76 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑎 ∈ ℤ) → (𝑦 = 〈(𝑋 + 𝑎), 𝑌〉 → ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 𝑌〉)) |
78 | 77 | rexlimdva 3152 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 = 〈(𝑋 + 𝑎), 𝑌〉 → ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 𝑌〉)) |
79 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℤ) |
80 | | simpll 766 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈
ℤ) |
81 | 79, 80 | zsubcld 12701 |
. . . . . . . . . . . . . 14
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑏 − 𝑋) ∈ ℤ) |
82 | 81 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 𝑌〉) → (𝑏 − 𝑋) ∈ ℤ) |
83 | | simplr 768 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
〈𝑏, 𝑌〉) ∧ 𝑎 = (𝑏 − 𝑋)) → 𝑦 = 〈𝑏, 𝑌〉) |
84 | | oveq2 7428 |
. . . . . . . . . . . . . . . 16
⊢ (𝑎 = (𝑏 − 𝑋) → (𝑋 + 𝑎) = (𝑋 + (𝑏 − 𝑋))) |
85 | 84 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
〈𝑏, 𝑌〉) ∧ 𝑎 = (𝑏 − 𝑋)) → (𝑋 + 𝑎) = (𝑋 + (𝑏 − 𝑋))) |
86 | 85 | opeq1d 4880 |
. . . . . . . . . . . . . 14
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
〈𝑏, 𝑌〉) ∧ 𝑎 = (𝑏 − 𝑋)) → 〈(𝑋 + 𝑎), 𝑌〉 = 〈(𝑋 + (𝑏 − 𝑋)), 𝑌〉) |
87 | 83, 86 | eqeq12d 2744 |
. . . . . . . . . . . . 13
⊢
(((((𝑋 ∈
ℤ ∧ 𝑌 ∈
ℤ) ∧ 𝑏 ∈
ℤ) ∧ 𝑦 =
〈𝑏, 𝑌〉) ∧ 𝑎 = (𝑏 − 𝑋)) → (𝑦 = 〈(𝑋 + 𝑎), 𝑌〉 ↔ 〈𝑏, 𝑌〉 = 〈(𝑋 + (𝑏 − 𝑋)), 𝑌〉)) |
88 | | zcn 12593 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑋 ∈ ℤ → 𝑋 ∈
ℂ) |
89 | 88 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → 𝑋 ∈
ℂ) |
90 | 89 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑋 ∈
ℂ) |
91 | | zcn 12593 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
92 | 91 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 ∈
ℂ) |
93 | 90, 92 | pncan3d 11604 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑋 + (𝑏 − 𝑋)) = 𝑏) |
94 | 93 | eqcomd 2734 |
. . . . . . . . . . . . . . 15
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → 𝑏 = (𝑋 + (𝑏 − 𝑋))) |
95 | 94 | adantr 480 |
. . . . . . . . . . . . . 14
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 𝑌〉) → 𝑏 = (𝑋 + (𝑏 − 𝑋))) |
96 | 95 | opeq1d 4880 |
. . . . . . . . . . . . 13
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 𝑌〉) → 〈𝑏, 𝑌〉 = 〈(𝑋 + (𝑏 − 𝑋)), 𝑌〉) |
97 | 82, 87, 96 | rspcedvd 3611 |
. . . . . . . . . . . 12
⊢ ((((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) ∧ 𝑦 = 〈𝑏, 𝑌〉) → ∃𝑎 ∈ ℤ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉) |
98 | 97 | ex 412 |
. . . . . . . . . . 11
⊢ (((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) ∧ 𝑏 ∈ ℤ) → (𝑦 = 〈𝑏, 𝑌〉 → ∃𝑎 ∈ ℤ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉)) |
99 | 98 | rexlimdva 3152 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑏 ∈ ℤ
𝑦 = 〈𝑏, 𝑌〉 → ∃𝑎 ∈ ℤ 𝑦 = 〈(𝑋 + 𝑎), 𝑌〉)) |
100 | 78, 99 | impbid 211 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 = 〈(𝑋 + 𝑎), 𝑌〉 ↔ ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 𝑌〉)) |
101 | 69, 100 | bitrid 283 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 ∈ {〈(𝑋 + 𝑎), 𝑌〉} ↔ ∃𝑏 ∈ ℤ 𝑦 = 〈𝑏, 𝑌〉)) |
102 | | opeq2 4875 |
. . . . . . . . . . . . 13
⊢ (𝑐 = 𝑌 → 〈𝑏, 𝑐〉 = 〈𝑏, 𝑌〉) |
103 | 102 | eqeq2d 2739 |
. . . . . . . . . . . 12
⊢ (𝑐 = 𝑌 → (𝑦 = 〈𝑏, 𝑐〉 ↔ 𝑦 = 〈𝑏, 𝑌〉)) |
104 | 103 | rexsng 4679 |
. . . . . . . . . . 11
⊢ (𝑌 ∈ ℤ →
(∃𝑐 ∈ {𝑌}𝑦 = 〈𝑏, 𝑐〉 ↔ 𝑦 = 〈𝑏, 𝑌〉)) |
105 | 104 | adantl 481 |
. . . . . . . . . 10
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑐 ∈ {𝑌}𝑦 = 〈𝑏, 𝑐〉 ↔ 𝑦 = 〈𝑏, 𝑌〉)) |
106 | 105 | bicomd 222 |
. . . . . . . . 9
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑦 = 〈𝑏, 𝑌〉 ↔ ∃𝑐 ∈ {𝑌}𝑦 = 〈𝑏, 𝑐〉)) |
107 | 106 | rexbidv 3175 |
. . . . . . . 8
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑏 ∈ ℤ
𝑦 = 〈𝑏, 𝑌〉 ↔ ∃𝑏 ∈ ℤ ∃𝑐 ∈ {𝑌}𝑦 = 〈𝑏, 𝑐〉)) |
108 | 101, 107 | bitrd 279 |
. . . . . . 7
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
(∃𝑎 ∈ ℤ
𝑦 ∈ {〈(𝑋 + 𝑎), 𝑌〉} ↔ ∃𝑏 ∈ ℤ ∃𝑐 ∈ {𝑌}𝑦 = 〈𝑏, 𝑐〉)) |
109 | | eliun 5000 |
. . . . . . 7
⊢ (𝑦 ∈ ∪ 𝑎 ∈ ℤ {〈(𝑋 + 𝑎), 𝑌〉} ↔ ∃𝑎 ∈ ℤ 𝑦 ∈ {〈(𝑋 + 𝑎), 𝑌〉}) |
110 | | elxp2 5702 |
. . . . . . 7
⊢ (𝑦 ∈ (ℤ × {𝑌}) ↔ ∃𝑏 ∈ ℤ ∃𝑐 ∈ {𝑌}𝑦 = 〈𝑏, 𝑐〉) |
111 | 108, 109,
110 | 3bitr4g 314 |
. . . . . 6
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → (𝑦 ∈ ∪ 𝑎 ∈ ℤ {〈(𝑋 + 𝑎), 𝑌〉} ↔ 𝑦 ∈ (ℤ × {𝑌}))) |
112 | 111 | eqrdv 2726 |
. . . . 5
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {〈(𝑋 + 𝑎), 𝑌〉} = (ℤ × {𝑌})) |
113 | 62, 67, 112 | 3eqtrd 2772 |
. . . 4
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ∪ 𝑎 ∈ ℤ {𝑒 ∣ 𝑒 = 〈(𝑋 + 𝑎), (𝑌 + 0)〉} = (ℤ × {𝑌})) |
114 | 52, 55, 113 | 3eqtrd 2772 |
. . 3
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → {𝑒 ∣ ∃𝑎 ∈ ℤ ∃𝑏 ∈ {0}𝑒 = (〈𝑋, 𝑌〉(+g‘𝑅)〈𝑎, 𝑏〉)} = (ℤ × {𝑌})) |
115 | 22, 29, 114 | 3eqtrd 2772 |
. 2
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) → ran
(𝑥 ∈ 𝐼 ↦ (〈𝑋, 𝑌〉(+g‘𝑅)𝑥)) = (ℤ × {𝑌})) |
116 | 18, 19, 115 | 3eqtrd 2772 |
1
⊢ ((𝑋 ∈ ℤ ∧ 𝑌 ∈ ℤ) →
[〈𝑋, 𝑌〉] ∼ = (ℤ ×
{𝑌})) |