MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-cyg Structured version   Visualization version   GIF version

Definition df-cyg 18201
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
StepHypRef Expression
1 ccyg 18200 . 2 class CycGrp
2 vn . . . . . . 7 setvar 𝑛
3 cz 11321 . . . . . . 7 class
42cv 1479 . . . . . . . 8 class 𝑛
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1479 . . . . . . . 8 class 𝑥
7 vg . . . . . . . . . 10 setvar 𝑔
87cv 1479 . . . . . . . . 9 class 𝑔
9 cmg 17461 . . . . . . . . 9 class .g
108, 9cfv 5847 . . . . . . . 8 class (.g𝑔)
114, 6, 10co 6604 . . . . . . 7 class (𝑛(.g𝑔)𝑥)
122, 3, 11cmpt 4673 . . . . . 6 class (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥))
1312crn 5075 . . . . 5 class ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥))
14 cbs 15781 . . . . . 6 class Base
158, 14cfv 5847 . . . . 5 class (Base‘𝑔)
1613, 15wceq 1480 . . . 4 wff ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)
1716, 5, 15wrex 2908 . . 3 wff 𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)
18 cgrp 17343 . . 3 class Grp
1917, 7, 18crab 2911 . 2 class {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)}
201, 19wceq 1480 1 wff CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)}
Colors of variables: wff setvar class
This definition is referenced by:  iscyg  18202
  Copyright terms: Public domain W3C validator