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 )