Theorem 2zrngamnd

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

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

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	⊢ 𝐸 = { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) }
2		2zrngbas.r	⊢ 𝑅 = ( ℂfld ↾s 𝐸 )
3	1 2	2zrngasgrp	⊢ 𝑅 ∈ Smgrp
4	1	0even	⊢ 0 ∈ 𝐸
5		id	⊢ ( 0 ∈ 𝐸 → 0 ∈ 𝐸 )
6		oveq1	⊢ ( 𝑥 = 0 → ( 𝑥 + 𝑦 ) = ( 0 + 𝑦 ) )
7	6	eqeq1d	⊢ ( 𝑥 = 0 → ( ( 𝑥 + 𝑦 ) = 𝑦 ↔ ( 0 + 𝑦 ) = 𝑦 ) )
8	7	ovanraleqv	⊢ ( 𝑥 = 0 → ( ∀ 𝑦 ∈ 𝐸 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐸 ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) ) )
9	8	adantl	⊢ ( ( 0 ∈ 𝐸 ∧ 𝑥 = 0 ) → ( ∀ 𝑦 ∈ 𝐸 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ↔ ∀ 𝑦 ∈ 𝐸 ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) ) )
10		elrabi	⊢ ( 𝑦 ∈ { 𝑧 ∈ ℤ ∣ ∃ 𝑥 ∈ ℤ 𝑧 = ( 2 · 𝑥 ) } → 𝑦 ∈ ℤ )
11	10 1	eleq2s	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ℤ )
12	11	zcnd	⊢ ( 𝑦 ∈ 𝐸 → 𝑦 ∈ ℂ )
13		addid2	⊢ ( 𝑦 ∈ ℂ → ( 0 + 𝑦 ) = 𝑦 )
14		addid1	⊢ ( 𝑦 ∈ ℂ → ( 𝑦 + 0 ) = 𝑦 )
15	13 14	jca	⊢ ( 𝑦 ∈ ℂ → ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) )
16	12 15	syl	⊢ ( 𝑦 ∈ 𝐸 → ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) )
17	16	adantl	⊢ ( ( 0 ∈ 𝐸 ∧ 𝑦 ∈ 𝐸 ) → ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) )
18	17	ralrimiva	⊢ ( 0 ∈ 𝐸 → ∀ 𝑦 ∈ 𝐸 ( ( 0 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 0 ) = 𝑦 ) )
19	5 9 18	rspcedvd	⊢ ( 0 ∈ 𝐸 → ∃ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) )
20	4 19	ax-mp	⊢ ∃ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 )
21	1 2	2zrngbas	⊢ 𝐸 = ( Base ‘ 𝑅 )
22	1 2	2zrngadd	⊢ + = ( +g ‘ 𝑅 )
23	21 22	ismnddef	⊢ ( 𝑅 ∈ Mnd ↔ ( 𝑅 ∈ Smgrp ∧ ∃ 𝑥 ∈ 𝐸 ∀ 𝑦 ∈ 𝐸 ( ( 𝑥 + 𝑦 ) = 𝑦 ∧ ( 𝑦 + 𝑥 ) = 𝑦 ) ) )
24	3 20 23	mpbir2an	⊢ 𝑅 ∈ Mnd