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

Metamath Proof Explorer

Theorem chrdvds

Description: The ZZ ring homomorphism is zero only at multiples of the characteristic. (Contributed by Mario Carneiro, 23-Sep-2015)

Ref Expression
Hypotheses chrcl.c ⊢ 𝐶 = ( chr ‘ 𝑅 )
chrid.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
chrid.z ⊢ 0 = ( 0g ‘ 𝑅 )
Assertion chrdvds ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ 𝑁 ↔ ( 𝐿 ‘ 𝑁 ) = 0 ) )

Proof

Step Hyp Ref Expression
1 chrcl.c ⊢ 𝐶 = ( chr ‘ 𝑅 )
2 chrid.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3 chrid.z ⊢ 0 = ( 0g ‘ 𝑅 )
4 eqid ⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
5 eqid ⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6 4 5 1 chrval ⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 𝐶
7 6 breq1i ⊢ ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ↔ 𝐶 ∥ 𝑁 )
8 ringgrp ⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
9 8 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → 𝑅 ∈ Grp )
10 eqid ⊢ ( Base ‘ 𝑅 ) = ( Base ‘ 𝑅 )
11 10 5 ringidcl ⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
12 11 adantr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) )
13 simpr ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → 𝑁 ∈ ℤ )
14 eqid ⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
15 10 4 14 3 oddvds ⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ ( Base ‘ 𝑅 ) ∧ 𝑁 ∈ ℤ ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
16 9 12 13 15 syl3anc ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
17 7 16 bitr3id ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ 𝑁 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
18 2 14 5 zrhmulg ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐿 ‘ 𝑁 ) = ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
19 18 eqeq1d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( ( 𝐿 ‘ 𝑁 ) = 0 ↔ ( 𝑁 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) = 0 ) )
20 17 19 bitr4d ⊢ ( ( 𝑅 ∈ Ring ∧ 𝑁 ∈ ℤ ) → ( 𝐶 ∥ 𝑁 ↔ ( 𝐿 ‘ 𝑁 ) = 0 ) )