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 18103
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 18102 . 2 class CycGrp
2 vn . . . . . . 7 setvar 𝑛
3 cz 11254 . . . . . . 7 class
42cv 1474 . . . . . . . 8 class 𝑛
5 vx . . . . . . . . 9 setvar 𝑥
65cv 1474 . . . . . . . 8 class 𝑥
7 vg . . . . . . . . . 10 setvar 𝑔
87cv 1474 . . . . . . . . 9 class 𝑔
9 cmg 17363 . . . . . . . . 9 class .g
108, 9cfv 5804 . . . . . . . 8 class (.g𝑔)
114, 6, 10co 6549 . . . . . . 7 class (𝑛(.g𝑔)𝑥)
122, 3, 11cmpt 4643 . . . . . 6 class (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥))
1312crn 5039 . . . . 5 class ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥))
14 cbs 15695 . . . . . 6 class Base
158, 14cfv 5804 . . . . 5 class (Base‘𝑔)
1613, 15wceq 1475 . . . 4 wff ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)
1716, 5, 15wrex 2897 . . 3 wff 𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)
18 cgrp 17245 . . 3 class Grp
1917, 7, 18crab 2900 . 2 class {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)}
201, 19wceq 1475 1 wff CycGrp = {𝑔 ∈ Grp ∣ ∃𝑥 ∈ (Base‘𝑔)ran (𝑛 ∈ ℤ ↦ (𝑛(.g𝑔)𝑥)) = (Base‘𝑔)}
Colors of variables: wff setvar class
This definition is referenced by:  iscyg  18104
  Copyright terms: Public domain W3C validator