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

Metamath Proof Explorer

Theorem domnchr

Description: The characteristic of a domain can only be zero or a prime. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion domnchr 
|- ( R e. Domn -> ( ( chr ` R ) = 0 \/ ( chr ` R ) e. Prime ) )

Proof

Step Hyp Ref Expression
1 df-ne 
 |-  ( ( chr ` R ) =/= 0 <-> -. ( chr ` R ) = 0 )
2 domnring 
 |-  ( R e. Domn -> R e. Ring )
3 eqid 
 |-  ( chr ` R ) = ( chr ` R )
4 3 chrcl 
 |-  ( R e. Ring -> ( chr ` R ) e. NN0 )
5 2 4 syl 
 |-  ( R e. Domn -> ( chr ` R ) e. NN0 )
6 5 adantr 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) e. NN0 )
7 simpr 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) =/= 0 )
8 eldifsn 
 |-  ( ( chr ` R ) e. ( NN0 \ { 0 } ) <-> ( ( chr ` R ) e. NN0 /\ ( chr ` R ) =/= 0 ) )
9 6 7 8 sylanbrc 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) e. ( NN0 \ { 0 } ) )
10 dfn2 
 |-  NN = ( NN0 \ { 0 } )
11 9 10 eleqtrrdi 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) e. NN )
12 domnnzr 
 |-  ( R e. Domn -> R e. NzRing )
13 nzrring 
 |-  ( R e. NzRing -> R e. Ring )
14 chrnzr 
 |-  ( R e. Ring -> ( R e. NzRing <-> ( chr ` R ) =/= 1 ) )
15 13 14 syl 
 |-  ( R e. NzRing -> ( R e. NzRing <-> ( chr ` R ) =/= 1 ) )
16 15 ibi 
 |-  ( R e. NzRing -> ( chr ` R ) =/= 1 )
17 12 16 syl 
 |-  ( R e. Domn -> ( chr ` R ) =/= 1 )
18 17 adantr 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) =/= 1 )
19 eluz2b3 
 |-  ( ( chr ` R ) e. ( ZZ>= ` 2 ) <-> ( ( chr ` R ) e. NN /\ ( chr ` R ) =/= 1 ) )
20 11 18 19 sylanbrc 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) e. ( ZZ>= ` 2 ) )
21 2 ad2antrr 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> R e. Ring )
22 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
23 22 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
24 21 23 syl 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
25 simprl 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> x e. ZZ )
26 simprr 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> y e. ZZ )
27 zringbas 
 |-  ZZ = ( Base ` ZZring )
28 zringmulr 
 |-  x. = ( .r ` ZZring )
29 eqid 
 |-  ( .r ` R ) = ( .r ` R )
30 27 28 29 rhmmul 
 |-  ( ( ( ZRHom ` R ) e. ( ZZring RingHom R ) /\ x e. ZZ /\ y e. ZZ ) -> ( ( ZRHom ` R ) ` ( x x. y ) ) = ( ( ( ZRHom ` R ) ` x ) ( .r ` R ) ( ( ZRHom ` R ) ` y ) ) )
31 24 25 26 30 syl3anc 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ZRHom ` R ) ` ( x x. y ) ) = ( ( ( ZRHom ` R ) ` x ) ( .r ` R ) ( ( ZRHom ` R ) ` y ) ) )
32 31 eqeq1d 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( ZRHom ` R ) ` ( x x. y ) ) = ( 0g ` R ) <-> ( ( ( ZRHom ` R ) ` x ) ( .r ` R ) ( ( ZRHom ` R ) ` y ) ) = ( 0g ` R ) ) )
33 simpll 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> R e. Domn )
34 eqid 
 |-  ( Base ` R ) = ( Base ` R )
35 27 34 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
36 24 35 syl 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
37 36 25 ffvelcdmd 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ZRHom ` R ) ` x ) e. ( Base ` R ) )
38 36 26 ffvelcdmd 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ZRHom ` R ) ` y ) e. ( Base ` R ) )
39 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
40 34 29 39 domneq0 
 |-  ( ( R e. Domn /\ ( ( ZRHom ` R ) ` x ) e. ( Base ` R ) /\ ( ( ZRHom ` R ) ` y ) e. ( Base ` R ) ) -> ( ( ( ( ZRHom ` R ) ` x ) ( .r ` R ) ( ( ZRHom ` R ) ` y ) ) = ( 0g ` R ) <-> ( ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) \/ ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) ) )
41 33 37 38 40 syl3anc 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( ( ZRHom ` R ) ` x ) ( .r ` R ) ( ( ZRHom ` R ) ` y ) ) = ( 0g ` R ) <-> ( ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) \/ ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) ) )
42 32 41 bitrd 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( ZRHom ` R ) ` ( x x. y ) ) = ( 0g ` R ) <-> ( ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) \/ ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) ) )
43 42 biimpd 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( ZRHom ` R ) ` ( x x. y ) ) = ( 0g ` R ) -> ( ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) \/ ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) ) )
44 zmulcl 
 |-  ( ( x e. ZZ /\ y e. ZZ ) -> ( x x. y ) e. ZZ )
45 44 adantl 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( x x. y ) e. ZZ )
46 3 22 39 chrdvds 
 |-  ( ( R e. Ring /\ ( x x. y ) e. ZZ ) -> ( ( chr ` R ) || ( x x. y ) <-> ( ( ZRHom ` R ) ` ( x x. y ) ) = ( 0g ` R ) ) )
47 21 45 46 syl2anc 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( chr ` R ) || ( x x. y ) <-> ( ( ZRHom ` R ) ` ( x x. y ) ) = ( 0g ` R ) ) )
48 3 22 39 chrdvds 
 |-  ( ( R e. Ring /\ x e. ZZ ) -> ( ( chr ` R ) || x <-> ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) ) )
49 21 25 48 syl2anc 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( chr ` R ) || x <-> ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) ) )
50 3 22 39 chrdvds 
 |-  ( ( R e. Ring /\ y e. ZZ ) -> ( ( chr ` R ) || y <-> ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) )
51 21 26 50 syl2anc 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( chr ` R ) || y <-> ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) )
52 49 51 orbi12d 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( ( chr ` R ) || x \/ ( chr ` R ) || y ) <-> ( ( ( ZRHom ` R ) ` x ) = ( 0g ` R ) \/ ( ( ZRHom ` R ) ` y ) = ( 0g ` R ) ) ) )
53 43 47 52 3imtr4d 
 |-  ( ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) /\ ( x e. ZZ /\ y e. ZZ ) ) -> ( ( chr ` R ) || ( x x. y ) -> ( ( chr ` R ) || x \/ ( chr ` R ) || y ) ) )
54 53 ralrimivva 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> A. x e. ZZ A. y e. ZZ ( ( chr ` R ) || ( x x. y ) -> ( ( chr ` R ) || x \/ ( chr ` R ) || y ) ) )
55 isprm6 
 |-  ( ( chr ` R ) e. Prime <-> ( ( chr ` R ) e. ( ZZ>= ` 2 ) /\ A. x e. ZZ A. y e. ZZ ( ( chr ` R ) || ( x x. y ) -> ( ( chr ` R ) || x \/ ( chr ` R ) || y ) ) ) )
56 20 54 55 sylanbrc 
 |-  ( ( R e. Domn /\ ( chr ` R ) =/= 0 ) -> ( chr ` R ) e. Prime )
57 56 ex 
 |-  ( R e. Domn -> ( ( chr ` R ) =/= 0 -> ( chr ` R ) e. Prime ) )
58 1 57 biimtrrid 
 |-  ( R e. Domn -> ( -. ( chr ` R ) = 0 -> ( chr ` R ) e. Prime ) )
59 58 orrd 
 |-  ( R e. Domn -> ( ( chr ` R ) = 0 \/ ( chr ` R ) e. Prime ) )