Theorem 2zrngamnd

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

	Ref	Expression
Hypotheses	2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
	2zrngbas.r	|- R = ( CCfld |`s E )
Assertion	2zrngamnd	|- R e. Mnd

Proof

Step	Hyp	Ref	Expression
1		2zrng.e	|- E = { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) }
2		2zrngbas.r	|- R = ( CCfld |`s E )
3	1 2	2zrngasgrp	|- R e. Smgrp
4	1	0even	|- 0 e. E
5		id	|- ( 0 e. E -> 0 e. E )
6		oveq1	|- ( x = 0 -> ( x + y ) = ( 0 + y ) )
7	6	eqeq1d	|- ( x = 0 -> ( ( x + y ) = y <-> ( 0 + y ) = y ) )
8	7	ovanraleqv	|- ( x = 0 -> ( A. y e. E ( ( x + y ) = y /\ ( y + x ) = y ) <-> A. y e. E ( ( 0 + y ) = y /\ ( y + 0 ) = y ) ) )
9	8	adantl	|- ( ( 0 e. E /\ x = 0 ) -> ( A. y e. E ( ( x + y ) = y /\ ( y + x ) = y ) <-> A. y e. E ( ( 0 + y ) = y /\ ( y + 0 ) = y ) ) )
10		elrabi	|- ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. ZZ )
11	10 1	eleq2s	|- ( y e. E -> y e. ZZ )
12	11	zcnd	|- ( y e. E -> y e. CC )
13		addid2	|- ( y e. CC -> ( 0 + y ) = y )
14		addid1	|- ( y e. CC -> ( y + 0 ) = y )
15	13 14	jca	|- ( y e. CC -> ( ( 0 + y ) = y /\ ( y + 0 ) = y ) )
16	12 15	syl	|- ( y e. E -> ( ( 0 + y ) = y /\ ( y + 0 ) = y ) )
17	16	adantl	|- ( ( 0 e. E /\ y e. E ) -> ( ( 0 + y ) = y /\ ( y + 0 ) = y ) )
18	17	ralrimiva	|- ( 0 e. E -> A. y e. E ( ( 0 + y ) = y /\ ( y + 0 ) = y ) )
19	5 9 18	rspcedvd	|- ( 0 e. E -> E. x e. E A. y e. E ( ( x + y ) = y /\ ( y + x ) = y ) )
20	4 19	ax-mp	|- E. x e. E A. y e. E ( ( x + y ) = y /\ ( y + x ) = y )
21	1 2	2zrngbas	|- E = ( Base ` R )
22	1 2	2zrngadd	|- + = ( +g ` R )
23	21 22	ismnddef	|- ( R e. Mnd <-> ( R e. Smgrp /\ E. x e. E A. y e. E ( ( x + y ) = y /\ ( y + x ) = y ) ) )
24	3 20 23	mpbir2an	|- R e. Mnd