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

Definition df-cyg 16360
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.)
Assertion
Ref Expression
df-cyg  |- CycGrp  =  {
g  e.  Grp  |  E. x  e.  ( Base `  g ) ran  ( n  e.  ZZ  |->  ( n (.g `  g
) x ) )  =  ( Base `  g
) }
Distinct variable group:    g, n, x

Detailed syntax breakdown of Definition df-cyg
StepHypRef Expression
1 ccyg 16359 . 2  class CycGrp
2 vn . . . . . . 7  setvar  n
3 cz 10651 . . . . . . 7  class  ZZ
42cv 1368 . . . . . . . 8  class  n
5 vx . . . . . . . . 9  setvar  x
65cv 1368 . . . . . . . 8  class  x
7 vg . . . . . . . . . 10  setvar  g
87cv 1368 . . . . . . . . 9  class  g
9 cmg 15419 . . . . . . . . 9  class .g
108, 9cfv 5423 . . . . . . . 8  class  (.g `  g
)
114, 6, 10co 6096 . . . . . . 7  class  ( n (.g `  g ) x )
122, 3, 11cmpt 4355 . . . . . 6  class  ( n  e.  ZZ  |->  ( n (.g `  g ) x ) )
1312crn 4846 . . . . 5  class  ran  (
n  e.  ZZ  |->  ( n (.g `  g ) x ) )
14 cbs 14179 . . . . . 6  class  Base
158, 14cfv 5423 . . . . 5  class  ( Base `  g )
1613, 15wceq 1369 . . . 4  wff  ran  (
n  e.  ZZ  |->  ( n (.g `  g ) x ) )  =  (
Base `  g )
1716, 5, 15wrex 2721 . . 3  wff  E. x  e.  ( Base `  g
) ran  ( n  e.  ZZ  |->  ( n (.g `  g ) x ) )  =  ( Base `  g )
18 cgrp 15415 . . 3  class  Grp
1917, 7, 18crab 2724 . 2  class  { g  e.  Grp  |  E. x  e.  ( Base `  g ) ran  (
n  e.  ZZ  |->  ( n (.g `  g ) x ) )  =  (
Base `  g ) }
201, 19wceq 1369 1  wff CycGrp  =  {
g  e.  Grp  |  E. x  e.  ( Base `  g ) ran  ( n  e.  ZZ  |->  ( n (.g `  g
) x ) )  =  ( Base `  g
) }
Colors of variables: wff setvar class
This definition is referenced by:  iscyg  16361
  Copyright terms: Public domain W3C validator