This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }

Detailed syntax breakdown

Step Hyp Ref Expression
0 ccyg 
 |-  CycGrp
1 vg 
 |-  g
2 cgrp 
 |-  Grp
3 vx 
 |-  x
4 cbs 
 |-  Base
5 1 cv 
 |-  g
6 5 4 cfv 
 |-  ( Base ` g )
7 vn 
 |-  n
8 cz 
 |-  ZZ
9 7 cv 
 |-  n
10 cmg 
 |-  .g
11 5 10 cfv 
 |-  ( .g ` g )
12 3 cv 
 |-  x
13 9 12 11 co 
 |-  ( n ( .g ` g ) x )
14 7 8 13 cmpt 
 |-  ( n e. ZZ |-> ( n ( .g ` g ) x ) )
15 14 crn 
 |-  ran ( n e. ZZ |-> ( n ( .g ` g ) x ) )
16 15 6 wceq 
 |-  ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g )
17 16 3 6 wrex 
 |-  E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g )
18 17 1 2 crab 
 |-  { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }
19 0 18 wceq 
 |-  CycGrp = { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }