Theorem rhmkerinj

Description: A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011) (Revised by AV, 24-Jul-2026)

	Ref	Expression
Hypotheses	rhmkerinj.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
	rhmkerinj.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
	rhmkerinj.0	⊢ 0 = ( 0g ‘ 𝑅 )
	rhmkerinj.z	⊢ 𝑍 = ( 0g ‘ 𝑆 )
Assertion	rhmkerinj	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1→ 𝐶 ↔ ( ◡ 𝐹 “ { 𝑍 } ) = { 0 } ) )

Proof

Step	Hyp	Ref	Expression
1		rhmkerinj.b	⊢ 𝐵 = ( Base ‘ 𝑅 )
2		rhmkerinj.c	⊢ 𝐶 = ( Base ‘ 𝑆 )
3		rhmkerinj.0	⊢ 0 = ( 0g ‘ 𝑅 )
4		rhmkerinj.z	⊢ 𝑍 = ( 0g ‘ 𝑆 )
5		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
6	1 2 3 4	kerf1ghm	⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1→ 𝐶 ↔ ( ◡ 𝐹 “ { 𝑍 } ) = { 0 } ) )
7	5 6	syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 : 𝐵 –1-1→ 𝐶 ↔ ( ◡ 𝐹 “ { 𝑍 } ) = { 0 } ) )