Theorem 2zrngacmnd

Description: R is a commutative (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	2zrngacmnd	|- R e. CMnd

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	0even	|- 0 e. E
4	1 2	2zrngbas	|- E = ( Base ` R )
5	4	a1i	|- ( 0 e. E -> E = ( Base ` R ) )
6	1 2	2zrngadd	|- + = ( +g ` R )
7	6	a1i	|- ( 0 e. E -> + = ( +g ` R ) )
8	1 2	2zrngamnd	|- R e. Mnd
9	8	a1i	|- ( 0 e. E -> R e. Mnd )
10		elrabi	|- ( x e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> x e. ZZ )
11	10	zcnd	|- ( x e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> x e. CC )
12	11 1	eleq2s	|- ( x e. E -> x e. CC )
13	12	adantr	|- ( ( x e. E /\ y e. E ) -> x e. CC )
14		elrabi	|- ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. ZZ )
15	14	zcnd	|- ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. CC )
16	15 1	eleq2s	|- ( y e. E -> y e. CC )
17	16	adantl	|- ( ( x e. E /\ y e. E ) -> y e. CC )
18	13 17	addcomd	|- ( ( x e. E /\ y e. E ) -> ( x + y ) = ( y + x ) )
19	18	3adant1	|- ( ( 0 e. E /\ x e. E /\ y e. E ) -> ( x + y ) = ( y + x ) )
20	5 7 9 19	iscmnd	|- ( 0 e. E -> R e. CMnd )
21	3 20	ax-mp	|- R e. CMnd