Metamath Proof Explorer

Theorem 2zrngamgm

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

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

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢E=z∈ℤ|∃x∈ℤz=2⁢x
2 2zrngbas.r ⊢R=ℂfld↾𝑠E
3 eqeq1 ⊢z=a→z=2⁢x↔a=2⁢x
4 3 rexbidv ⊢z=a→∃x∈ℤz=2⁢x↔∃x∈ℤa=2⁢x
5 4 1 elrab2 ⊢a∈E↔a∈ℤ∧∃x∈ℤa=2⁢x
6 eqeq1 ⊢z=b→z=2⁢x↔b=2⁢x
7 6 rexbidv ⊢z=b→∃x∈ℤz=2⁢x↔∃x∈ℤb=2⁢x
8 7 1 elrab2 ⊢b∈E↔b∈ℤ∧∃x∈ℤb=2⁢x
9 oveq2 ⊢x=y→2⁢x=2⁢y
10 9 eqeq2d ⊢x=y→a=2⁢x↔a=2⁢y
11 10 cbvrexvw ⊢∃x∈ℤa=2⁢x↔∃y∈ℤa=2⁢y
12 zaddcl ⊢a∈ℤ∧b∈ℤ→a+b∈ℤ
13 12 ancoms ⊢b∈ℤ∧a∈ℤ→a+b∈ℤ
14 13 adantr ⊢b∈ℤ∧a∈ℤ∧∃x∈ℤb=2⁢x∧∃y∈ℤa=2⁢y→a+b∈ℤ
15 simpl ⊢y∈ℤ∧a=2⁢y→y∈ℤ
16 simpl ⊢x∈ℤ∧b=2⁢x→x∈ℤ
17 zaddcl ⊢y∈ℤ∧x∈ℤ→y+x∈ℤ
18 15 16 17 syl2anr ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→y+x∈ℤ
19 18 adantr ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→y+x∈ℤ
20 oveq2 ⊢z=y+x→2⁢z=2⁢y+x
21 20 eqeq2d ⊢z=y+x→2⁢y+x=2⁢z↔2⁢y+x=2⁢y+x
22 21 adantl ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ∧z=y+x→2⁢y+x=2⁢z↔2⁢y+x=2⁢y+x
23 eqidd ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→2⁢y+x=2⁢y+x
24 19 22 23 rspcedvd ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→∃z∈ℤ2⁢y+x=2⁢z
25 simpr ⊢y∈ℤ∧a=2⁢y→a=2⁢y
26 simpr ⊢x∈ℤ∧b=2⁢x→b=2⁢x
27 25 26 oveqan12rd ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→a+b=2⁢y+2⁢x
28 27 adantr ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→a+b=2⁢y+2⁢x
29 2cnd ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→2∈ℂ
30 zcn ⊢y∈ℤ→y∈ℂ
31 30 adantr ⊢y∈ℤ∧a=2⁢y→y∈ℂ
32 31 adantl ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→y∈ℂ
33 zcn ⊢x∈ℤ→x∈ℂ
34 33 adantr ⊢x∈ℤ∧b=2⁢x→x∈ℂ
35 34 adantr ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→x∈ℂ
36 29 32 35 adddid ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→2⁢y+x=2⁢y+2⁢x
37 36 adantr ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→2⁢y+x=2⁢y+2⁢x
38 28 37 eqtr4d ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→a+b=2⁢y+x
39 38 eqeq1d ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→a+b=2⁢z↔2⁢y+x=2⁢z
40 39 rexbidv ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→∃z∈ℤa+b=2⁢z↔∃z∈ℤ2⁢y+x=2⁢z
41 24 40 mpbird ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y∧b∈ℤ∧a∈ℤ→∃z∈ℤa+b=2⁢z
42 41 ex ⊢x∈ℤ∧b=2⁢x∧y∈ℤ∧a=2⁢y→b∈ℤ∧a∈ℤ→∃z∈ℤa+b=2⁢z
43 42 rexlimdvaa ⊢x∈ℤ∧b=2⁢x→∃y∈ℤa=2⁢y→b∈ℤ∧a∈ℤ→∃z∈ℤa+b=2⁢z
44 43 rexlimiva ⊢∃x∈ℤb=2⁢x→∃y∈ℤa=2⁢y→b∈ℤ∧a∈ℤ→∃z∈ℤa+b=2⁢z
45 44 imp ⊢∃x∈ℤb=2⁢x∧∃y∈ℤa=2⁢y→b∈ℤ∧a∈ℤ→∃z∈ℤa+b=2⁢z
46 oveq2 ⊢x=z→2⁢x=2⁢z
47 46 eqeq2d ⊢x=z→a+b=2⁢x↔a+b=2⁢z
48 47 cbvrexvw ⊢∃x∈ℤa+b=2⁢x↔∃z∈ℤa+b=2⁢z
49 45 48 syl6ibr ⊢∃x∈ℤb=2⁢x∧∃y∈ℤa=2⁢y→b∈ℤ∧a∈ℤ→∃x∈ℤa+b=2⁢x
50 49 impcom ⊢b∈ℤ∧a∈ℤ∧∃x∈ℤb=2⁢x∧∃y∈ℤa=2⁢y→∃x∈ℤa+b=2⁢x
51 eqeq1 ⊢z=a+b→z=2⁢x↔a+b=2⁢x
52 51 rexbidv ⊢z=a+b→∃x∈ℤz=2⁢x↔∃x∈ℤa+b=2⁢x
53 52 1 elrab2 ⊢a+b∈E↔a+b∈ℤ∧∃x∈ℤa+b=2⁢x
54 14 50 53 sylanbrc ⊢b∈ℤ∧a∈ℤ∧∃x∈ℤb=2⁢x∧∃y∈ℤa=2⁢y→a+b∈E
55 54 exp32 ⊢b∈ℤ∧a∈ℤ→∃x∈ℤb=2⁢x→∃y∈ℤa=2⁢y→a+b∈E
56 55 impancom ⊢b∈ℤ∧∃x∈ℤb=2⁢x→a∈ℤ→∃y∈ℤa=2⁢y→a+b∈E
57 56 com13 ⊢∃y∈ℤa=2⁢y→a∈ℤ→b∈ℤ∧∃x∈ℤb=2⁢x→a+b∈E
58 11 57 sylbi ⊢∃x∈ℤa=2⁢x→a∈ℤ→b∈ℤ∧∃x∈ℤb=2⁢x→a+b∈E
59 58 impcom ⊢a∈ℤ∧∃x∈ℤa=2⁢x→b∈ℤ∧∃x∈ℤb=2⁢x→a+b∈E
60 59 imp ⊢a∈ℤ∧∃x∈ℤa=2⁢x∧b∈ℤ∧∃x∈ℤb=2⁢x→a+b∈E
61 5 8 60 syl2anb ⊢a∈E∧b∈E→a+b∈E
62 61 rgen2 ⊢∀a∈E∀b∈Ea+b∈E
63 0z ⊢0∈ℤ
64 2cn ⊢2∈ℂ
65 0zd ⊢2∈ℂ→0∈ℤ
66 oveq2 ⊢x=0→2⁢x=2⋅0
67 66 eqeq2d ⊢x=0→0=2⁢x↔0=2⋅0
68 67 adantl ⊢2∈ℂ∧x=0→0=2⁢x↔0=2⋅0
69 mul01 ⊢2∈ℂ→2⋅0=0
70 69 eqcomd ⊢2∈ℂ→0=2⋅0
71 65 68 70 rspcedvd ⊢2∈ℂ→∃x∈ℤ0=2⁢x
72 64 71 ax-mp ⊢∃x∈ℤ0=2⁢x
73 eqeq1 ⊢z=0→z=2⁢x↔0=2⁢x
74 73 rexbidv ⊢z=0→∃x∈ℤz=2⁢x↔∃x∈ℤ0=2⁢x
75 74 elrab ⊢0∈z∈ℤ|∃x∈ℤz=2⁢x↔0∈ℤ∧∃x∈ℤ0=2⁢x
76 63 72 75 mpbir2an ⊢0∈z∈ℤ|∃x∈ℤz=2⁢x
77 76 1 eleqtrri ⊢0∈E
78 1 2 2zrngbas ⊢E=BaseR
79 1 2 2zrngadd ⊢+=+R
80 78 79 ismgmn0 ⊢0∈E→R∈Mgm↔∀a∈E∀b∈Ea+b∈E
81 77 80 ax-mp ⊢R∈Mgm↔∀a∈E∀b∈Ea+b∈E
82 62 81 mpbir ⊢R∈Mgm