chrid

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

Step	Hyp	Ref	Expression
1		chrcl.c	$⊢ C = chr (R)$
2		chrid.l	$⊢ L = ℤRHom (R)$
3		chrid.z	$⊢ \underset{˙}{0} = 0_{R}$
4	1	chrcl	$⊢ R \in Ring \to C \in ℕ_{0}$
5	4	nn0zd	$⊢ R \in Ring \to C \in ℤ$
6		eqid	$⊢ \cdot_{R} = \cdot_{R}$
7		eqid	$⊢ 1_{R} = 1_{R}$
8	2 6 7	zrhmulg	$⊢ (R \in Ring \land C \in ℤ) \to L (C) = C \cdot_{R} 1_{R}$
9	5 8	mpdan	$⊢ R \in Ring \to L (C) = C \cdot_{R} 1_{R}$
10		eqid	$⊢ od (R) = od (R)$
11	10 7 1	chrval	$⊢ od (R) (1_{R}) = C$
12	11	oveq1i	$⊢ od (R) (1_{R}) \cdot_{R} 1_{R} = C \cdot_{R} 1_{R}$
13		eqid	$⊢ {Base}_{R} = {Base}_{R}$
14	13 7	ringidcl	$⊢ R \in Ring \to 1_{R} \in {Base}_{R}$
15	13 10 6 3	odid	$⊢ 1_{R} \in {Base}_{R} \to od (R) (1_{R}) \cdot_{R} 1_{R} = \underset{˙}{0}$
16	14 15	syl	$⊢ R \in Ring \to od (R) (1_{R}) \cdot_{R} 1_{R} = \underset{˙}{0}$
17	12 16	eqtr3id	$⊢ R \in Ring \to C \cdot_{R} 1_{R} = \underset{˙}{0}$
18	9 17	eqtrd	$⊢ R \in Ring \to L (C) = \underset{˙}{0}$

Metamath Proof Explorer