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. )