Metamath Proof Explorer

Theorem cygznlem3

Description: A cyclic group with n elements is isomorphic to ZZ / n 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 )
cygzn.m 
|- .x. = ( .g ` G )
cygzn.l 
|- L = ( ZRHom ` Y )
cygzn.e 
|- E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
cygzn.g 
|- ( ph -> G e. CycGrp )
cygzn.x 
|- ( ph -> X e. E )
cygzn.f 
|- F = ran ( m e. ZZ |-> <. ( L ` m ) , ( m .x. X ) >. )
Assertion cygznlem3 
|- ( ph -> 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 cygzn.m 
 |-  .x. = ( .g ` G )
5 cygzn.l 
 |-  L = ( ZRHom ` Y )
6 cygzn.e 
 |-  E = { x e. B | ran ( n e. ZZ |-> ( n .x. x ) ) = B }
7 cygzn.g 
 |-  ( ph -> G e. CycGrp )
8 cygzn.x 
 |-  ( ph -> X e. E )
9 cygzn.f 
 |-  F = ran ( m e. ZZ |-> <. ( L ` m ) , ( m .x. X ) >. )
10 eqid 
 |-  ( Base ` Y ) = ( Base ` Y )
11 eqid 
 |-  ( +g ` Y ) = ( +g ` Y )
12 eqid 
 |-  ( +g ` G ) = ( +g ` G )
13 hashcl 
 |-  ( B e. Fin -> ( # ` B ) e. NN0 )
14 13 adantl 
 |-  ( ( ph /\ B e. Fin ) -> ( # ` B ) e. NN0 )
15 0nn0 
 |-  0 e. NN0
16 15 a1i 
 |-  ( ( ph /\ -. B e. Fin ) -> 0 e. NN0 )
17 14 16 ifclda 
 |-  ( ph -> if ( B e. Fin , ( # ` B ) , 0 ) e. NN0 )
18 2 17 eqeltrid 
 |-  ( ph -> N e. NN0 )
19 3 zncrng 
 |-  ( N e. NN0 -> Y e. CRing )
20 crngring 
 |-  ( Y e. CRing -> Y e. Ring )
21 ringgrp 
 |-  ( Y e. Ring -> Y e. Grp )
22 18 19 20 21 4syl 
 |-  ( ph -> Y e. Grp )
23 cyggrp 
 |-  ( G e. CycGrp -> G e. Grp )
24 7 23 syl 
 |-  ( ph -> G e. Grp )
25 1 2 3 4 5 6 7 8 9 cygznlem2a 
 |-  ( ph -> F : ( Base ` Y ) --> B )
26 3 10 5 znzrhfo 
 |-  ( N e. NN0 -> L : ZZ -onto-> ( Base ` Y ) )
27 18 26 syl 
 |-  ( ph -> L : ZZ -onto-> ( Base ` Y ) )
28 foelrn 
 |-  ( ( L : ZZ -onto-> ( Base ` Y ) /\ a e. ( Base ` Y ) ) -> E. i e. ZZ a = ( L ` i ) )
29 27 28 sylan 
 |-  ( ( ph /\ a e. ( Base ` Y ) ) -> E. i e. ZZ a = ( L ` i ) )
30 foelrn 
 |-  ( ( L : ZZ -onto-> ( Base ` Y ) /\ b e. ( Base ` Y ) ) -> E. j e. ZZ b = ( L ` j ) )
31 27 30 sylan 
 |-  ( ( ph /\ b e. ( Base ` Y ) ) -> E. j e. ZZ b = ( L ` j ) )
32 29 31 anim12dan 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> ( E. i e. ZZ a = ( L ` i ) /\ E. j e. ZZ b = ( L ` j ) ) )
33 reeanv 
 |-  ( E. i e. ZZ E. j e. ZZ ( a = ( L ` i ) /\ b = ( L ` j ) ) <-> ( E. i e. ZZ a = ( L ` i ) /\ E. j e. ZZ b = ( L ` j ) ) )
34 24 adantr 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> G e. Grp )
35 simprl 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> i e. ZZ )
36 simprr 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> j e. ZZ )
37 1 4 6 iscyggen 
 |-  ( X e. E <-> ( X e. B /\ ran ( n e. ZZ |-> ( n .x. X ) ) = B ) )
38 37 simplbi 
 |-  ( X e. E -> X e. B )
39 8 38 syl 
 |-  ( ph -> X e. B )
40 39 adantr 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> X e. B )
41 1 4 12 mulgdir 
 |-  ( ( G e. Grp /\ ( i e. ZZ /\ j e. ZZ /\ X e. B ) ) -> ( ( i + j ) .x. X ) = ( ( i .x. X ) ( +g ` G ) ( j .x. X ) ) )
42 34 35 36 40 41 syl13anc 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( i + j ) .x. X ) = ( ( i .x. X ) ( +g ` G ) ( j .x. X ) ) )
43 18 19 syl 
 |-  ( ph -> Y e. CRing )
44 5 zrhrhm 
 |-  ( Y e. Ring -> L e. ( ZZring RingHom Y ) )
45 rhmghm 
 |-  ( L e. ( ZZring RingHom Y ) -> L e. ( ZZring GrpHom Y ) )
46 43 20 44 45 4syl 
 |-  ( ph -> L e. ( ZZring GrpHom Y ) )
47 46 adantr 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> L e. ( ZZring GrpHom Y ) )
48 zringbas 
 |-  ZZ = ( Base ` ZZring )
49 zringplusg 
 |-  + = ( +g ` ZZring )
50 48 49 11 ghmlin 
 |-  ( ( L e. ( ZZring GrpHom Y ) /\ i e. ZZ /\ j e. ZZ ) -> ( L ` ( i + j ) ) = ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) )
51 47 35 36 50 syl3anc 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( L ` ( i + j ) ) = ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) )
52 51 fveq2d 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( F ` ( L ` ( i + j ) ) ) = ( F ` ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) ) )
53 zaddcl 
 |-  ( ( i e. ZZ /\ j e. ZZ ) -> ( i + j ) e. ZZ )
54 1 2 3 4 5 6 7 8 9 cygznlem2 
 |-  ( ( ph /\ ( i + j ) e. ZZ ) -> ( F ` ( L ` ( i + j ) ) ) = ( ( i + j ) .x. X ) )
55 53 54 sylan2 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( F ` ( L ` ( i + j ) ) ) = ( ( i + j ) .x. X ) )
56 52 55 eqtr3d 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( F ` ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) ) = ( ( i + j ) .x. X ) )
57 1 2 3 4 5 6 7 8 9 cygznlem2 
 |-  ( ( ph /\ i e. ZZ ) -> ( F ` ( L ` i ) ) = ( i .x. X ) )
58 57 adantrr 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( F ` ( L ` i ) ) = ( i .x. X ) )
59 1 2 3 4 5 6 7 8 9 cygznlem2 
 |-  ( ( ph /\ j e. ZZ ) -> ( F ` ( L ` j ) ) = ( j .x. X ) )
60 59 adantrl 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( F ` ( L ` j ) ) = ( j .x. X ) )
61 58 60 oveq12d 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( F ` ( L ` i ) ) ( +g ` G ) ( F ` ( L ` j ) ) ) = ( ( i .x. X ) ( +g ` G ) ( j .x. X ) ) )
62 42 56 61 3eqtr4d 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( F ` ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) ) = ( ( F ` ( L ` i ) ) ( +g ` G ) ( F ` ( L ` j ) ) ) )
63 oveq12 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( a ( +g ` Y ) b ) = ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) )
64 63 fveq2d 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( F ` ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) ) )
65 fveq2 
 |-  ( a = ( L ` i ) -> ( F ` a ) = ( F ` ( L ` i ) ) )
66 fveq2 
 |-  ( b = ( L ` j ) -> ( F ` b ) = ( F ` ( L ` j ) ) )
67 65 66 oveqan12d 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( ( F ` a ) ( +g ` G ) ( F ` b ) ) = ( ( F ` ( L ` i ) ) ( +g ` G ) ( F ` ( L ` j ) ) ) )
68 64 67 eqeq12d 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) <-> ( F ` ( ( L ` i ) ( +g ` Y ) ( L ` j ) ) ) = ( ( F ` ( L ` i ) ) ( +g ` G ) ( F ` ( L ` j ) ) ) ) )
69 62 68 syl5ibrcom 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) ) )
70 69 rexlimdvva 
 |-  ( ph -> ( E. i e. ZZ E. j e. ZZ ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) ) )
71 33 70 syl5bir 
 |-  ( ph -> ( ( E. i e. ZZ a = ( L ` i ) /\ E. j e. ZZ b = ( L ` j ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) ) )
72 71 imp 
 |-  ( ( ph /\ ( E. i e. ZZ a = ( L ` i ) /\ E. j e. ZZ b = ( L ` j ) ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) )
73 32 72 syldan 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> ( F ` ( a ( +g ` Y ) b ) ) = ( ( F ` a ) ( +g ` G ) ( F ` b ) ) )
74 10 1 11 12 22 24 25 73 isghmd 
 |-  ( ph -> F e. ( Y GrpHom G ) )
75 58 60 eqeq12d 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( F ` ( L ` i ) ) = ( F ` ( L ` j ) ) <-> ( i .x. X ) = ( j .x. X ) ) )
76 1 2 3 4 5 6 7 8 cygznlem1 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( L ` i ) = ( L ` j ) <-> ( i .x. X ) = ( j .x. X ) ) )
77 75 76 bitr4d 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( F ` ( L ` i ) ) = ( F ` ( L ` j ) ) <-> ( L ` i ) = ( L ` j ) ) )
78 77 biimpd 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( F ` ( L ` i ) ) = ( F ` ( L ` j ) ) -> ( L ` i ) = ( L ` j ) ) )
79 65 66 eqeqan12d 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( ( F ` a ) = ( F ` b ) <-> ( F ` ( L ` i ) ) = ( F ` ( L ` j ) ) ) )
80 eqeq12 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( a = b <-> ( L ` i ) = ( L ` j ) ) )
81 79 80 imbi12d 
 |-  ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( ( ( F ` a ) = ( F ` b ) -> a = b ) <-> ( ( F ` ( L ` i ) ) = ( F ` ( L ` j ) ) -> ( L ` i ) = ( L ` j ) ) ) )
82 78 81 syl5ibrcom 
 |-  ( ( ph /\ ( i e. ZZ /\ j e. ZZ ) ) -> ( ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
83 82 rexlimdvva 
 |-  ( ph -> ( E. i e. ZZ E. j e. ZZ ( a = ( L ` i ) /\ b = ( L ` j ) ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
84 33 83 syl5bir 
 |-  ( ph -> ( ( E. i e. ZZ a = ( L ` i ) /\ E. j e. ZZ b = ( L ` j ) ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
85 84 imp 
 |-  ( ( ph /\ ( E. i e. ZZ a = ( L ` i ) /\ E. j e. ZZ b = ( L ` j ) ) ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) )
86 32 85 syldan 
 |-  ( ( ph /\ ( a e. ( Base ` Y ) /\ b e. ( Base ` Y ) ) ) -> ( ( F ` a ) = ( F ` b ) -> a = b ) )
87 86 ralrimivva 
 |-  ( ph -> A. a e. ( Base ` Y ) A. b e. ( Base ` Y ) ( ( F ` a ) = ( F ` b ) -> a = b ) )
88 dff13 
 |-  ( F : ( Base ` Y ) -1-1-> B <-> ( F : ( Base ` Y ) --> B /\ A. a e. ( Base ` Y ) A. b e. ( Base ` Y ) ( ( F ` a ) = ( F ` b ) -> a = b ) ) )
89 25 87 88 sylanbrc 
 |-  ( ph -> F : ( Base ` Y ) -1-1-> B )
90 1 4 6 iscyggen2 
 |-  ( G e. Grp -> ( X e. E <-> ( X e. B /\ A. z e. B E. n e. ZZ z = ( n .x. X ) ) ) )
91 24 90 syl 
 |-  ( ph -> ( X e. E <-> ( X e. B /\ A. z e. B E. n e. ZZ z = ( n .x. X ) ) ) )
92 8 91 mpbid 
 |-  ( ph -> ( X e. B /\ A. z e. B E. n e. ZZ z = ( n .x. X ) ) )
93 92 simprd 
 |-  ( ph -> A. z e. B E. n e. ZZ z = ( n .x. X ) )
94 oveq1 
 |-  ( n = j -> ( n .x. X ) = ( j .x. X ) )
95 94 eqeq2d 
 |-  ( n = j -> ( z = ( n .x. X ) <-> z = ( j .x. X ) ) )
96 95 cbvrexvw 
 |-  ( E. n e. ZZ z = ( n .x. X ) <-> E. j e. ZZ z = ( j .x. X ) )
97 27 adantr 
 |-  ( ( ph /\ z e. B ) -> L : ZZ -onto-> ( Base ` Y ) )
98 fof 
 |-  ( L : ZZ -onto-> ( Base ` Y ) -> L : ZZ --> ( Base ` Y ) )
99 97 98 syl 
 |-  ( ( ph /\ z e. B ) -> L : ZZ --> ( Base ` Y ) )
100 99 ffvelrnda 
 |-  ( ( ( ph /\ z e. B ) /\ j e. ZZ ) -> ( L ` j ) e. ( Base ` Y ) )
101 59 adantlr 
 |-  ( ( ( ph /\ z e. B ) /\ j e. ZZ ) -> ( F ` ( L ` j ) ) = ( j .x. X ) )
102 101 eqcomd 
 |-  ( ( ( ph /\ z e. B ) /\ j e. ZZ ) -> ( j .x. X ) = ( F ` ( L ` j ) ) )
103 fveq2 
 |-  ( a = ( L ` j ) -> ( F ` a ) = ( F ` ( L ` j ) ) )
104 103 rspceeqv 
 |-  ( ( ( L ` j ) e. ( Base ` Y ) /\ ( j .x. X ) = ( F ` ( L ` j ) ) ) -> E. a e. ( Base ` Y ) ( j .x. X ) = ( F ` a ) )
105 100 102 104 syl2anc 
 |-  ( ( ( ph /\ z e. B ) /\ j e. ZZ ) -> E. a e. ( Base ` Y ) ( j .x. X ) = ( F ` a ) )
106 eqeq1 
 |-  ( z = ( j .x. X ) -> ( z = ( F ` a ) <-> ( j .x. X ) = ( F ` a ) ) )
107 106 rexbidv 
 |-  ( z = ( j .x. X ) -> ( E. a e. ( Base ` Y ) z = ( F ` a ) <-> E. a e. ( Base ` Y ) ( j .x. X ) = ( F ` a ) ) )
108 105 107 syl5ibrcom 
 |-  ( ( ( ph /\ z e. B ) /\ j e. ZZ ) -> ( z = ( j .x. X ) -> E. a e. ( Base ` Y ) z = ( F ` a ) ) )
109 108 rexlimdva 
 |-  ( ( ph /\ z e. B ) -> ( E. j e. ZZ z = ( j .x. X ) -> E. a e. ( Base ` Y ) z = ( F ` a ) ) )
110 96 109 syl5bi 
 |-  ( ( ph /\ z e. B ) -> ( E. n e. ZZ z = ( n .x. X ) -> E. a e. ( Base ` Y ) z = ( F ` a ) ) )
111 110 ralimdva 
 |-  ( ph -> ( A. z e. B E. n e. ZZ z = ( n .x. X ) -> A. z e. B E. a e. ( Base ` Y ) z = ( F ` a ) ) )
112 93 111 mpd 
 |-  ( ph -> A. z e. B E. a e. ( Base ` Y ) z = ( F ` a ) )
113 dffo3 
 |-  ( F : ( Base ` Y ) -onto-> B <-> ( F : ( Base ` Y ) --> B /\ A. z e. B E. a e. ( Base ` Y ) z = ( F ` a ) ) )
114 25 112 113 sylanbrc 
 |-  ( ph -> F : ( Base ` Y ) -onto-> B )
115 df-f1o 
 |-  ( F : ( Base ` Y ) -1-1-onto-> B <-> ( F : ( Base ` Y ) -1-1-> B /\ F : ( Base ` Y ) -onto-> B ) )
116 89 114 115 sylanbrc 
 |-  ( ph -> F : ( Base ` Y ) -1-1-onto-> B )
117 10 1 isgim 
 |-  ( F e. ( Y GrpIso G ) <-> ( F e. ( Y GrpHom G ) /\ F : ( Base ` Y ) -1-1-onto-> B ) )
118 74 116 117 sylanbrc 
 |-  ( ph -> F e. ( Y GrpIso G ) )
119 brgici 
 |-  ( F e. ( Y GrpIso G ) -> Y ~=g G )
120 gicsym 
 |-  ( Y ~=g G -> G ~=g Y )
121 118 119 120 3syl 
 |-  ( ph -> G ~=g Y )