| Step | Hyp | Ref
| Expression |
| 1 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑧 = 𝑎 → (𝑧 = (2 · 𝑥) ↔ 𝑎 = (2 · 𝑥))) |
| 2 | 1 | rexbidv 3179 |
. . . . 5
⊢ (𝑧 = 𝑎 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑎 = (2 · 𝑥))) |
| 3 | | 2zrng.e |
. . . . 5
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} |
| 4 | 2, 3 | elrab2 3695 |
. . . 4
⊢ (𝑎 ∈ 𝐸 ↔ (𝑎 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑎 = (2 · 𝑥))) |
| 5 | | eqeq1 2741 |
. . . . . 6
⊢ (𝑧 = 𝑏 → (𝑧 = (2 · 𝑥) ↔ 𝑏 = (2 · 𝑥))) |
| 6 | 5 | rexbidv 3179 |
. . . . 5
⊢ (𝑧 = 𝑏 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) |
| 7 | 6, 3 | elrab2 3695 |
. . . 4
⊢ (𝑏 ∈ 𝐸 ↔ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) |
| 8 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
| 9 | 8 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → (𝑎 = (2 · 𝑥) ↔ 𝑎 = (2 · 𝑦))) |
| 10 | 9 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℤ 𝑎 = (2 ·
𝑥) ↔ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦)) |
| 11 | | zaddcl 12657 |
. . . . . . . . . . . . 13
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
| 12 | 11 | ancoms 458 |
. . . . . . . . . . . 12
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → (𝑎 + 𝑏) ∈ ℤ) |
| 13 | 12 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦))) → (𝑎 + 𝑏) ∈ ℤ) |
| 14 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦)) → 𝑦 ∈ ℤ) |
| 15 | | simpl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → 𝑥 ∈ ℤ) |
| 16 | | zaddcl 12657 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) → (𝑦 + 𝑥) ∈ ℤ) |
| 17 | 14, 15, 16 | syl2anr 597 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → (𝑦 + 𝑥) ∈ ℤ) |
| 18 | 17 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (𝑦 + 𝑥) ∈ ℤ) |
| 19 | | oveq2 7439 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑧 = (𝑦 + 𝑥) → (2 · 𝑧) = (2 · (𝑦 + 𝑥))) |
| 20 | 19 | eqeq2d 2748 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑧 = (𝑦 + 𝑥) → ((2 · (𝑦 + 𝑥)) = (2 · 𝑧) ↔ (2 · (𝑦 + 𝑥)) = (2 · (𝑦 + 𝑥)))) |
| 21 | 20 | adantl 481 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝑥 ∈
ℤ ∧ 𝑏 = (2
· 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) ∧ 𝑧 = (𝑦 + 𝑥)) → ((2 · (𝑦 + 𝑥)) = (2 · 𝑧) ↔ (2 · (𝑦 + 𝑥)) = (2 · (𝑦 + 𝑥)))) |
| 22 | | eqidd 2738 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (2 · (𝑦 + 𝑥)) = (2 · (𝑦 + 𝑥))) |
| 23 | 18, 21, 22 | rspcedvd 3624 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → ∃𝑧 ∈ ℤ (2 ·
(𝑦 + 𝑥)) = (2 · 𝑧)) |
| 24 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦)) → 𝑎 = (2 · 𝑦)) |
| 25 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → 𝑏 = (2 · 𝑥)) |
| 26 | 24, 25 | oveqan12rd 7451 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → (𝑎 + 𝑏) = ((2 · 𝑦) + (2 · 𝑥))) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (𝑎 + 𝑏) = ((2 · 𝑦) + (2 · 𝑥))) |
| 28 | | 2cnd 12344 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → 2 ∈ ℂ) |
| 29 | | zcn 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦)) → 𝑦 ∈ ℂ) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → 𝑦 ∈ ℂ) |
| 32 | | zcn 12618 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 33 | 32 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → 𝑥 ∈ ℂ) |
| 34 | 33 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → 𝑥 ∈ ℂ) |
| 35 | 28, 31, 34 | adddid 11285 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → (2 · (𝑦 + 𝑥)) = ((2 · 𝑦) + (2 · 𝑥))) |
| 36 | 35 | adantr 480 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (2 · (𝑦 + 𝑥)) = ((2 · 𝑦) + (2 · 𝑥))) |
| 37 | 27, 36 | eqtr4d 2780 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (𝑎 + 𝑏) = (2 · (𝑦 + 𝑥))) |
| 38 | 37 | eqeq1d 2739 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → ((𝑎 + 𝑏) = (2 · 𝑧) ↔ (2 · (𝑦 + 𝑥)) = (2 · 𝑧))) |
| 39 | 38 | rexbidv 3179 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → (∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧) ↔ ∃𝑧 ∈ ℤ (2 · (𝑦 + 𝑥)) = (2 · 𝑧))) |
| 40 | 23, 39 | mpbird 257 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) ∧ (𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ)) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)) |
| 41 | 40 | ex 412 |
. . . . . . . . . . . . . . . 16
⊢ (((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) ∧ (𝑦 ∈ ℤ ∧ 𝑎 = (2 · 𝑦))) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧))) |
| 42 | 41 | rexlimdvaa 3156 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 = (2 · 𝑥)) → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)))) |
| 43 | 42 | rexlimiva 3147 |
. . . . . . . . . . . . . 14
⊢
(∃𝑥 ∈
ℤ 𝑏 = (2 ·
𝑥) → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)))) |
| 44 | 43 | imp 406 |
. . . . . . . . . . . . 13
⊢
((∃𝑥 ∈
ℤ 𝑏 = (2 ·
𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦)) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧))) |
| 45 | | oveq2 7439 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 = 𝑧 → (2 · 𝑥) = (2 · 𝑧)) |
| 46 | 45 | eqeq2d 2748 |
. . . . . . . . . . . . . 14
⊢ (𝑥 = 𝑧 → ((𝑎 + 𝑏) = (2 · 𝑥) ↔ (𝑎 + 𝑏) = (2 · 𝑧))) |
| 47 | 46 | cbvrexvw 3238 |
. . . . . . . . . . . . 13
⊢
(∃𝑥 ∈
ℤ (𝑎 + 𝑏) = (2 · 𝑥) ↔ ∃𝑧 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑧)) |
| 48 | 44, 47 | imbitrrdi 252 |
. . . . . . . . . . . 12
⊢
((∃𝑥 ∈
ℤ 𝑏 = (2 ·
𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦)) → ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) → ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥))) |
| 49 | 48 | impcom 407 |
. . . . . . . . . . 11
⊢ (((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦))) → ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥)) |
| 50 | | eqeq1 2741 |
. . . . . . . . . . . . 13
⊢ (𝑧 = (𝑎 + 𝑏) → (𝑧 = (2 · 𝑥) ↔ (𝑎 + 𝑏) = (2 · 𝑥))) |
| 51 | 50 | rexbidv 3179 |
. . . . . . . . . . . 12
⊢ (𝑧 = (𝑎 + 𝑏) → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥))) |
| 52 | 51, 3 | elrab2 3695 |
. . . . . . . . . . 11
⊢ ((𝑎 + 𝑏) ∈ 𝐸 ↔ ((𝑎 + 𝑏) ∈ ℤ ∧ ∃𝑥 ∈ ℤ (𝑎 + 𝑏) = (2 · 𝑥))) |
| 53 | 13, 49, 52 | sylanbrc 583 |
. . . . . . . . . 10
⊢ (((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) ∧
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) ∧ ∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦))) → (𝑎 + 𝑏) ∈ 𝐸) |
| 54 | 53 | exp32 420 |
. . . . . . . . 9
⊢ ((𝑏 ∈ ℤ ∧ 𝑎 ∈ ℤ) →
(∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥) → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → (𝑎 + 𝑏) ∈ 𝐸))) |
| 55 | 54 | impancom 451 |
. . . . . . . 8
⊢ ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → (𝑎 ∈ ℤ → (∃𝑦 ∈ ℤ 𝑎 = (2 · 𝑦) → (𝑎 + 𝑏) ∈ 𝐸))) |
| 56 | 55 | com13 88 |
. . . . . . 7
⊢
(∃𝑦 ∈
ℤ 𝑎 = (2 ·
𝑦) → (𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → (𝑎 + 𝑏) ∈ 𝐸))) |
| 57 | 10, 56 | sylbi 217 |
. . . . . 6
⊢
(∃𝑥 ∈
ℤ 𝑎 = (2 ·
𝑥) → (𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → (𝑎 + 𝑏) ∈ 𝐸))) |
| 58 | 57 | impcom 407 |
. . . . 5
⊢ ((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) → ((𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥)) → (𝑎 + 𝑏) ∈ 𝐸)) |
| 59 | 58 | imp 406 |
. . . 4
⊢ (((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑎 + 𝑏) ∈ 𝐸) |
| 60 | 4, 7, 59 | syl2anb 598 |
. . 3
⊢ ((𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸) → (𝑎 + 𝑏) ∈ 𝐸) |
| 61 | 60 | rgen2 3199 |
. 2
⊢
∀𝑎 ∈
𝐸 ∀𝑏 ∈ 𝐸 (𝑎 + 𝑏) ∈ 𝐸 |
| 62 | | 0z 12624 |
. . . . 5
⊢ 0 ∈
ℤ |
| 63 | | 2cn 12341 |
. . . . . 6
⊢ 2 ∈
ℂ |
| 64 | | 0zd 12625 |
. . . . . . 7
⊢ (2 ∈
ℂ → 0 ∈ ℤ) |
| 65 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 0 → (2 · 𝑥) = (2 ·
0)) |
| 66 | 65 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑥 = 0 → (0 = (2 ·
𝑥) ↔ 0 = (2 ·
0))) |
| 67 | 66 | adantl 481 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ 𝑥 = 0)
→ (0 = (2 · 𝑥)
↔ 0 = (2 · 0))) |
| 68 | | mul01 11440 |
. . . . . . . 8
⊢ (2 ∈
ℂ → (2 · 0) = 0) |
| 69 | 68 | eqcomd 2743 |
. . . . . . 7
⊢ (2 ∈
ℂ → 0 = (2 · 0)) |
| 70 | 64, 67, 69 | rspcedvd 3624 |
. . . . . 6
⊢ (2 ∈
ℂ → ∃𝑥
∈ ℤ 0 = (2 · 𝑥)) |
| 71 | 63, 70 | ax-mp 5 |
. . . . 5
⊢
∃𝑥 ∈
ℤ 0 = (2 · 𝑥) |
| 72 | | eqeq1 2741 |
. . . . . . 7
⊢ (𝑧 = 0 → (𝑧 = (2 · 𝑥) ↔ 0 = (2 · 𝑥))) |
| 73 | 72 | rexbidv 3179 |
. . . . . 6
⊢ (𝑧 = 0 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 0 = (2 ·
𝑥))) |
| 74 | 73 | elrab 3692 |
. . . . 5
⊢ (0 ∈
{𝑧 ∈ ℤ ∣
∃𝑥 ∈ ℤ
𝑧 = (2 · 𝑥)} ↔ (0 ∈ ℤ
∧ ∃𝑥 ∈
ℤ 0 = (2 · 𝑥))) |
| 75 | 62, 71, 74 | mpbir2an 711 |
. . . 4
⊢ 0 ∈
{𝑧 ∈ ℤ ∣
∃𝑥 ∈ ℤ
𝑧 = (2 · 𝑥)} |
| 76 | 75, 3 | eleqtrri 2840 |
. . 3
⊢ 0 ∈
𝐸 |
| 77 | | 2zrngbas.r |
. . . . 5
⊢ 𝑅 = (ℂfld
↾s 𝐸) |
| 78 | 3, 77 | 2zrngbas 48158 |
. . . 4
⊢ 𝐸 = (Base‘𝑅) |
| 79 | 3, 77 | 2zrngadd 48159 |
. . . 4
⊢ + =
(+g‘𝑅) |
| 80 | 78, 79 | ismgmn0 18655 |
. . 3
⊢ (0 ∈
𝐸 → (𝑅 ∈ Mgm ↔ ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 + 𝑏) ∈ 𝐸)) |
| 81 | 76, 80 | ax-mp 5 |
. 2
⊢ (𝑅 ∈ Mgm ↔ ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 + 𝑏) ∈ 𝐸) |
| 82 | 61, 81 | mpbir 231 |
1
⊢ 𝑅 ∈ Mgm |