Theorem zrhker

Description: The kernel of the homomorphism from the integers to a ring with characteristic 0. (Contributed by Thierry Arnoux, 8-Nov-2017)

	Ref	Expression
Hypotheses	zrhker.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
	zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
	zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
Assertion	zrhker	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ ( ◡ 𝐿 “ { 0 } ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3		zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
4	1 2 3	zrhchr	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ 𝐿 : ℤ –1-1→ 𝐵 ) )
5	1 2 3	zrhf1ker	⊢ ( 𝑅 ∈ Ring → ( 𝐿 : ℤ –1-1→ 𝐵 ↔ ( ◡ 𝐿 “ { 0 } ) = { 0 } ) )
6	4 5	bitrd	⊢ ( 𝑅 ∈ Ring → ( ( chr ‘ 𝑅 ) = 0 ↔ ( ◡ 𝐿 “ { 0 } ) = { 0 } ) )