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=BaseG
cygzn.n N=ifBFinB0
cygzn.y Y=/N
Assertion cygzn GCycGrpG𝑔Y

Proof

Step Hyp Ref Expression
1 cygzn.b B=BaseG
2 cygzn.n N=ifBFinB0
3 cygzn.y Y=/N
4 eqid G=G
5 eqid xB|rannnGx=B=xB|rannnGx=B
6 1 4 5 iscyg2 GCycGrpGGrpxB|rannnGx=B
7 6 simprbi GCycGrpxB|rannnGx=B
8 n0 xB|rannnGx=BggxB|rannnGx=B
9 7 8 sylib GCycGrpggxB|rannnGx=B
10 eqid ℤRHomY=ℤRHomY
11 simpl GCycGrpgxB|rannnGx=BGCycGrp
12 simpr GCycGrpgxB|rannnGx=BgxB|rannnGx=B
13 eqid ranmℤRHomYmmGg=ranmℤRHomYmmGg
14 1 2 3 4 10 5 11 12 13 cygznlem3 GCycGrpgxB|rannnGx=BG𝑔Y
15 9 14 exlimddv GCycGrpG𝑔Y