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	|- B = ( Base ` R )
	rhmkerinj.c	|- C = ( Base ` S )
	rhmkerinj.0	|- .0. = ( 0g ` R )
	rhmkerinj.z	|- Z = ( 0g ` S )
Assertion	rhmkerinj	|- ( F e. ( R RingHom S ) -> ( F : B -1-1-> C <-> ( `' F " { Z } ) = { .0. } ) )

Proof

Step	Hyp	Ref	Expression
1		rhmkerinj.b	|- B = ( Base ` R )
2		rhmkerinj.c	|- C = ( Base ` S )
3		rhmkerinj.0	|- .0. = ( 0g ` R )
4		rhmkerinj.z	|- Z = ( 0g ` S )
5		rhmghm	|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
6	1 2 3 4	kerf1ghm	|- ( F e. ( R GrpHom S ) -> ( F : B -1-1-> C <-> ( `' F " { Z } ) = { .0. } ) )
7	5 6	syl	|- ( F e. ( R RingHom S ) -> ( F : B -1-1-> C <-> ( `' F " { Z } ) = { .0. } ) )