| 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 | | zmulcl 12666 |
. . . . . 6
⊢ ((𝑎 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑎 · 𝑏) ∈ ℤ) |
| 9 | 8 | ad2ant2r 747 |
. . . . 5
⊢ (((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑎 · 𝑏) ∈ ℤ) |
| 10 | | nfv 1914 |
. . . . . . . . 9
⊢
Ⅎ𝑥 𝑎 ∈ ℤ |
| 11 | | nfv 1914 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥 𝑏 ∈ ℤ |
| 12 | | nfre1 3285 |
. . . . . . . . . . 11
⊢
Ⅎ𝑥∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥) |
| 13 | 11, 12 | nfan 1899 |
. . . . . . . . . 10
⊢
Ⅎ𝑥(𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) |
| 14 | | nfv 1914 |
. . . . . . . . . 10
⊢
Ⅎ𝑥∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦) |
| 15 | 13, 14 | nfim 1896 |
. . . . . . . . 9
⊢
Ⅎ𝑥((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦)) |
| 16 | 10, 15 | nfim 1896 |
. . . . . . . 8
⊢
Ⅎ𝑥(𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦))) |
| 17 | | simpll 767 |
. . . . . . . . . . 11
⊢ (((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) → 𝑥 ∈ ℤ) |
| 18 | | simpl 482 |
. . . . . . . . . . 11
⊢ ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → 𝑏 ∈ ℤ) |
| 19 | | zmulcl 12666 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℤ ∧ 𝑏 ∈ ℤ) → (𝑥 · 𝑏) ∈ ℤ) |
| 20 | 17, 18, 19 | syl2an 596 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑥 · 𝑏) ∈ ℤ) |
| 21 | | oveq2 7439 |
. . . . . . . . . . . 12
⊢ (𝑦 = (𝑥 · 𝑏) → (2 · 𝑦) = (2 · (𝑥 · 𝑏))) |
| 22 | 21 | eqeq2d 2748 |
. . . . . . . . . . 11
⊢ (𝑦 = (𝑥 · 𝑏) → ((𝑎 · 𝑏) = (2 · 𝑦) ↔ (𝑎 · 𝑏) = (2 · (𝑥 · 𝑏)))) |
| 23 | 22 | adantl 481 |
. . . . . . . . . 10
⊢
(((((𝑥 ∈
ℤ ∧ 𝑎 = (2
· 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥))) ∧ 𝑦 = (𝑥 · 𝑏)) → ((𝑎 · 𝑏) = (2 · 𝑦) ↔ (𝑎 · 𝑏) = (2 · (𝑥 · 𝑏)))) |
| 24 | | oveq1 7438 |
. . . . . . . . . . . 12
⊢ (𝑎 = (2 · 𝑥) → (𝑎 · 𝑏) = ((2 · 𝑥) · 𝑏)) |
| 25 | 24 | ad3antlr 731 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑎 · 𝑏) = ((2 · 𝑥) · 𝑏)) |
| 26 | | 2cnd 12344 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → 2 ∈
ℂ) |
| 27 | | zcn 12618 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
| 28 | 27 | ad3antrrr 730 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → 𝑥 ∈ ℂ) |
| 29 | | zcn 12618 |
. . . . . . . . . . . . . 14
⊢ (𝑏 ∈ ℤ → 𝑏 ∈
ℂ) |
| 30 | 29 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → 𝑏 ∈ ℂ) |
| 31 | 30 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → 𝑏 ∈ ℂ) |
| 32 | 26, 28, 31 | mulassd 11284 |
. . . . . . . . . . 11
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → ((2 · 𝑥) · 𝑏) = (2 · (𝑥 · 𝑏))) |
| 33 | 25, 32 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑎 · 𝑏) = (2 · (𝑥 · 𝑏))) |
| 34 | 20, 23, 33 | rspcedvd 3624 |
. . . . . . . . 9
⊢ ((((𝑥 ∈ ℤ ∧ 𝑎 = (2 · 𝑥)) ∧ 𝑎 ∈ ℤ) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦)) |
| 35 | 34 | exp41 434 |
. . . . . . . 8
⊢ (𝑥 ∈ ℤ → (𝑎 = (2 · 𝑥) → (𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥)) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦))))) |
| 36 | 16, 35 | rexlimi 3259 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℤ 𝑎 = (2 ·
𝑥) → (𝑎 ∈ ℤ → ((𝑏 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑏 = (2 · 𝑥)) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦)))) |
| 37 | 36 | impcom 407 |
. . . . . 6
⊢ ((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) → ((𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥)) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦))) |
| 38 | 37 | imp 406 |
. . . . 5
⊢ (((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦)) |
| 39 | | eqeq1 2741 |
. . . . . . . 8
⊢ (𝑧 = (𝑎 · 𝑏) → (𝑧 = (2 · 𝑥) ↔ (𝑎 · 𝑏) = (2 · 𝑥))) |
| 40 | 39 | rexbidv 3179 |
. . . . . . 7
⊢ (𝑧 = (𝑎 · 𝑏) → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑥))) |
| 41 | 40, 3 | elrab2 3695 |
. . . . . 6
⊢ ((𝑎 · 𝑏) ∈ 𝐸 ↔ ((𝑎 · 𝑏) ∈ ℤ ∧ ∃𝑥 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑥))) |
| 42 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑥 = 𝑦 → (2 · 𝑥) = (2 · 𝑦)) |
| 43 | 42 | eqeq2d 2748 |
. . . . . . . 8
⊢ (𝑥 = 𝑦 → ((𝑎 · 𝑏) = (2 · 𝑥) ↔ (𝑎 · 𝑏) = (2 · 𝑦))) |
| 44 | 43 | cbvrexvw 3238 |
. . . . . . 7
⊢
(∃𝑥 ∈
ℤ (𝑎 · 𝑏) = (2 · 𝑥) ↔ ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦)) |
| 45 | 44 | anbi2i 623 |
. . . . . 6
⊢ (((𝑎 · 𝑏) ∈ ℤ ∧ ∃𝑥 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑥)) ↔ ((𝑎 · 𝑏) ∈ ℤ ∧ ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦))) |
| 46 | 41, 45 | bitri 275 |
. . . . 5
⊢ ((𝑎 · 𝑏) ∈ 𝐸 ↔ ((𝑎 · 𝑏) ∈ ℤ ∧ ∃𝑦 ∈ ℤ (𝑎 · 𝑏) = (2 · 𝑦))) |
| 47 | 9, 38, 46 | sylanbrc 583 |
. . . 4
⊢ (((𝑎 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑎 = (2 · 𝑥)) ∧ (𝑏 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑏 = (2 · 𝑥))) → (𝑎 · 𝑏) ∈ 𝐸) |
| 48 | 4, 7, 47 | syl2anb 598 |
. . 3
⊢ ((𝑎 ∈ 𝐸 ∧ 𝑏 ∈ 𝐸) → (𝑎 · 𝑏) ∈ 𝐸) |
| 49 | 48 | rgen2 3199 |
. 2
⊢
∀𝑎 ∈
𝐸 ∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ∈ 𝐸 |
| 50 | 3 | 0even 48153 |
. . 3
⊢ 0 ∈
𝐸 |
| 51 | | 2zrngmmgm.1 |
. . . . 5
⊢ 𝑀 = (mulGrp‘𝑅) |
| 52 | | 2zrngbas.r |
. . . . . 6
⊢ 𝑅 = (ℂfld
↾s 𝐸) |
| 53 | 3, 52 | 2zrngbas 48158 |
. . . . 5
⊢ 𝐸 = (Base‘𝑅) |
| 54 | 51, 53 | mgpbas 20142 |
. . . 4
⊢ 𝐸 = (Base‘𝑀) |
| 55 | 3, 52 | 2zrngmul 48167 |
. . . . 5
⊢ ·
= (.r‘𝑅) |
| 56 | 51, 55 | mgpplusg 20141 |
. . . 4
⊢ ·
= (+g‘𝑀) |
| 57 | 54, 56 | ismgmn0 18655 |
. . 3
⊢ (0 ∈
𝐸 → (𝑀 ∈ Mgm ↔ ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ∈ 𝐸)) |
| 58 | 50, 57 | ax-mp 5 |
. 2
⊢ (𝑀 ∈ Mgm ↔ ∀𝑎 ∈ 𝐸 ∀𝑏 ∈ 𝐸 (𝑎 · 𝑏) ∈ 𝐸) |
| 59 | 49, 58 | mpbir 231 |
1
⊢ 𝑀 ∈ Mgm |