Theorem iscygd

Description: Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Hypotheses	iscyg.1	|- B = ( Base ` G )
	iscyg.2	|- .x. = ( .g ` G )
	iscygd.3	|- ( ph -> G e. Grp )
	iscygd.4	|- ( ph -> X e. B )
	iscygd.5	|- ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. X ) )
Assertion	iscygd	|- ( ph -> G e. CycGrp )

Proof

Step	Hyp	Ref	Expression
1		iscyg.1	|- B = ( Base ` G )
2		iscyg.2	|- .x. = ( .g ` G )
3		iscygd.3	|- ( ph -> G e. Grp )
4		iscygd.4	|- ( ph -> X e. B )
5		iscygd.5	|- ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. X ) )
6	5	ralrimiva	|- ( ph -> A. y e. B E. n e. ZZ y = ( n .x. X ) )
7		eqid	|- { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
8	1 2 7	iscyggen2	|- ( G e. Grp -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } <-> ( X e. B /\ A. y e. B E. n e. ZZ y = ( n .x. X ) ) ) )
9	3 8	syl	|- ( ph -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } <-> ( X e. B /\ A. y e. B E. n e. ZZ y = ( n .x. X ) ) ) )
10	4 6 9	mpbir2and	|- ( ph -> X e. { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } )
11	10	ne0d	|- ( ph -> { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) )
12	1 2 7	iscyg2	|- ( G e. CycGrp <-> ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) ) )
13	3 11 12	sylanbrc	|- ( ph -> G e. CycGrp )