Metamath Proof Explorer

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 = g ∈ Grp | ∃ x ∈ Base g ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccyg class CycGrp
1 vg setvar g
2 cgrp class Grp
3 vx setvar x
4 cbs class Base
5 1 cv setvar g
6 5 4 cfv class Base g
7 vn setvar n
8 cz class ℤ
9 7 cv setvar n
10 cmg class ⋅ 𝑔
11 5 10 cfv class ⋅ g
12 3 cv setvar x
13 9 12 11 co class n ⋅ g x
14 7 8 13 cmpt class n ∈ ℤ ⟼ n ⋅ g x
15 14 crn class ran ⁡ n ∈ ℤ ⟼ n ⋅ g x
16 15 6 wceq wff ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g
17 16 3 6 wrex wff ∃ x ∈ Base g ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g
18 17 1 2 crab class g ∈ Grp | ∃ x ∈ Base g ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g
19 0 18 wceq wff CycGrp = g ∈ Grp | ∃ x ∈ Base g ran ⁡ n ∈ ℤ ⟼ n ⋅ g x = Base g