Theorem znchr

Description: Cyclic rings are defined by their characteristic. (Contributed by Stefan O'Rear, 6-Sep-2015)

	Ref	Expression
Hypothesis	znchr.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
Assertion	znchr	$$⊢N\in {\mathbb{N}}_0\to \mathrm{chr}\left(Y\right)=N$$

Proof

Step	Hyp	Ref	Expression
1		znchr.y	$$⊢Y=\mathbb{Z}/N\mathbb{Z}$$
2	1	zncrng	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{CRing}$$
3		crngring	$$⊢Y\in \mathrm{CRing}\to Y\in \mathrm{Ring}$$
4	2 3	syl	$$⊢N\in {\mathbb{N}}_0\to Y\in \mathrm{Ring}$$
5		nn0z	$$⊢x\in {\mathbb{N}}_0\to x\in \mathbb{Z}$$
6		eqid	$$⊢\mathrm{chr}\left(Y\right)=\mathrm{chr}\left(Y\right)$$
7		eqid	$$⊢\mathrm{\mathbb{Z}RHom}\left(Y\right)=\mathrm{\mathbb{Z}RHom}\left(Y\right)$$
8		eqid	$$⊢0_Y=0_Y$$
9	6 7 8	chrdvds	$$⊢\left(Y\in \mathrm{Ring}\wedge x\in \mathbb{Z}\right)\to \left(\mathrm{chr}\left(Y\right)\parallel x\leftrightarrow \mathrm{\mathbb{Z}RHom}\left(Y\right)\left(x\right)=0_Y\right)$$
10	4 5 9	syl2an	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in {\mathbb{N}}_0\right)\to \left(\mathrm{chr}\left(Y\right)\parallel x\leftrightarrow \mathrm{\mathbb{Z}RHom}\left(Y\right)\left(x\right)=0_Y\right)$$
11	1 7 8	zndvds0	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in \mathbb{Z}\right)\to \left(\mathrm{\mathbb{Z}RHom}\left(Y\right)\left(x\right)=0_Y\leftrightarrow N\parallel x\right)$$
12	5 11	sylan2	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in {\mathbb{N}}_0\right)\to \left(\mathrm{\mathbb{Z}RHom}\left(Y\right)\left(x\right)=0_Y\leftrightarrow N\parallel x\right)$$
13	10 12	bitrd	$$⊢\left(N\in {\mathbb{N}}_0\wedge x\in {\mathbb{N}}_0\right)\to \left(\mathrm{chr}\left(Y\right)\parallel x\leftrightarrow N\parallel x\right)$$
14	13	ralrimiva	$$⊢N\in {\mathbb{N}}_0\to \forall x\in {\mathbb{N}}_0\left(\mathrm{chr}\left(Y\right)\parallel x\leftrightarrow N\parallel x\right)$$
15	6	chrcl	$$⊢Y\in \mathrm{Ring}\to \mathrm{chr}\left(Y\right)\in {\mathbb{N}}_0$$
16	4 15	syl	$$⊢N\in {\mathbb{N}}_0\to \mathrm{chr}\left(Y\right)\in {\mathbb{N}}_0$$
17		dvdsext	$$⊢\left(\mathrm{chr}\left(Y\right)\in {\mathbb{N}}_0\wedge N\in {\mathbb{N}}_0\right)\to \left(\mathrm{chr}\left(Y\right)=N\leftrightarrow \forall x\in {\mathbb{N}}_0\left(\mathrm{chr}\left(Y\right)\parallel x\leftrightarrow N\parallel x\right)\right)$$
18	16 17	mpancom	$$⊢N\in {\mathbb{N}}_0\to \left(\mathrm{chr}\left(Y\right)=N\leftrightarrow \forall x\in {\mathbb{N}}_0\left(\mathrm{chr}\left(Y\right)\parallel x\leftrightarrow N\parallel x\right)\right)$$
19	14 18	mpbird	$$⊢N\in {\mathbb{N}}_0\to \mathrm{chr}\left(Y\right)=N$$