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 𝐶 = ( 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 eqtr3id ( 𝑅 ∈ Ring → ( 𝐶 ( .g𝑅 ) ( 1r𝑅 ) ) = 0 )
18 9 17 eqtrd ( 𝑅 ∈ Ring → ( 𝐿𝐶 ) = 0 )