Definition df-cyg

Description: Define a cyclic group, which is a group with an element x , called the generator of the group, such that all elements in the group are multiples of x . A generator is usually not unique. (Contributed by Mario Carneiro, 21-Apr-2016)

	Ref	Expression
Assertion	df-cyg	|- CycGrp = { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccyg	|- CycGrp
1		vg	|- g
2		cgrp	|- Grp
3		vx	|- x
4		cbs	|- Base
5	1	cv	|- g
6	5 4	cfv	|- ( Base ` g )
7		vn	|- n
8		cz	|- ZZ
9	7	cv	|- n
10		cmg	|- .g
11	5 10	cfv	|- ( .g ` g )
12	3	cv	|- x
13	9 12 11	co	|- ( n ( .g ` g ) x )
14	7 8 13	cmpt	|- ( n e. ZZ |-> ( n ( .g ` g ) x ) )
15	14	crn	|- ran ( n e. ZZ |-> ( n ( .g ` g ) x ) )
16	15 6	wceq	|- ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g )
17	16 3 6	wrex	|- E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g )
18	17 1 2	crab	|- { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }
19	0 18	wceq	|- CycGrp = { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }