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

Metamath Proof Explorer

Theorem zncyg

Description: The group ZZ / n ZZ is cyclic for all n (including n = 0 ). (Contributed by Mario Carneiro, 21-Apr-2016)

Ref Expression
Hypothesis zncyg.y 
|- Y = ( Z/nZ ` N )
Assertion zncyg 
|- ( N e. NN0 -> Y e. CycGrp )

Proof

Step Hyp Ref Expression
1 zncyg.y 
 |-  Y = ( Z/nZ ` N )
2 1 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
3 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
4 2 3 syl 
 |-  ( N e. NN0 -> Y e. Ring )
5 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
6 4 5 syl 
 |-  ( N e. NN0 -> Y e. Grp )
7 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
8 eqid 
 |-  ( 1r ` Y ) = ( 1r ` Y )
9 7 8 ringidcl 
 |-  ( Y e. Ring -> ( 1r ` Y ) e. ( Base ` Y ) )
10 4 9 syl 
 |-  ( N e. NN0 -> ( 1r ` Y ) e. ( Base ` Y ) )
11 eqid 
 |-  ( ZRHom ` Y ) = ( ZRHom ` Y )
12 eqid 
 |-  ( .g ` Y ) = ( .g ` Y )
13 11 12 8 zrhval2 
 |-  ( Y e. Ring -> ( ZRHom ` Y ) = ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) )
14 4 13 syl 
 |-  ( N e. NN0 -> ( ZRHom ` Y ) = ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) )
15 14 rneqd 
 |-  ( N e. NN0 -> ran ( ZRHom ` Y ) = ran ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) )
16 1 7 11 znzrhfo 
 |-  ( N e. NN0 -> ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) )
17 forn 
 |-  ( ( ZRHom ` Y ) : ZZ -onto-> ( Base ` Y ) -> ran ( ZRHom ` Y ) = ( Base ` Y ) )
18 16 17 syl 
 |-  ( N e. NN0 -> ran ( ZRHom ` Y ) = ( Base ` Y ) )
19 15 18 eqtr3d 
 |-  ( N e. NN0 -> ran ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) = ( Base ` Y ) )
20 oveq2 
 |-  ( x = ( 1r ` Y ) -> ( n ( .g ` Y ) x ) = ( n ( .g ` Y ) ( 1r ` Y ) ) )
21 20 mpteq2dv 
 |-  ( x = ( 1r ` Y ) -> ( n e. ZZ |-> ( n ( .g ` Y ) x ) ) = ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) )
22 21 rneqd 
 |-  ( x = ( 1r ` Y ) -> ran ( n e. ZZ |-> ( n ( .g ` Y ) x ) ) = ran ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) )
23 22 eqeq1d 
 |-  ( x = ( 1r ` Y ) -> ( ran ( n e. ZZ |-> ( n ( .g ` Y ) x ) ) = ( Base ` Y ) <-> ran ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) = ( Base ` Y ) ) )
24 23 rspcev 
 |-  ( ( ( 1r ` Y ) e. ( Base ` Y ) /\ ran ( n e. ZZ |-> ( n ( .g ` Y ) ( 1r ` Y ) ) ) = ( Base ` Y ) ) -> E. x e. ( Base ` Y ) ran ( n e. ZZ |-> ( n ( .g ` Y ) x ) ) = ( Base ` Y ) )
25 10 19 24 syl2anc 
 |-  ( N e. NN0 -> E. x e. ( Base ` Y ) ran ( n e. ZZ |-> ( n ( .g ` Y ) x ) ) = ( Base ` Y ) )
26 7 12 iscyg 
 |-  ( Y e. CycGrp <-> ( Y e. Grp /\ E. x e. ( Base ` Y ) ran ( n e. ZZ |-> ( n ( .g ` Y ) x ) ) = ( Base ` Y ) ) )
27 6 25 26 sylanbrc 
 |-  ( N e. NN0 -> Y e. CycGrp )