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 = Base G
cygzn.n ⊢ N = if B ∈ Fin B 0
cygzn.y ⊢ Y = ℤ/Nℤ
Assertion cygzn ⊢ G ∈ CycGrp → G ≃ 𝑔 Y

Proof

Step Hyp Ref Expression
1 cygzn.b ⊢ B = Base G
2 cygzn.n ⊢ N = if B ∈ Fin B 0
3 cygzn.y ⊢ Y = ℤ/Nℤ
4 eqid ⊢ ⋅ G = ⋅ G
5 eqid ⊢ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B = x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
6 1 4 5 iscyg2 ⊢ G ∈ CycGrp ↔ G ∈ Grp ∧ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅
7 6 simprbi ⊢ G ∈ CycGrp → x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅
8 n0 ⊢ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B ≠ ∅ ↔ ∃ g g ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
9 7 8 sylib ⊢ G ∈ CycGrp → ∃ g g ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
10 eqid ⊢ ℤRHom ⁡ Y = ℤRHom ⁡ Y
11 simpl ⊢ G ∈ CycGrp ∧ g ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → G ∈ CycGrp
12 simpr ⊢ G ∈ CycGrp ∧ g ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → g ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B
13 eqid ⊢ ran ⁡ m ∈ ℤ ⟼ ℤRHom ⁡ Y ⁡ m m ⋅ G g = ran ⁡ m ∈ ℤ ⟼ ℤRHom ⁡ Y ⁡ m m ⋅ G g
14 1 2 3 4 10 5 11 12 13 cygznlem3 ⊢ G ∈ CycGrp ∧ g ∈ x ∈ B | ran ⁡ n ∈ ℤ ⟼ n ⋅ G x = B → G ≃ 𝑔 Y
15 9 14 exlimddv ⊢ G ∈ CycGrp → G ≃ 𝑔 Y