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

Metamath Proof Explorer

Theorem chrnzr

Description: Nonzero rings are precisely those with characteristic not 1. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion chrnzr 
|- ( R e. Ring -> ( R e. NzRing <-> ( chr ` R ) =/= 1 ) )

Proof

Step Hyp Ref Expression
1 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
2 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
3 1 2 isnzr 
 |-  ( R e. NzRing <-> ( R e. Ring /\ ( 1r ` R ) =/= ( 0g ` R ) ) )
4 3 baib 
 |-  ( R e. Ring -> ( R e. NzRing <-> ( 1r ` R ) =/= ( 0g ` R ) ) )
5 1z 
 |-  1 e. ZZ
6 eqid 
 |-  ( chr ` R ) = ( chr ` R )
7 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
8 6 7 2 chrdvds 
 |-  ( ( R e. Ring /\ 1 e. ZZ ) -> ( ( chr ` R ) || 1 <-> ( ( ZRHom ` R ) ` 1 ) = ( 0g ` R ) ) )
9 5 8 mpan2 
 |-  ( R e. Ring -> ( ( chr ` R ) || 1 <-> ( ( ZRHom ` R ) ` 1 ) = ( 0g ` R ) ) )
10 6 chrcl 
 |-  ( R e. Ring -> ( chr ` R ) e. NN0 )
11 dvds1 
 |-  ( ( chr ` R ) e. NN0 -> ( ( chr ` R ) || 1 <-> ( chr ` R ) = 1 ) )
12 10 11 syl 
 |-  ( R e. Ring -> ( ( chr ` R ) || 1 <-> ( chr ` R ) = 1 ) )
13 7 1 zrh1 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` 1 ) = ( 1r ` R ) )
14 13 eqeq1d 
 |-  ( R e. Ring -> ( ( ( ZRHom ` R ) ` 1 ) = ( 0g ` R ) <-> ( 1r ` R ) = ( 0g ` R ) ) )
15 9 12 14 3bitr3d 
 |-  ( R e. Ring -> ( ( chr ` R ) = 1 <-> ( 1r ` R ) = ( 0g ` R ) ) )
16 15 necon3bid 
 |-  ( R e. Ring -> ( ( chr ` R ) =/= 1 <-> ( 1r ` R ) =/= ( 0g ` R ) ) )
17 4 16 bitr4d 
 |-  ( R e. Ring -> ( R e. NzRing <-> ( chr ` R ) =/= 1 ) )