# 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}={\mathrm{Base}}_{{G}}$
cygzn.n ${⊢}{N}=if\left({B}\in \mathrm{Fin},\left|{B}\right|,0\right)$
cygzn.y ${⊢}{Y}=ℤ/{N}ℤ$
cygzn.m
cygzn.l ${⊢}{L}=\mathrm{ℤRHom}\left({Y}\right)$
cygzn.e
cygzn.g ${⊢}{\phi }\to {G}\in \mathrm{CycGrp}$
cygzn.x ${⊢}{\phi }\to {X}\in {E}$
cygzn.f
Assertion cygznlem3 ${⊢}{\phi }\to {G}{\simeq }_{𝑔}{Y}$

### Proof

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