Metamath Proof Explorer

Theorem 2zrngacmnd

Description: R is a commutative (additive) monoid. (Contributed by AV, 11-Feb-2020)

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

Proof

Step Hyp Ref Expression
1 2zrng.e ⊢ E = z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x
2 2zrngbas.r ⊢ R = ℂ fld ↾ 𝑠 E
3 1 0even ⊢ 0 ∈ E
4 1 2 2zrngbas ⊢ E = Base R
5 4 a1i ⊢ 0 ∈ E → E = Base R
6 1 2 2zrngadd ⊢ + = + R
7 6 a1i ⊢ 0 ∈ E → + = + R
8 1 2 2zrngamnd ⊢ R ∈ Mnd
9 8 a1i ⊢ 0 ∈ E → R ∈ Mnd
10 elrabi ⊢ x ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → x ∈ ℤ
11 10 zcnd ⊢ x ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → x ∈ ℂ
12 11 1 eleq2s ⊢ x ∈ E → x ∈ ℂ
13 12 adantr ⊢ x ∈ E ∧ y ∈ E → x ∈ ℂ
14 elrabi ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℤ
15 14 zcnd ⊢ y ∈ z ∈ ℤ | ∃ x ∈ ℤ z = 2 ⁢ x → y ∈ ℂ
16 15 1 eleq2s ⊢ y ∈ E → y ∈ ℂ
17 16 adantl ⊢ x ∈ E ∧ y ∈ E → y ∈ ℂ
18 13 17 addcomd ⊢ x ∈ E ∧ y ∈ E → x + y = y + x
19 18 3adant1 ⊢ 0 ∈ E ∧ x ∈ E ∧ y ∈ E → x + y = y + x
20 5 7 9 19 iscmnd ⊢ 0 ∈ E → R ∈ CMnd
21 3 20 ax-mp ⊢ R ∈ CMnd