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	⊢ 𝐶 = ( chr ‘ 𝑅 )
	chrid.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	chrid.z	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	chrid	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 𝐶 ) = 0 )

Proof

Step	Hyp	Ref	Expression
1		chrcl.c	⊢ 𝐶 = ( chr ‘ 𝑅 )
2		chrid.l	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3		chrid.z	⊢ 0 = ( 0g ‘ 𝑅 )
4	1	chrcl	⊢ ( 𝑅 ∈ Ring → 𝐶 ∈ ℕ0 )
5	4	nn0zd	⊢ ( 𝑅 ∈ Ring → 𝐶 ∈ ℤ )
6		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
7		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
8	2 6 7	zrhmulg	⊢ ( ( 𝑅 ∈ Ring ∧ 𝐶 ∈ ℤ ) → ( 𝐿 ‘ 𝐶 ) = ( 𝐶 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
9	5 8	mpdan	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 𝐶 ) = ( 𝐶 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
10		eqid	⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
11	10 7 1	chrval	⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 𝐶
12	11	oveq1i	⊢ ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = ( 𝐶 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) )
13		eqid	⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
14	13 7	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
15	13 10 6 3	odid	⊢ ( ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 )
16	14 15	syl	⊢ ( 𝑅 ∈ Ring → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 )
17	12 16	syl5eqr	⊢ ( 𝑅 ∈ Ring → ( 𝐶 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 )
18	9 17	eqtrd	⊢ ( 𝑅 ∈ Ring → ( 𝐿 ‘ 𝐶 ) = 0 )