Definition df-cyg 19487

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

Assertion

Ref	Expression
df-cyg	⊢ CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)}

Distinct variable group:   𝑔,𝑛,𝑥

Detailed syntax breakdown of Definition df-cyg

Step	Hyp	Ref	Expression
1		ccyg 19486	. 2 class CycGrp
2		vn	. . . . . . 7 setvar 𝑛
3		cz 12328	. . . . . . 7 class ℤ
4	2	cv 1538	. . . . . . . 8 class 𝑛
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1538	. . . . . . . 8 class 𝑥
7		vg	. . . . . . . . . 10 setvar 𝑔
8	7	cv 1538	. . . . . . . . 9 class 𝑔
9		cmg 18709	. . . . . . . . 9 class .g
10	8, 9	cfv 6437	. . . . . . . 8 class (.g‘𝑔)
11	4, 6, 10	co 7284	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
12	2, 3, 11	cmpt 5158	. . . . . 6 class (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥))
13	12	crn 5591	. . . . 5 class ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥))
14		cbs 16921	. . . . . 6 class Base
15	8, 14	cfv 6437	. . . . 5 class (Base‘𝑔)
16	13, 15	wceq 1539	. . . 4 wff ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)
17	16, 5, 15	wrex 3066	. . 3 wff ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)
18		cgrp 18586	. . 3 class Grp
19	17, 7, 18	crab 3069	. 2 class {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)}
20	1, 19	wceq 1539	1 wff CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)}

This definition is referenced by:  iscyg  19488