Theorem zrhf1ker

Description: The kernel of the homomorphism from the integers to a ring, if it is injective. (Contributed by Thierry Arnoux, 26-Oct-2017) (Revised by Thierry Arnoux, 23-May-2023)

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

Proof

Step	Hyp	Ref	Expression
1		zrhker.0	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		zrhker.1	⊢ 𝐿 = ( ℤRHom ‘ 𝑅 )
3		zrhker.2	⊢ 0 = ( 0g ‘ 𝑅 )
4	2	zrhrhm	⊢ ( 𝑅 ∈ Ring → 𝐿 ∈ ( ℤring RingHom 𝑅 ) )
5		rhmghm	⊢ ( 𝐿 ∈ ( ℤring RingHom 𝑅 ) → 𝐿 ∈ ( ℤring GrpHom 𝑅 ) )
6		zringbas	⊢ ℤ = ( Base ‘ ℤring )
7		zring0	⊢ 0 = ( 0g ‘ ℤring )
8	6 1 7 3	kerf1ghm	⊢ ( 𝐿 ∈ ( ℤring GrpHom 𝑅 ) → ( 𝐿 : ℤ –1-1→ 𝐵 ↔ ( ◡ 𝐿 “ { 0 } ) = { 0 } ) )
9	4 5 8	3syl	⊢ ( 𝑅 ∈ Ring → ( 𝐿 : ℤ –1-1→ 𝐵 ↔ ( ◡ 𝐿 “ { 0 } ) = { 0 } ) )