Metamath Proof Explorer

Theorem cyggrp

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

Ref Expression
Assertion cyggrp 
|- ( G e. CycGrp -> G e. Grp )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( Base ` G ) = ( Base ` G )
2 eqid 
 |-  ( .g ` G ) = ( .g ` G )
3 1 2 iscyg 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ E. x e. ( Base ` G ) ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = ( Base ` G ) ) )
4 3 simplbi 
 |-  ( G e. CycGrp -> G e. Grp )