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

Metamath Proof Explorer

Theorem iscygd

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 )
iscygd.3 
|- ( ph -> G e. Grp )
iscygd.4 
|- ( ph -> X e. B )
iscygd.5 
|- ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. X ) )
Assertion iscygd 
|- ( ph -> G e. CycGrp )

Proof

Step Hyp Ref Expression
1 iscyg.1 
 |-  B = ( Base ` G )
2 iscyg.2 
 |-  .x. = ( .g ` G )
3 iscygd.3 
 |-  ( ph -> G e. Grp )
4 iscygd.4 
 |-  ( ph -> X e. B )
5 iscygd.5 
 |-  ( ( ph /\ y e. B ) -> E. n e. ZZ y = ( n .x. X ) )
6 5 ralrimiva 
 |-  ( ph -> A. y e. B E. n e. ZZ y = ( n .x. X ) )
7 eqid 
 |-  { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
8 1 2 7 iscyggen2 
 |-  ( G e. Grp -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } <-> ( X e. B /\ A. y e. B E. n e. ZZ y = ( n .x. X ) ) ) )
9 3 8 syl 
 |-  ( ph -> ( X e. { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } <-> ( X e. B /\ A. y e. B E. n e. ZZ y = ( n .x. X ) ) ) )
10 4 6 9 mpbir2and 
 |-  ( ph -> X e. { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } )
11 10 ne0d 
 |-  ( ph -> { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) )
12 1 2 7 iscyg2 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) ) )
13 3 11 12 sylanbrc 
 |-  ( ph -> G e. CycGrp )