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	$$⊢\mathrm{CycGrp}=\left\{g\in \mathrm{Grp}|\exists x\in {\mathrm{Base}}_g\mathrm{ran}\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)={\mathrm{Base}}_g\right\}$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccyg	$$class\mathrm{CycGrp}$$
1		vg	$$setvarg$$
2		cgrp	$$class\mathrm{Grp}$$
3		vx	$$setvarx$$
4		cbs	$$class\mathrm{Base}$$
5	1	cv	$$setvarg$$
6	5 4	cfv	$$class{\mathrm{Base}}_g$$
7		vn	$$setvarn$$
8		cz	$$class\mathbb{Z}$$
9	7	cv	$$setvarn$$
10		cmg	$$class{\mathrm{\cdot }}_{𝑔}$$
11	5 10	cfv	$$class{\cdot }_g$$
12	3	cv	$$setvarx$$
13	9 12 11	co	$$class\left(n{\cdot }_{g}x\right)$$
14	7 8 13	cmpt	$$class\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)$$
15	14	crn	$$class\mathrm{ran}\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)$$
16	15 6	wceq	$$wff\mathrm{ran}\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)={\mathrm{Base}}_g$$
17	16 3 6	wrex	$$wff\exists x\in {\mathrm{Base}}_g\mathrm{ran}\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)={\mathrm{Base}}_g$$
18	17 1 2	crab	$$class\left\{g\in \mathrm{Grp}|\exists x\in {\mathrm{Base}}_g\mathrm{ran}\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)={\mathrm{Base}}_g\right\}$$
19	0 18	wceq	$$wff\mathrm{CycGrp}=\left\{g\in \mathrm{Grp}|\exists x\in {\mathrm{Base}}_g\mathrm{ran}\left(n\in \mathbb{Z}⟼n{\cdot }_{g}x\right)={\mathrm{Base}}_g\right\}$$