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

Metamath Proof Explorer

Theorem cygzn

Description: A cyclic group with n elements is isomorphic to ZZ / n ZZ , and an infinite cyclic group is isomorphic to ZZ / 0 ZZ ~ZZ . (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypotheses cygzn.b 
|- B = ( Base ` G )
cygzn.n 
|- N = if ( B e. Fin , ( # ` B ) , 0 )
cygzn.y 
|- Y = ( Z/nZ ` N )
Assertion cygzn 
|- ( G e. CycGrp -> G ~=g Y )

Proof

Step Hyp Ref Expression
1 cygzn.b 
 |-  B = ( Base ` G )
2 cygzn.n 
 |-  N = if ( B e. Fin , ( # ` B ) , 0 )
3 cygzn.y 
 |-  Y = ( Z/nZ ` N )
4 eqid 
 |-  ( .g ` G ) = ( .g ` G )
5 eqid 
 |-  { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } = { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B }
6 1 4 5 iscyg2 
 |-  ( G e. CycGrp <-> ( G e. Grp /\ { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) ) )
7 6 simprbi 
 |-  ( G e. CycGrp -> { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) )
8 n0 
 |-  ( { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } =/= (/) <-> E. g g e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
9 7 8 sylib 
 |-  ( G e. CycGrp -> E. g g e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
10 eqid 
 |-  ( ZRHom ` Y ) = ( ZRHom ` Y )
11 simpl 
 |-  ( ( G e. CycGrp /\ g e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> G e. CycGrp )
12 simpr 
 |-  ( ( G e. CycGrp /\ g e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> g e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } )
13 eqid 
 |-  ran ( m e. ZZ |-> <. ( ( ZRHom ` Y ) ` m ) , ( m ( .g ` G ) g ) >. ) = ran ( m e. ZZ |-> <. ( ( ZRHom ` Y ) ` m ) , ( m ( .g ` G ) g ) >. )
14 1 2 3 4 10 5 11 12 13 cygznlem3 
 |-  ( ( G e. CycGrp /\ g e. { x e. B | ran ( n e. ZZ |-> ( n ( .g ` G ) x ) ) = B } ) -> G ~=g Y )
15 9 14 exlimddv 
 |-  ( G e. CycGrp -> G ~=g Y )