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

Metamath Proof Explorer

Theorem chrid

Description: The canonical ZZ ring homomorphism applied to a ring's characteristic is zero. (Contributed by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses chrcl.c 
|- C = ( chr ` R )
chrid.l 
|- L = ( ZRHom ` R )
chrid.z 
|- .0. = ( 0g ` R )
Assertion chrid 
|- ( R e. Ring -> ( L ` C ) = .0. )

Proof

Step Hyp Ref Expression
1 chrcl.c 
 |-  C = ( chr ` R )
2 chrid.l 
 |-  L = ( ZRHom ` R )
3 chrid.z 
 |-  .0. = ( 0g ` R )
4 1 chrcl 
 |-  ( R e. Ring -> C e. NN0 )
5 4 nn0zd 
 |-  ( R e. Ring -> C e. ZZ )
6 eqid 
 |-  ( .g ` R ) = ( .g ` R )
7 eqid 
 |-  ( 1r ` R ) = ( 1r ` R )
8 2 6 7 zrhmulg 
 |-  ( ( R e. Ring /\ C e. ZZ ) -> ( L ` C ) = ( C ( .g ` R ) ( 1r ` R ) ) )
9 5 8 mpdan 
 |-  ( R e. Ring -> ( L ` C ) = ( C ( .g ` R ) ( 1r ` R ) ) )
10 eqid 
 |-  ( od ` R ) = ( od ` R )
11 10 7 1 chrval 
 |-  ( ( od ` R ) ` ( 1r ` R ) ) = C
12 11 oveq1i 
 |-  ( ( ( od ` R ) ` ( 1r ` R ) ) ( .g ` R ) ( 1r ` R ) ) = ( C ( .g ` R ) ( 1r ` R ) )
13 eqid 
 |-  ( Base ` R ) = ( Base ` R )
14 13 7 ringidcl 
 |-  ( R e. Ring -> ( 1r ` R ) e. ( Base ` R ) )
15 13 10 6 3 odid 
 |-  ( ( 1r ` R ) e. ( Base ` R ) -> ( ( ( od ` R ) ` ( 1r ` R ) ) ( .g ` R ) ( 1r ` R ) ) = .0. )
16 14 15 syl 
 |-  ( R e. Ring -> ( ( ( od ` R ) ` ( 1r ` R ) ) ( .g ` R ) ( 1r ` R ) ) = .0. )
17 12 16 eqtr3id 
 |-  ( R e. Ring -> ( C ( .g ` R ) ( 1r ` R ) ) = .0. )
18 9 17 eqtrd 
 |-  ( R e. Ring -> ( L ` C ) = .0. )