Theorem 2zrngacmnd

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

	Ref	Expression
Hypotheses	2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
	2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
Assertion	2zrngacmnd	⊢ 𝑅 ∈ CMnd

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3	1	0even	⊢ 0 ∈ 𝐸
4	1 2	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )
5	4	a1i	⊢ ( 0 ∈ 𝐸 → 𝐸 = ( Base ‘ 𝑅 ) )
6	1 2	2zrngadd	⊢ + = ( +g ‘ 𝑅 )
7	6	a1i	⊢ ( 0 ∈ 𝐸 → + = ( +g ‘ 𝑅 ) )
8	1 2	2zrngamnd	⊢ 𝑅 ∈ Mnd
9	8	a1i	⊢ ( 0 ∈ 𝐸 → 𝑅 ∈ Mnd )
10		elrabi	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑥 ∈ ℤ )
11	10	zcnd	⊢ ( 𝑥 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑥 ∈ ℂ )
12	11 1	eleq2s	⊢ ( 𝑥 ∈ 𝐸 → 𝑥 ∈ ℂ )
13	12	adantr	⊢ ( ( 𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) → 𝑥 ∈ ℂ )
14		elrabi	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℤ )
15	14	zcnd	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℂ )
16	15 1	eleq2s	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ℂ )
17	16	adantl	⊢ ( ( 𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) → 𝑦 ∈ ℂ )
18	13 17	addcomd	⊢ ( ( 𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
19	18	3adant1	⊢ ( ( 0 ∈ 𝐸 ∧ 𝑥 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) → ( 𝑥 + 𝑦 ) = ( 𝑦 + 𝑥 ) )
20	5 7 9 19	iscmnd	⊢ ( 0 ∈ 𝐸 → 𝑅 ∈ CMnd )
21	3 20	ax-mp	⊢ 𝑅 ∈ CMnd