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 = { 𝑔 ∈ Grp ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 ) }

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		ccyg	⊢ CycGrp
1		vg	⊢ 𝑔
2		cgrp	⊢ Grp
3		vx	⊢ 𝑥
4		cbs	⊢ Base
5	1	cv	⊢ 𝑔
6	5 4	cfv	⊢ ( Base ‘ 𝑔 )
7		vn	⊢ 𝑛
8		cz	⊢ ℤ
9	7	cv	⊢ 𝑛
10		cmg	⊢ .g
11	5 10	cfv	⊢ ( .g ‘ 𝑔 )
12	3	cv	⊢ 𝑥
13	9 12 11	co	⊢ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 )
14	7 8 13	cmpt	⊢ ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) )
15	14	crn	⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) )
16	15 6	wceq	⊢ ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 )
17	16 3 6	wrex	⊢ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 )
18	17 1 2	crab	⊢ { 𝑔 ∈ Grp ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 ) }
19	0 18	wceq	⊢ CycGrp = { 𝑔 ∈ Grp ∣ ∃ 𝑥 ∈ ( Base ‘ 𝑔 ) ran ( 𝑛 ∈ ℤ ↦ ( 𝑛 ( .g ‘ 𝑔 ) 𝑥 ) ) = ( Base ‘ 𝑔 ) }