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 ⊢Ⅎxy∈ℤ
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∈Ez+y=0
48 47 rgen ⊢∀y∈E∃z∈Ez+y=0
49 1 2 2zrngbas ⊢E=BaseR
50 1 2 2zrngadd ⊢+=+R
51 1 2 2zrng0 ⊢0=0R
52 49 50 51 isgrp ⊢R∈Grp↔R∈Mnd∧∀y∈E∃z∈Ez+y=0
53 3 48 52 mpbir2an ⊢R∈Grp