Metamath Proof Explorer

Theorem chrrhm

Description: The characteristic restriction on ring homomorphisms. (Contributed by Stefan O'Rear, 6-Sep-2015)

Ref Expression
Assertion chrrhm 
|- ( F e. ( R RingHom S ) -> ( chr ` S ) || ( chr ` R ) )

Proof

Step Hyp Ref Expression
1 rhmrcl1 
 |-  ( F e. ( R RingHom S ) -> R e. Ring )
2 eqid 
 |-  ( ZRHom ` R ) = ( ZRHom ` R )
3 2 zrhrhm 
 |-  ( R e. Ring -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
4 1 3 syl 
 |-  ( F e. ( R RingHom S ) -> ( ZRHom ` R ) e. ( ZZring RingHom R ) )
5 zringbas 
 |-  ZZ = ( Base ` ZZring )
6 eqid 
 |-  ( Base ` R ) = ( Base ` R )
7 5 6 rhmf 
 |-  ( ( ZRHom ` R ) e. ( ZZring RingHom R ) -> ( ZRHom ` R ) : ZZ --> ( Base ` R ) )
8 ffn 
 |-  ( ( ZRHom ` R ) : ZZ --> ( Base ` R ) -> ( ZRHom ` R ) Fn ZZ )
9 4 7 8 3syl 
 |-  ( F e. ( R RingHom S ) -> ( ZRHom ` R ) Fn ZZ )
10 eqid 
 |-  ( chr ` R ) = ( chr ` R )
11 10 chrcl 
 |-  ( R e. Ring -> ( chr ` R ) e. NN0 )
12 nn0z 
 |-  ( ( chr ` R ) e. NN0 -> ( chr ` R ) e. ZZ )
13 1 11 12 3syl 
 |-  ( F e. ( R RingHom S ) -> ( chr ` R ) e. ZZ )
14 fvco2 
 |-  ( ( ( ZRHom ` R ) Fn ZZ /\ ( chr ` R ) e. ZZ ) -> ( ( F o. ( ZRHom ` R ) ) ` ( chr ` R ) ) = ( F ` ( ( ZRHom ` R ) ` ( chr ` R ) ) ) )
15 9 13 14 syl2anc 
 |-  ( F e. ( R RingHom S ) -> ( ( F o. ( ZRHom ` R ) ) ` ( chr ` R ) ) = ( F ` ( ( ZRHom ` R ) ` ( chr ` R ) ) ) )
16 eqid 
 |-  ( 0g ` R ) = ( 0g ` R )
17 10 2 16 chrid 
 |-  ( R e. Ring -> ( ( ZRHom ` R ) ` ( chr ` R ) ) = ( 0g ` R ) )
18 1 17 syl 
 |-  ( F e. ( R RingHom S ) -> ( ( ZRHom ` R ) ` ( chr ` R ) ) = ( 0g ` R ) )
19 18 fveq2d 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( ( ZRHom ` R ) ` ( chr ` R ) ) ) = ( F ` ( 0g ` R ) ) )
20 15 19 eqtrd 
 |-  ( F e. ( R RingHom S ) -> ( ( F o. ( ZRHom ` R ) ) ` ( chr ` R ) ) = ( F ` ( 0g ` R ) ) )
21 rhmco 
 |-  ( ( F e. ( R RingHom S ) /\ ( ZRHom ` R ) e. ( ZZring RingHom R ) ) -> ( F o. ( ZRHom ` R ) ) e. ( ZZring RingHom S ) )
22 4 21 mpdan 
 |-  ( F e. ( R RingHom S ) -> ( F o. ( ZRHom ` R ) ) e. ( ZZring RingHom S ) )
23 rhmrcl2 
 |-  ( F e. ( R RingHom S ) -> S e. Ring )
24 eqid 
 |-  ( ZRHom ` S ) = ( ZRHom ` S )
25 24 zrhrhmb 
 |-  ( S e. Ring -> ( ( F o. ( ZRHom ` R ) ) e. ( ZZring RingHom S ) <-> ( F o. ( ZRHom ` R ) ) = ( ZRHom ` S ) ) )
26 23 25 syl 
 |-  ( F e. ( R RingHom S ) -> ( ( F o. ( ZRHom ` R ) ) e. ( ZZring RingHom S ) <-> ( F o. ( ZRHom ` R ) ) = ( ZRHom ` S ) ) )
27 22 26 mpbid 
 |-  ( F e. ( R RingHom S ) -> ( F o. ( ZRHom ` R ) ) = ( ZRHom ` S ) )
28 27 fveq1d 
 |-  ( F e. ( R RingHom S ) -> ( ( F o. ( ZRHom ` R ) ) ` ( chr ` R ) ) = ( ( ZRHom ` S ) ` ( chr ` R ) ) )
29 rhmghm 
 |-  ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
30 eqid 
 |-  ( 0g ` S ) = ( 0g ` S )
31 16 30 ghmid 
 |-  ( F e. ( R GrpHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
32 29 31 syl 
 |-  ( F e. ( R RingHom S ) -> ( F ` ( 0g ` R ) ) = ( 0g ` S ) )
33 20 28 32 3eqtr3d 
 |-  ( F e. ( R RingHom S ) -> ( ( ZRHom ` S ) ` ( chr ` R ) ) = ( 0g ` S ) )
34 eqid 
 |-  ( chr ` S ) = ( chr ` S )
35 34 24 30 chrdvds 
 |-  ( ( S e. Ring /\ ( chr ` R ) e. ZZ ) -> ( ( chr ` S ) || ( chr ` R ) <-> ( ( ZRHom ` S ) ` ( chr ` R ) ) = ( 0g ` S ) ) )
36 23 13 35 syl2anc 
 |-  ( F e. ( R RingHom S ) -> ( ( chr ` S ) || ( chr ` R ) <-> ( ( ZRHom ` S ) ` ( chr ` R ) ) = ( 0g ` S ) ) )
37 33 36 mpbird 
 |-  ( F e. ( R RingHom S ) -> ( chr ` S ) || ( chr ` R ) )