Theorem zrhchr

Description: The kernel of the homomorphism from the integers to a ring is injective if and only if the ring has characteristic 0 . (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	zrhker.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
	zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	zrhchr	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ 𝐿 : ℤ –1-1→ 𝐵 ) )

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3		zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
4		eqid	⊢ ( .g ‘ 𝑅 ) = ( .g ‘ 𝑅 )
5		eqid	⊢ ( 1r ‘ 𝑅 ) = ( 1r ‘ 𝑅 )
6	2 4 5	zrhval2	⊢ ( 𝑅 ∈ Ring → 𝐿 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) )
7		f1eq1	⊢ ( 𝐿 = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) → ( 𝐿 : ℤ –1-1→ 𝐵 ↔ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) : ℤ –1-1→ 𝐵 ) )
8	6 7	syl	⊢ ( 𝑅 ∈ Ring → ( 𝐿 : ℤ –1-1→ 𝐵 ↔ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) : ℤ –1-1→ 𝐵 ) )
9		ringgrp	⊢ ( 𝑅 ∈ Ring → 𝑅 ∈ Grp )
10	1 5	ringidcl	⊢ ( 𝑅 ∈ Ring → ( 1r ‘ 𝑅 ) ∈ 𝐵 )
11		eqid	⊢ ( od ‘ 𝑅 ) = ( od ‘ 𝑅 )
12		eqid	⊢ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) = ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) )
13	1 11 4 12	odf1	⊢ ( ( 𝑅 ∈ Grp ∧ ( 1r ‘ 𝑅 ) ∈ 𝐵 ) → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 0 ↔ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) : ℤ –1-1→ 𝐵 ) )
14	9 10 13	syl2anc	⊢ ( 𝑅 ∈ Ring → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 0 ↔ ( 𝑥 ∈ ℤ ↦ ( 𝑥 ( .g ‘ 𝑅 ) ( 1r ‘ 𝑅 ) ) ) : ℤ –1-1→ 𝐵 ) )
15		eqid	⊢ ( chr ‘ 𝑅 ) = ( chr ‘ 𝑅 )
16	11 5 15	chrval	⊢ ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = ( chr ‘ 𝑅 )
17	16	eqeq1i	⊢ ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 0 ↔ ( chr ‘ 𝑅 ) = 0 )
18	17	a1i	⊢ ( 𝑅 ∈ Ring → ( ( ( od ‘ 𝑅 ) ‘ ( 1r ‘ 𝑅 ) ) = 0 ↔ ( chr ‘ 𝑅 ) = 0 ) )
19	8 14 18	3bitr2rd	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ 𝐿 : ℤ –1-1→ 𝐵 ) )