Step | Hyp | Ref
| Expression |
1 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑧 = 𝑎 → (𝑧 = (2 · 𝑥) ↔ 𝑎 = (2 · 𝑥))) |
2 | 1 | rexbidv 3208 |
. . . . 5
⊢ (𝑧 = 𝑎 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑎 = (2 · 𝑥))) |
3 | | 2zrng.e |
. . . . 5
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} |
4 | 2, 3 | elrab2 3596 |
. . . 4
⊢ (𝑎 ∈ 𝐸 ↔ (𝑎 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑎 = (2 · 𝑥))) |
5 | | eqeq1 2743 |
. . . . . 6
⊢ (𝑧 = 𝑏 → (𝑧 = (2 · 𝑥) ↔ 𝑏 = (2 · 𝑥))) |
6 | 5 | rexbidv 3208 |
. . . . 5
⊢ (𝑧 = 𝑏 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) |
7 | 6, 3 | elrab2 3596 |
. . . 4
⊢ (𝑏 ∈ 𝐸 ↔ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) |
8 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
9 | 8 | eqeq2d 2750 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑎 = (2 · 𝑥) ↔ 𝑎 = (2 · 𝑦))) |
10 | 9 | cbvrexvw 3351 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℤ 𝑎 = (2 ·
𝑥) ↔ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦)) |
11 | | zaddcl 12116 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
12 | 11 | ancoms 462 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
13 | 12 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦))) → (𝑎 + 𝑏) ∈ ℤ) |
14 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦)) → 𝑦 ∈ ℤ) |
15 | | simpl 486 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → 𝑥 ∈ ℤ) |
16 | | zaddcl 12116 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑦 + 𝑥) ∈ ℤ) |
17 | 14, 15, 16 | syl2anr 600 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → (𝑦 + 𝑥) ∈ ℤ) |
18 | 17 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (𝑦 + 𝑥) ∈ ℤ) |
19 | | oveq2 7191 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝑦 + 𝑥) → (2 · 𝑧) = (2 · (𝑦 + 𝑥))) |
20 | 19 | eqeq2d 2750 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑦 + 𝑥) → ((2 · (𝑦 + 𝑥)) = (2 · 𝑧) ↔ (2 · (𝑦 + 𝑥)) = (2 · (𝑦 + 𝑥)))) |
21 | 20 | adantl 485 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℤ ∧ 𝑏 = (2
· 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) ∧ 𝑧 = (𝑦 + 𝑥)) → ((2 · (𝑦 + 𝑥)) = (2 · 𝑧) ↔ (2 · (𝑦 + 𝑥)) = (2 · (𝑦 + 𝑥)))) |
22 | | eqidd 2740 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (2 · (𝑦 + 𝑥)) = (2 · (𝑦 + 𝑥))) |
23 | 18, 21, 22 | rspcedvd 3532 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → ∃𝑧 ∈ ℤ (2 ·
(𝑦 + 𝑥)) = (2 · 𝑧)) |
24 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦)) → 𝑎 = (2 · 𝑦)) |
25 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → 𝑏 = (2 · 𝑥)) |
26 | 24, 25 | oveqan12rd 7203 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → (𝑎 + 𝑏) = ((2 · 𝑦) + (2 · 𝑥))) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (𝑎 + 𝑏) = ((2 · 𝑦) + (2 · 𝑥))) |
28 | | 2cnd 11807 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → 2 ∈ ℂ) |
29 | | zcn 12080 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
30 | 29 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦)) → 𝑦 ∈ ℂ) |
31 | 30 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → 𝑦 ∈ ℂ) |
32 | | zcn 12080 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
33 | 32 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → 𝑥 ∈ ℂ) |
34 | 33 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → 𝑥 ∈ ℂ) |
35 | 28, 31, 34 | adddid 10756 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → (2 · (𝑦 + 𝑥)) = ((2 · 𝑦) + (2 · 𝑥))) |
36 | 35 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (2 · (𝑦 + 𝑥)) = ((2 · 𝑦) + (2 · 𝑥))) |
37 | 27, 36 | eqtr4d 2777 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (𝑎 + 𝑏) = (2 · (𝑦 + 𝑥))) |
38 | 37 | eqeq1d 2741 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → ((𝑎 + 𝑏) = (2 · 𝑧) ↔ (2 · (𝑦 + 𝑥)) = (2 · 𝑧))) |
39 | 38 | rexbidv 3208 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧) ↔ ∃𝑧 ∈ ℤ (2 · (𝑦 + 𝑥)) = (2 · 𝑧))) |
40 | 23, 39 | mpbird 260 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)) |
41 | 40 | ex 416 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧))) |
42 | 41 | rexlimdvaa 3196 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)))) |
43 | 42 | rexlimiva 3192 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℤ 𝑏 = (2 ·
𝑥) → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)))) |
44 | 43 | imp 410 |
. . . . . . . . . . . . 13
⊢
((∃𝑥 ∈
ℤ 𝑏 = (2 ·
𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦)) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧))) |
45 | | oveq2 7191 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (2 · 𝑥) = (2 · 𝑧)) |
46 | 45 | eqeq2d 2750 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((𝑎 + 𝑏) = (2 · 𝑥) ↔ (𝑎 + 𝑏) = (2 · 𝑧))) |
47 | 46 | cbvrexvw 3351 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ (𝑎 + 𝑏) = (2 · 𝑥) ↔ ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)) |
48 | 44, 47 | syl6ibr 255 |
. . . . . . . . . . . 12
⊢
((∃𝑥 ∈
ℤ 𝑏 = (2 ·
𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦)) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥))) |
49 | 48 | impcom 411 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦))) → ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥)) |
50 | | eqeq1 2743 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑎 + 𝑏) → (𝑧 = (2 · 𝑥) ↔ (𝑎 + 𝑏) = (2 · 𝑥))) |
51 | 50 | rexbidv 3208 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑎 + 𝑏) → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥))) |
52 | 51, 3 | elrab2 3596 |
. . . . . . . . . . 11
⊢ ((𝑎 + 𝑏) ∈ 𝐸 ↔ ((𝑎 + 𝑏) ∈ ℤ ∧ ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥))) |
53 | 13, 49, 52 | sylanbrc 586 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦))) → (𝑎 + 𝑏) ∈ 𝐸) |
54 | 53 | exp32 424 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) →
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → (𝑎 + 𝑏) ∈ 𝐸))) |
55 | 54 | impancom 455 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → (𝑎 ∈ ℤ → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → (𝑎 + 𝑏) ∈ 𝐸))) |
56 | 55 | com13 88 |
. . . . . . 7
⊢
(∃𝑦 ∈
ℤ 𝑎 = (2 ·
𝑦) → (𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → (𝑎 + 𝑏) ∈ 𝐸))) |
57 | 10, 56 | sylbi 220 |
. . . . . 6
⊢
(∃𝑥 ∈
ℤ 𝑎 = (2 ·
𝑥) → (𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → (𝑎 + 𝑏) ∈ 𝐸))) |
58 | 57 | impcom 411 |
. . . . 5
⊢ ((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) → ((𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥)) → (𝑎 + 𝑏) ∈ 𝐸)) |
59 | 58 | imp 410 |
. . . 4
⊢ (((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑎 + 𝑏) ∈ 𝐸) |
60 | 4, 7, 59 | syl2anb 601 |
. . 3
⊢ ((𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸) → (𝑎 + 𝑏) ∈ 𝐸) |
61 | 60 | rgen2 3116 |
. 2
⊢
∀𝑎 ∈
𝐸 ∀𝑏 ∈ 𝐸 (𝑎 + 𝑏) ∈ 𝐸 |
62 | | 0z 12086 |
. . . . 5
⊢ 0 ∈
ℤ |
63 | | 2cn 11804 |
. . . . . 6
⊢ 2 ∈
ℂ |
64 | | 0zd 12087 |
. . . . . . 7
⊢ (2 ∈
ℂ → 0 ∈ ℤ) |
65 | | oveq2 7191 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (2 · 𝑥) = (2 ·
0)) |
66 | 65 | eqeq2d 2750 |
. . . . . . . 8
⊢ (𝑥 = 0 → (0 = (2 ·
𝑥) ↔ 0 = (2 ·
0))) |
67 | 66 | adantl 485 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ 𝑥 = 0)
→ (0 = (2 · 𝑥)
↔ 0 = (2 · 0))) |
68 | | mul01 10910 |
. . . . . . . 8
⊢ (2 ∈
ℂ → (2 · 0) = 0) |
69 | 68 | eqcomd 2745 |
. . . . . . 7
⊢ (2 ∈
ℂ → 0 = (2 · 0)) |
70 | 64, 67, 69 | rspcedvd 3532 |
. . . . . 6
⊢ (2 ∈
ℂ → ∃𝑥
∈ ℤ 0 = (2 · 𝑥)) |
71 | 63, 70 | ax-mp 5 |
. . . . 5
⊢
∃𝑥 ∈
ℤ 0 = (2 · 𝑥) |
72 | | eqeq1 2743 |
. . . . . . 7
⊢ (𝑧 = 0 → (𝑧 = (2 · 𝑥) ↔ 0 = (2 · 𝑥))) |
73 | 72 | rexbidv 3208 |
. . . . . 6
⊢ (𝑧 = 0 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 0 = (2 ·
𝑥))) |
74 | 73 | elrab 3593 |
. . . . 5
⊢ (0 ∈
{𝑧 ∈ ℤ ∣
∃𝑥 ∈ ℤ
𝑧 = (2 · 𝑥)} ↔ (0 ∈ ℤ
∧ ∃𝑥 ∈
ℤ 0 = (2 · 𝑥))) |
75 | 62, 71, 74 | mpbir2an 711 |
. . . 4
⊢ 0 ∈
{𝑧 ∈ ℤ ∣
∃𝑥 ∈ ℤ
𝑧 = (2 · 𝑥)} |
76 | 75, 3 | eleqtrri 2833 |
. . 3
⊢ 0 ∈
𝐸 |
77 | | 2zrngbas.r |
. . . . 5
⊢ 𝑅 = (ℂfld
↾s 𝐸) |
78 | 3, 77 | 2zrngbas 45076 |
. . . 4
⊢ 𝐸 = (Base‘𝑅) |
79 | 3, 77 | 2zrngadd 45077 |
. . . 4
⊢ + =
(+g‘𝑅) |
80 | 78, 79 | ismgmn0 17983 |
. . 3
⊢ (0 ∈
𝐸 → (𝑅 ∈ Mgm ↔ ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 + 𝑏) ∈ 𝐸)) |
81 | 76, 80 | ax-mp 5 |
. 2
⊢ (𝑅 ∈ Mgm ↔ ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 + 𝑏) ∈ 𝐸) |
82 | 61, 81 | mpbir 234 |
1
⊢ 𝑅 ∈ Mgm |