Theorem 2zrngasgrp

Description: R is an (additive) semigroup. (Contributed by AV, 4-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	2zrngasgrp	|- R e. Smgrp

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	2zrngamgm	|- R e. Mgm
4		elrabi	|- ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> a e. ZZ )
5		elrabi	|- ( y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> y e. ZZ )
6		elrabi	|- ( b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } -> b e. ZZ )
7	4 5 6	3anim123i	|- ( ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ) -> ( a e. ZZ /\ y e. ZZ /\ b e. ZZ ) )
8		zcn	|- ( a e. ZZ -> a e. CC )
9		zcn	|- ( y e. ZZ -> y e. CC )
10		zcn	|- ( b e. ZZ -> b e. CC )
11	8 9 10	3anim123i	|- ( ( a e. ZZ /\ y e. ZZ /\ b e. ZZ ) -> ( a e. CC /\ y e. CC /\ b e. CC ) )
12		addass	|- ( ( a e. CC /\ y e. CC /\ b e. CC ) -> ( ( a + y ) + b ) = ( a + ( y + b ) ) )
13	7 11 12	3syl	|- ( ( a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } /\ b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ) -> ( ( a + y ) + b ) = ( a + ( y + b ) ) )
14	13	rgen3	|- A. a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ( ( a + y ) + b ) = ( a + ( y + b ) )
15	1 2	2zrngbas	|- E = ( Base ` R )
16	1 15	eqtr3i	|- { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } = ( Base ` R )
17	1 2	2zrngadd	|- + = ( +g ` R )
18	16 17	issgrp	|- ( R e. Smgrp <-> ( R e. Mgm /\ A. a e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. y e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } A. b e. { z e. ZZ | E. x e. ZZ z = ( 2 x. x ) } ( ( a + y ) + b ) = ( a + ( y + b ) ) ) )
19	3 14 18	mpbir2an	|- R e. Smgrp