Theorem znchr

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

	Ref	Expression
Hypothesis	znchr.y	|- Y = ( Z/nZ ` N )
Assertion	znchr	|- ( N e. NN0 -> ( chr ` Y ) = N )

Proof

Step	Hyp	Ref	Expression
1		znchr.y	|- Y = ( Z/nZ ` N )
2	1	zncrng	|- ( N e. NN0 -> Y e. CRing )
3		crngring	|- ( Y e. CRing -> Y e. Ring )
4	2 3	syl	|- ( N e. NN0 -> Y e. Ring )
5		nn0z	|- ( x e. NN0 -> x e. ZZ )
6		eqid	|- ( chr ` Y ) = ( chr ` Y )
7		eqid	|- ( ZRHom ` Y ) = ( ZRHom ` Y )
8		eqid	|- ( 0g ` Y ) = ( 0g ` Y )
9	6 7 8	chrdvds	|- ( ( Y e. Ring /\ x e. ZZ ) -> ( ( chr ` Y ) || x <-> ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) ) )
10	4 5 9	syl2an	|- ( ( N e. NN0 /\ x e. NN0 ) -> ( ( chr ` Y ) || x <-> ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) ) )
11	1 7 8	zndvds0	|- ( ( N e. NN0 /\ x e. ZZ ) -> ( ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) <-> N || x ) )
12	5 11	sylan2	|- ( ( N e. NN0 /\ x e. NN0 ) -> ( ( ( ZRHom ` Y ) ` x ) = ( 0g ` Y ) <-> N || x ) )
13	10 12	bitrd	|- ( ( N e. NN0 /\ x e. NN0 ) -> ( ( chr ` Y ) || x <-> N || x ) )
14	13	ralrimiva	|- ( N e. NN0 -> A. x e. NN0 ( ( chr ` Y ) || x <-> N || x ) )
15	6	chrcl	|- ( Y e. Ring -> ( chr ` Y ) e. NN0 )
16	4 15	syl	|- ( N e. NN0 -> ( chr ` Y ) e. NN0 )
17		dvdsext	|- ( ( ( chr ` Y ) e. NN0 /\ N e. NN0 ) -> ( ( chr ` Y ) = N <-> A. x e. NN0 ( ( chr ` Y ) || x <-> N || x ) ) )
18	16 17	mpancom	|- ( N e. NN0 -> ( ( chr ` Y ) = N <-> A. x e. NN0 ( ( chr ` Y ) || x <-> N || x ) ) )
19	14 18	mpbird	|- ( N e. NN0 -> ( chr ` Y ) = N )