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 = ℤ/Nℤ
Assertion zncyg ⊢ N ∈ ℕ 0 → Y ∈ CycGrp

Proof

Step Hyp Ref Expression
1 zncyg.y ⊢ Y = ℤ/Nℤ
2 1 zncrng ⊢ N ∈ ℕ 0 → Y ∈ CRing
3 crngring ⊢ Y ∈ CRing → Y ∈ Ring
4 2 3 syl ⊢ N ∈ ℕ 0 → Y ∈ Ring
5 ringgrp ⊢ Y ∈ Ring → Y ∈ Grp
6 4 5 syl ⊢ N ∈ ℕ 0 → Y ∈ Grp
7 eqid ⊢ Base Y = Base Y
8 eqid ⊢ 1 Y = 1 Y
9 7 8 ringidcl ⊢ Y ∈ Ring → 1 Y ∈ Base Y
10 4 9 syl ⊢ N ∈ ℕ 0 → 1 Y ∈ Base Y
11 eqid ⊢ ℤRHom ⁡ Y = ℤRHom ⁡ Y
12 eqid ⊢ ⋅ Y = ⋅ Y
13 11 12 8 zrhval2 ⊢ Y ∈ Ring → ℤRHom ⁡ Y = n ∈ ℤ ⟼ n ⋅ Y 1 Y
14 4 13 syl ⊢ N ∈ ℕ 0 → ℤRHom ⁡ Y = n ∈ ℤ ⟼ n ⋅ Y 1 Y
15 14 rneqd ⊢ N ∈ ℕ 0 → ran ⁡ ℤRHom ⁡ Y = ran ⁡ n ∈ ℤ ⟼ n ⋅ Y 1 Y
16 1 7 11 znzrhfo ⊢ N ∈ ℕ 0 → ℤRHom ⁡ Y : ℤ ⟶ onto Base Y
17 forn ⊢ ℤRHom ⁡ Y : ℤ ⟶ onto Base Y → ran ⁡ ℤRHom ⁡ Y = Base Y
18 16 17 syl ⊢ N ∈ ℕ 0 → ran ⁡ ℤRHom ⁡ Y = Base Y
19 15 18 eqtr3d ⊢ N ∈ ℕ 0 → ran ⁡ n ∈ ℤ ⟼ n ⋅ Y 1 Y = Base Y
20 oveq2 ⊢ x = 1 Y → n ⋅ Y x = n ⋅ Y 1 Y
21 20 mpteq2dv ⊢ x = 1 Y → n ∈ ℤ ⟼ n ⋅ Y x = n ∈ ℤ ⟼ n ⋅ Y 1 Y
22 21 rneqd ⊢ x = 1 Y → ran ⁡ n ∈ ℤ ⟼ n ⋅ Y x = ran ⁡ n ∈ ℤ ⟼ n ⋅ Y 1 Y
23 22 eqeq1d ⊢ x = 1 Y → ran ⁡ n ∈ ℤ ⟼ n ⋅ Y x = Base Y ↔ ran ⁡ n ∈ ℤ ⟼ n ⋅ Y 1 Y = Base Y
24 23 rspcev ⊢ 1 Y ∈ Base Y ∧ ran ⁡ n ∈ ℤ ⟼ n ⋅ Y 1 Y = Base Y → ∃ x ∈ Base Y ran ⁡ n ∈ ℤ ⟼ n ⋅ Y x = Base Y
25 10 19 24 syl2anc ⊢ N ∈ ℕ 0 → ∃ x ∈ Base Y ran ⁡ n ∈ ℤ ⟼ n ⋅ Y x = Base Y
26 7 12 iscyg ⊢ Y ∈ CycGrp ↔ Y ∈ Grp ∧ ∃ x ∈ Base Y ran ⁡ n ∈ ℤ ⟼ n ⋅ Y x = Base Y
27 6 25 26 sylanbrc ⊢ N ∈ ℕ 0 → Y ∈ CycGrp