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

Metamath Proof Explorer

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 )