Metamath Proof Explorer

Theorem 2zrngagrp

Description: R is an (additive) group. (Contributed by AV, 6-Jan-2020)

Ref Expression
Hypotheses 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
Assertion 2zrngagrp ⊢ R ∈ Grp

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 1 2 2zrngamnd ⊢ R ∈ Mnd
4 eqeq1 ⊢ z = y → z = 2 ⁢ x ↔ y = 2 ⁢ x
5 4 rexbidv ⊢ z = y → ∃ x ∈ ℤ z = 2 ⁢ x ↔ ∃ x ∈ ℤ y = 2 ⁢ x
6 5 1 elrab2 ⊢ y ∈ E ↔ y ∈ ℤ ∧ ∃ x ∈ ℤ y = 2 ⁢ x
7 znegcl ⊢ y ∈ ℤ → − y ∈ ℤ
8 7 adantr ⊢ y ∈ ℤ ∧ ∃ x ∈ ℤ y = 2 ⁢ x → − y ∈ ℤ
9 nfv ⊢ Ⅎ x y ∈ ℤ
10 nfre1 ⊢ Ⅎ x ∃ x ∈ ℤ − y = 2 ⁢ x
11 znegcl ⊢ x ∈ ℤ → − x ∈ ℤ
12 11 adantl ⊢ y ∈ ℤ ∧ x ∈ ℤ → − x ∈ ℤ
13 12 adantr ⊢ y ∈ ℤ ∧ x ∈ ℤ ∧ y = 2 ⁢ x → − x ∈ ℤ
14 oveq2 ⊢ z = − x → 2 ⁢ z = 2 ⁢ − x
15 14 eqeq2d ⊢ z = − x → − y = 2 ⁢ z ↔ − y = 2 ⁢ − x
16 15 adantl ⊢ y ∈ ℤ ∧ x ∈ ℤ ∧ y = 2 ⁢ x ∧ z = − x → − y = 2 ⁢ z ↔ − y = 2 ⁢ − x
17 negeq ⊢ y = 2 ⁢ x → − y = − 2 ⁢ x
18 2cnd ⊢ x ∈ ℤ → 2 ∈ ℂ
19 zcn ⊢ x ∈ ℤ → x ∈ ℂ
20 18 19 mulneg2d ⊢ x ∈ ℤ → 2 ⁢ − x = − 2 ⁢ x
21 20 eqcomd ⊢ x ∈ ℤ → − 2 ⁢ x = 2 ⁢ − x
22 21 adantl ⊢ y ∈ ℤ ∧ x ∈ ℤ → − 2 ⁢ x = 2 ⁢ − x
23 17 22 sylan9eqr ⊢ y ∈ ℤ ∧ x ∈ ℤ ∧ y = 2 ⁢ x → − y = 2 ⁢ − x
24 13 16 23 rspcedvd ⊢ y ∈ ℤ ∧ x ∈ ℤ ∧ y = 2 ⁢ x → ∃ z ∈ ℤ − y = 2 ⁢ z
25 oveq2 ⊢ x = z → 2 ⁢ x = 2 ⁢ z
26 25 eqeq2d ⊢ x = z → − y = 2 ⁢ x ↔ − y = 2 ⁢ z
27 26 cbvrexvw ⊢ ∃ x ∈ ℤ − y = 2 ⁢ x ↔ ∃ z ∈ ℤ − y = 2 ⁢ z
28 24 27 sylibr ⊢ y ∈ ℤ ∧ x ∈ ℤ ∧ y = 2 ⁢ x → ∃ x ∈ ℤ − y = 2 ⁢ x
29 28 exp31 ⊢ y ∈ ℤ → x ∈ ℤ → y = 2 ⁢ x → ∃ x ∈ ℤ − y = 2 ⁢ x
30 9 10 29 rexlimd ⊢ y ∈ ℤ → ∃ x ∈ ℤ y = 2 ⁢ x → ∃ x ∈ ℤ − y = 2 ⁢ x
31 30 imp ⊢ y ∈ ℤ ∧ ∃ x ∈ ℤ y = 2 ⁢ x → ∃ x ∈ ℤ − y = 2 ⁢ x
32 eqeq1 ⊢ z = − y → z = 2 ⁢ x ↔ − y = 2 ⁢ x
33 32 rexbidv ⊢ z = − y → ∃ x ∈ ℤ z = 2 ⁢ x ↔ ∃ x ∈ ℤ − y = 2 ⁢ x
34 33 1 elrab2 ⊢ − y ∈ E ↔ − y ∈ ℤ ∧ ∃ x ∈ ℤ − y = 2 ⁢ x
35 8 31 34 sylanbrc ⊢ y ∈ ℤ ∧ ∃ x ∈ ℤ y = 2 ⁢ x → − y ∈ E
36 6 35 sylbi ⊢ y ∈ E → − y ∈ E
37 oveq1 ⊢ z = − y → z + y = - y + y
38 37 eqeq1d ⊢ z = − y → z + y = 0 ↔ - y + y = 0
39 38 adantl ⊢ y ∈ E ∧ z = − y → z + y = 0 ↔ - y + y = 0
40 elrabi ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℤ
41 40 1 eleq2s ⊢ y ∈ E → y ∈ ℤ
42 41 zcnd ⊢ y ∈ E → y ∈ ℂ
43 42 negcld ⊢ y ∈ E → − y ∈ ℂ
44 43 42 addcomd ⊢ y ∈ E → - y + y = y + − y
45 42 negidd ⊢ y ∈ E → y + − y = 0
46 44 45 eqtrd ⊢ y ∈ E → - y + y = 0
47 36 39 46 rspcedvd ⊢ y ∈ E → ∃ z ∈ E z + y = 0
48 47 rgen ⊢ ∀ y ∈ E ∃ z ∈ E z + y = 0
49 1 2 2zrngbas ⊢ E = Base R
50 1 2 2zrngadd ⊢ + = + R
51 1 2 2zrng0 ⊢ 0 = 0 R
52 49 50 51 isgrp ⊢ R ∈ Grp ↔ R ∈ Mnd ∧ ∀ y ∈ E ∃ z ∈ E z + y = 0
53 3 48 52 mpbir2an ⊢ R ∈ Grp