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 \in ℕ_{0} \to Y \in CycGrp$

Proof

Step	Hyp	Ref	Expression
1		zncyg.y	$⊢ Y = ℤ / N ℤ$
2	1	zncrng	$⊢ N \in ℕ_{0} \to Y \in CRing$
3		crngring	$⊢ Y \in CRing \to Y \in Ring$
4	2 3	syl	$⊢ N \in ℕ_{0} \to Y \in Ring$
5		ringgrp	$⊢ Y \in Ring \to Y \in Grp$
6	4 5	syl	$⊢ N \in ℕ_{0} \to Y \in Grp$
7		eqid	$⊢ {Base}_{Y} = {Base}_{Y}$
8		eqid	$⊢ 1_{Y} = 1_{Y}$
9	7 8	ringidcl	$⊢ Y \in Ring \to 1_{Y} \in {Base}_{Y}$
10	4 9	syl	$⊢ N \in ℕ_{0} \to 1_{Y} \in {Base}_{Y}$
11		eqid	$⊢ ℤRHom (Y) = ℤRHom (Y)$
12		eqid	$⊢ \cdot_{Y} = \cdot_{Y}$
13	11 12 8	zrhval2	$⊢ Y \in Ring \to ℤRHom (Y) = (n \in ℤ ⟼ n \cdot_{Y} 1_{Y})$
14	4 13	syl	$⊢ N \in ℕ_{0} \to ℤRHom (Y) = (n \in ℤ ⟼ n \cdot_{Y} 1_{Y})$
15	14	rneqd	$⊢ N \in ℕ_{0} \to ran ℤRHom (Y) = ran (n \in ℤ ⟼ n \cdot_{Y} 1_{Y})$
16	1 7 11	znzrhfo	$⊢ N \in ℕ_{0} \to ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y}$
17		forn	$⊢ ℤRHom (Y) : ℤ \underset{onto}{⟶} {Base}_{Y} \to ran ℤRHom (Y) = {Base}_{Y}$
18	16 17	syl	$⊢ N \in ℕ_{0} \to ran ℤRHom (Y) = {Base}_{Y}$
19	15 18	eqtr3d	$⊢ N \in ℕ_{0} \to ran (n \in ℤ ⟼ n \cdot_{Y} 1_{Y}) = {Base}_{Y}$
20		oveq2	$⊢ x = 1_{Y} \to n \cdot_{Y} x = n \cdot_{Y} 1_{Y}$
21	20	mpteq2dv	$⊢ x = 1_{Y} \to (n \in ℤ ⟼ n \cdot_{Y} x) = (n \in ℤ ⟼ n \cdot_{Y} 1_{Y})$
22	21	rneqd	$⊢ x = 1_{Y} \to ran (n \in ℤ ⟼ n \cdot_{Y} x) = ran (n \in ℤ ⟼ n \cdot_{Y} 1_{Y})$
23	22	eqeq1d	$⊢ x = 1_{Y} \to (ran (n \in ℤ ⟼ n \cdot_{Y} x) = {Base}_{Y} \leftrightarrow ran (n \in ℤ ⟼ n \cdot_{Y} 1_{Y}) = {Base}_{Y})$
24	23	rspcev	$⊢ (1_{Y} \in {Base}_{Y} \land ran (n \in ℤ ⟼ n \cdot_{Y} 1_{Y}) = {Base}_{Y}) \to \exists x \in {Base}_{Y} ran (n \in ℤ ⟼ n \cdot_{Y} x) = {Base}_{Y}$
25	10 19 24	syl2anc	$⊢ N \in ℕ_{0} \to \exists x \in {Base}_{Y} ran (n \in ℤ ⟼ n \cdot_{Y} x) = {Base}_{Y}$
26	7 12	iscyg	$⊢ Y \in CycGrp \leftrightarrow (Y \in Grp \land \exists x \in {Base}_{Y} ran (n \in ℤ ⟼ n \cdot_{Y} x) = {Base}_{Y})$
27	6 25 26	sylanbrc	$⊢ N \in ℕ_{0} \to Y \in CycGrp$

Metamath Proof Explorer

Theorem zncyg

Proof