Metamath Proof Explorer

Theorem iscyg

Description: Definition of a cyclic group. (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses iscyg.1 
|- B = ( Base ` G )
iscyg.2 
|- .x. = ( .g ` G )
Assertion iscyg 
|- ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )

Proof

Step Hyp Ref Expression
1 iscyg.1 
 |-  B = ( Base ` G )
2 iscyg.2 
 |-  .x. = ( .g ` G )
3 fveq2 
 |-  ( g = G -> ( Base ` g ) = ( Base ` G ) )
4 3 1 eqtr4di 
 |-  ( g = G -> ( Base ` g ) = B )
5 fveq2 
 |-  ( g = G -> ( .g ` g ) = ( .g ` G ) )
6 5 2 eqtr4di 
 |-  ( g = G -> ( .g ` g ) = .x. )
7 6 oveqd 
 |-  ( g = G -> ( n ( .g ` g ) x ) = ( n .x. x ) )
8 7 mpteq2dv 
 |-  ( g = G -> ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( n e. ZZ |-> ( n .x. x ) ) )
9 8 rneqd 
 |-  ( g = G -> ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ran ( n e. ZZ |-> ( n .x. x ) ) )
10 9 4 eqeq12d 
 |-  ( g = G -> ( ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) <-> ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )
11 4 10 rexeqbidv 
 |-  ( g = G -> ( E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) <-> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )
12 df-cyg 
 |-  CycGrp = { g e. Grp | E. x e. ( Base ` g ) ran ( n e. ZZ |-> ( n ( .g ` g ) x ) ) = ( Base ` g ) }
13 11 12 elrab2 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )