| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | 2zrng.e | . . 3
⊢ 𝐸 = {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} | 
| 2 |  | 2zrngbas.r | . . 3
⊢ 𝑅 = (ℂfld
↾s 𝐸) | 
| 3 | 1, 2 | 2zrngamnd 48168 | . 2
⊢ 𝑅 ∈ Mnd | 
| 4 |  | eqeq1 2740 | . . . . . . 7
⊢ (𝑧 = 𝑦 → (𝑧 = (2 · 𝑥) ↔ 𝑦 = (2 · 𝑥))) | 
| 5 | 4 | rexbidv 3178 | . . . . . 6
⊢ (𝑧 = 𝑦 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ 𝑦 = (2 · 𝑥))) | 
| 6 | 5, 1 | elrab2 3694 | . . . . 5
⊢ (𝑦 ∈ 𝐸 ↔ (𝑦 ∈ ℤ ∧ ∃𝑥 ∈ ℤ 𝑦 = (2 · 𝑥))) | 
| 7 |  | znegcl 12654 | . . . . . . 7
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) | 
| 8 | 7 | adantr 480 | . . . . . 6
⊢ ((𝑦 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑦 = (2 · 𝑥)) → -𝑦 ∈ ℤ) | 
| 9 |  | nfv 1913 | . . . . . . . 8
⊢
Ⅎ𝑥 𝑦 ∈ ℤ | 
| 10 |  | nfre1 3284 | . . . . . . . 8
⊢
Ⅎ𝑥∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥) | 
| 11 |  | znegcl 12654 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → -𝑥 ∈
ℤ) | 
| 12 | 11 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) → -𝑥 ∈
ℤ) | 
| 13 | 12 | adantr 480 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑦 = (2 · 𝑥)) → -𝑥 ∈ ℤ) | 
| 14 |  | oveq2 7440 | . . . . . . . . . . . . 13
⊢ (𝑧 = -𝑥 → (2 · 𝑧) = (2 · -𝑥)) | 
| 15 | 14 | eqeq2d 2747 | . . . . . . . . . . . 12
⊢ (𝑧 = -𝑥 → (-𝑦 = (2 · 𝑧) ↔ -𝑦 = (2 · -𝑥))) | 
| 16 | 15 | adantl 481 | . . . . . . . . . . 11
⊢ ((((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑦 = (2 · 𝑥)) ∧ 𝑧 = -𝑥) → (-𝑦 = (2 · 𝑧) ↔ -𝑦 = (2 · -𝑥))) | 
| 17 |  | negeq 11501 | . . . . . . . . . . . 12
⊢ (𝑦 = (2 · 𝑥) → -𝑦 = -(2 · 𝑥)) | 
| 18 |  | 2cnd 12345 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 2 ∈
ℂ) | 
| 19 |  | zcn 12620 | . . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) | 
| 20 | 18, 19 | mulneg2d 11718 | . . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → (2
· -𝑥) = -(2 ·
𝑥)) | 
| 21 | 20 | eqcomd 2742 | . . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → -(2
· 𝑥) = (2 ·
-𝑥)) | 
| 22 | 21 | adantl 481 | . . . . . . . . . . . 12
⊢ ((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) → -(2
· 𝑥) = (2 ·
-𝑥)) | 
| 23 | 17, 22 | sylan9eqr 2798 | . . . . . . . . . . 11
⊢ (((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑦 = (2 · 𝑥)) → -𝑦 = (2 · -𝑥)) | 
| 24 | 13, 16, 23 | rspcedvd 3623 | . . . . . . . . . 10
⊢ (((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑦 = (2 · 𝑥)) → ∃𝑧 ∈ ℤ -𝑦 = (2 · 𝑧)) | 
| 25 |  | oveq2 7440 | . . . . . . . . . . . 12
⊢ (𝑥 = 𝑧 → (2 · 𝑥) = (2 · 𝑧)) | 
| 26 | 25 | eqeq2d 2747 | . . . . . . . . . . 11
⊢ (𝑥 = 𝑧 → (-𝑦 = (2 · 𝑥) ↔ -𝑦 = (2 · 𝑧))) | 
| 27 | 26 | cbvrexvw 3237 | . . . . . . . . . 10
⊢
(∃𝑥 ∈
ℤ -𝑦 = (2 ·
𝑥) ↔ ∃𝑧 ∈ ℤ -𝑦 = (2 · 𝑧)) | 
| 28 | 24, 27 | sylibr 234 | . . . . . . . . 9
⊢ (((𝑦 ∈ ℤ ∧ 𝑥 ∈ ℤ) ∧ 𝑦 = (2 · 𝑥)) → ∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥)) | 
| 29 | 28 | exp31 419 | . . . . . . . 8
⊢ (𝑦 ∈ ℤ → (𝑥 ∈ ℤ → (𝑦 = (2 · 𝑥) → ∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥)))) | 
| 30 | 9, 10, 29 | rexlimd 3265 | . . . . . . 7
⊢ (𝑦 ∈ ℤ →
(∃𝑥 ∈ ℤ
𝑦 = (2 · 𝑥) → ∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥))) | 
| 31 | 30 | imp 406 | . . . . . 6
⊢ ((𝑦 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑦 = (2 · 𝑥)) → ∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥)) | 
| 32 |  | eqeq1 2740 | . . . . . . . 8
⊢ (𝑧 = -𝑦 → (𝑧 = (2 · 𝑥) ↔ -𝑦 = (2 · 𝑥))) | 
| 33 | 32 | rexbidv 3178 | . . . . . . 7
⊢ (𝑧 = -𝑦 → (∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥) ↔ ∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥))) | 
| 34 | 33, 1 | elrab2 3694 | . . . . . 6
⊢ (-𝑦 ∈ 𝐸 ↔ (-𝑦 ∈ ℤ ∧ ∃𝑥 ∈ ℤ -𝑦 = (2 · 𝑥))) | 
| 35 | 8, 31, 34 | sylanbrc 583 | . . . . 5
⊢ ((𝑦 ∈ ℤ ∧
∃𝑥 ∈ ℤ
𝑦 = (2 · 𝑥)) → -𝑦 ∈ 𝐸) | 
| 36 | 6, 35 | sylbi 217 | . . . 4
⊢ (𝑦 ∈ 𝐸 → -𝑦 ∈ 𝐸) | 
| 37 |  | oveq1 7439 | . . . . . 6
⊢ (𝑧 = -𝑦 → (𝑧 + 𝑦) = (-𝑦 + 𝑦)) | 
| 38 | 37 | eqeq1d 2738 | . . . . 5
⊢ (𝑧 = -𝑦 → ((𝑧 + 𝑦) = 0 ↔ (-𝑦 + 𝑦) = 0)) | 
| 39 | 38 | adantl 481 | . . . 4
⊢ ((𝑦 ∈ 𝐸 ∧ 𝑧 = -𝑦) → ((𝑧 + 𝑦) = 0 ↔ (-𝑦 + 𝑦) = 0)) | 
| 40 |  | elrabi 3686 | . . . . . . . . 9
⊢ (𝑦 ∈ {𝑧 ∈ ℤ ∣ ∃𝑥 ∈ ℤ 𝑧 = (2 · 𝑥)} → 𝑦 ∈ ℤ) | 
| 41 | 40, 1 | eleq2s 2858 | . . . . . . . 8
⊢ (𝑦 ∈ 𝐸 → 𝑦 ∈ ℤ) | 
| 42 | 41 | zcnd 12725 | . . . . . . 7
⊢ (𝑦 ∈ 𝐸 → 𝑦 ∈ ℂ) | 
| 43 | 42 | negcld 11608 | . . . . . 6
⊢ (𝑦 ∈ 𝐸 → -𝑦 ∈ ℂ) | 
| 44 | 43, 42 | addcomd 11464 | . . . . 5
⊢ (𝑦 ∈ 𝐸 → (-𝑦 + 𝑦) = (𝑦 + -𝑦)) | 
| 45 | 42 | negidd 11611 | . . . . 5
⊢ (𝑦 ∈ 𝐸 → (𝑦 + -𝑦) = 0) | 
| 46 | 44, 45 | eqtrd 2776 | . . . 4
⊢ (𝑦 ∈ 𝐸 → (-𝑦 + 𝑦) = 0) | 
| 47 | 36, 39, 46 | rspcedvd 3623 | . . 3
⊢ (𝑦 ∈ 𝐸 → ∃𝑧 ∈ 𝐸 (𝑧 + 𝑦) = 0) | 
| 48 | 47 | rgen 3062 | . 2
⊢
∀𝑦 ∈
𝐸 ∃𝑧 ∈ 𝐸 (𝑧 + 𝑦) = 0 | 
| 49 | 1, 2 | 2zrngbas 48163 | . . 3
⊢ 𝐸 = (Base‘𝑅) | 
| 50 | 1, 2 | 2zrngadd 48164 | . . 3
⊢  + =
(+g‘𝑅) | 
| 51 | 1, 2 | 2zrng0 48165 | . . 3
⊢ 0 =
(0g‘𝑅) | 
| 52 | 49, 50, 51 | isgrp 18958 | . 2
⊢ (𝑅 ∈ Grp ↔ (𝑅 ∈ Mnd ∧ ∀𝑦 ∈ 𝐸 ∃𝑧 ∈ 𝐸 (𝑧 + 𝑦) = 0)) | 
| 53 | 3, 48, 52 | mpbir2an 711 | 1
⊢ 𝑅 ∈ Grp |