This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 )