Definition df-cyg 18280

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.)

Assertion

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

Distinct variable group:   g, n, x

Detailed syntax breakdown of Definition df-cyg

Step	Hyp	Ref	Expression
1		ccyg 18279	. 2 class CycGrp
2		vn	. . . . . . 7 setvar n
3		cz 11377	. . . . . . 7 class ZZ
4	2	cv 1482	. . . . . . . 8 class n
5		vx	. . . . . . . . 9 setvar x
6	5	cv 1482	. . . . . . . 8 class x
7		vg	. . . . . . . . . 10 setvar g
8	7	cv 1482	. . . . . . . . 9 class g
9		cmg 17540	. . . . . . . . 9 class .g
10	8, 9	cfv 5888	. . . . . . . 8 class (.g ` g )
11	4, 6, 10	co 6650	. . . . . . 7 class ( n (.g ` g ) x )
12	2, 3, 11	cmpt 4729	. . . . . 6 class ( n e. ZZ |-> ( n (.g ` g ) x ) )
13	12	crn 5115	. . . . 5 class ran ( n e. ZZ |-> ( n (.g ` g ) x ) )
14		cbs 15857	. . . . . 6 class Base
15	8, 14	cfv 5888	. . . . 5 class ( Base ` g )
16	13, 15	wceq 1483	. . . 4 wff ran ( n e. ZZ |-> ( n (.g ` g ) x ) ) = ( Base ` g )
17	16, 5, 15	wrex 2913	. . 3 wff E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n (.g ` g ) x ) ) = ( Base ` g )
18		cgrp 17422	. . 3 class Grp
19	17, 7, 18	crab 2916	. 2 class { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n (.g ` g ) x ) ) = ( Base ` g ) }
20	1, 19	wceq 1483	1 wff CycGrp = { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n (.g ` g ) x ) ) = ( Base ` g ) }

This definition is referenced by:  iscyg  18281