This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ⊢ 𝑌 = ( ℤ/nℤ ‘ 𝑁 )
Assertion zncyg ( 𝑁 ∈ ℕ0 → 𝑌 ∈ CycGrp )

Proof

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