Definition df-cyg 18280

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 18279	. 2 class CycGrp
2		vn	. . . . . . 7 setvar 𝑛
3		cz 11377	. . . . . . 7 class ℤ
4	2	cv 1482	. . . . . . . 8 class 𝑛
5		vx	. . . . . . . . 9 setvar 𝑥
6	5	cv 1482	. . . . . . . 8 class 𝑥
7		vg	. . . . . . . . . 10 setvar 𝑔
8	7	cv 1482	. . . . . . . . 9 class 𝑔
9		cmg 17540	. . . . . . . . 9 class .g
10	8, 9	cfv 5888	. . . . . . . 8 class (.g‘𝑔)
11	4, 6, 10	co 6650	. . . . . . 7 class (𝑛(.g‘𝑔)𝑥)
12	2, 3, 11	cmpt 4729	. . . . . 6 class (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥))
13	12	crn 5115	. . . . 5 class ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥))
14		cbs 15857	. . . . . 6 class Base
15	8, 14	cfv 5888	. . . . 5 class (Base‘𝑔)
16	13, 15	wceq 1483	. . . 4 wff ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)
17	16, 5, 15	wrex 2913	. . 3 wff ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)
18		cgrp 17422	. . 3 class Grp
19	17, 7, 18	crab 2916	. 2 class {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)}
20	1, 19	wceq 1483	1 wff CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g‘𝑔)𝑥)) = (Base‘𝑔)}

This definition is referenced by:  iscyg  18281