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=\mathrm{chr}\left(R\right)$$
	chrid.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
	chrid.z	$$⊢\underset{\dot{}}{0}=0_R$$
Assertion	chrid	$$⊢R\in \mathrm{Ring}\to L\left(C\right)=\underset{\dot{}}{0}$$

Proof

Step	Hyp	Ref	Expression
1		chrcl.c	$$⊢C=\mathrm{chr}\left(R\right)$$
2		chrid.l	$$⊢L=\mathrm{\mathbb{Z}RHom}\left(R\right)$$
3		chrid.z	$$⊢\underset{\dot{}}{0}=0_R$$
4	1	chrcl	$$⊢R\in \mathrm{Ring}\to C\in {\mathbb{N}}_0$$
5	4	nn0zd	$$⊢R\in \mathrm{Ring}\to C\in \mathbb{Z}$$
6		eqid	$$⊢{\cdot }_R={\cdot }_R$$
7		eqid	$$⊢1_R=1_R$$
8	2 6 7	zrhmulg	$$⊢\left(R\in \mathrm{Ring}\wedge C\in \mathbb{Z}\right)\to L\left(C\right)=C{\cdot }_R{1}_R$$
9	5 8	mpdan	$$⊢R\in \mathrm{Ring}\to L\left(C\right)=C{\cdot }_R{1}_R$$
10		eqid	$$⊢\mathrm{od}\left(R\right)=\mathrm{od}\left(R\right)$$
11	10 7 1	chrval	$$⊢\mathrm{od}\left(R\right)\left(1_R\right)=C$$
12	11	oveq1i	$$⊢\mathrm{od}\left(R\right)\left(1_R\right){\cdot }_R{1}_R=C{\cdot }_R{1}_R$$
13		eqid	$$⊢{\mathrm{Base}}_R={\mathrm{Base}}_R$$
14	13 7	ringidcl	$$⊢R\in \mathrm{Ring}\to 1_R\in {\mathrm{Base}}_R$$
15	13 10 6 3	odid	$$⊢1_R\in {\mathrm{Base}}_R\to \mathrm{od}\left(R\right)\left(1_R\right){\cdot }_R{1}_R=\underset{\dot{}}{0}$$
16	14 15	syl	$$⊢R\in \mathrm{Ring}\to \mathrm{od}\left(R\right)\left(1_R\right){\cdot }_R{1}_R=\underset{\dot{}}{0}$$
17	12 16	syl5eqr	$$⊢R\in \mathrm{Ring}\to C{\cdot }_R{1}_R=\underset{\dot{}}{0}$$
18	9 17	eqtrd	$$⊢R\in \mathrm{Ring}\to L\left(C\right)=\underset{\dot{}}{0}$$