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

Definition df-cyg 15165
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 15164 . 2  class CycGrp
2 vn . . . . . . 7  set  n
3 cz 10024 . . . . . . 7  class  ZZ
42cv 1622 . . . . . . . 8  class  n
5 vx . . . . . . . . 9  set  x
65cv 1622 . . . . . . . 8  class  x
7 vg . . . . . . . . . 10  set  g
87cv 1622 . . . . . . . . 9  class  g
9 cmg 14366 . . . . . . . . 9  class .g
108, 9cfv 5255 . . . . . . . 8  class  (.g `  g
)
114, 6, 10co 5858 . . . . . . 7  class  ( n (.g `  g ) x )
122, 3, 11cmpt 4077 . . . . . 6  class  ( n  e.  ZZ  |->  ( n (.g `  g ) x ) )
1312crn 4690 . . . . 5  class  ran  (
n  e.  ZZ  |->  ( n (.g `  g ) x ) )
14 cbs 13148 . . . . . 6  class  Base
158, 14cfv 5255 . . . . 5  class  ( Base `  g )
1613, 15wceq 1623 . . . 4  wff  ran  (
n  e.  ZZ  |->  ( n (.g `  g ) x ) )  =  (
Base `  g )
1716, 5, 15wrex 2544 . . 3  wff  E. x  e.  ( Base `  g
) ran  ( n  e.  ZZ  |->  ( n (.g `  g ) x ) )  =  ( Base `  g )
18 cgrp 14362 . . 3  class  Grp
1917, 7, 18crab 2547 . 2  class  { g  e.  Grp  |  E. x  e.  ( Base `  g ) ran  (
n  e.  ZZ  |->  ( n (.g `  g ) x ) )  =  (
Base `  g ) }
201, 19wceq 1623 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 set class
This definition is referenced by:  iscyg  15166
  Copyright terms: Public domain W3C validator