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 )