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

Metamath Proof Explorer

Theorem iscyg2

Description: A cyclic group is a group which contains a generator. (Contributed by Mario Carneiro, 21-Apr-2016)

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

Proof

Step Hyp Ref Expression
1 iscyg.1 
 |-  B = ( Base ` G )
2 iscyg.2 
 |-  .x. = ( .g ` G )
3 iscyg3.e 
 |-  E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
4 1 2 iscyg 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )
5 3 neeq1i 
 |-  ( E =/= (/) <-> { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) )
6 rabn0 
 |-  ( { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B } =/= (/) <-> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B )
7 5 6 bitri 
 |-  ( E =/= (/) <-> E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B )
8 7 anbi2i 
 |-  ( ( G e. Grp /\ E =/= (/) ) <-> ( G e. Grp /\ E. x e. B ran ( n e. ZZ |-> ( n .x. x ) ) = B ) )
9 4 8 bitr4i 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E =/= (/) ) )