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={\mathrm{Base}}_R$$
	rhmkerinj.c	$$⊢C={\mathrm{Base}}_S$$
	rhmkerinj.0	$$⊢\underset{\dot{}}{0}=0_R$$
	rhmkerinj.z	$$⊢Z=0_S$$
Assertion	rhmkerinj	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to \left(F:B\underset{1-1}{⟶}C\leftrightarrow F^{-1}\left[\left\{Z\right\}\right]=\left\{\underset{\dot{}}{0}\right\}\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmkerinj.b	$$⊢B={\mathrm{Base}}_R$$
2		rhmkerinj.c	$$⊢C={\mathrm{Base}}_S$$
3		rhmkerinj.0	$$⊢\underset{\dot{}}{0}=0_R$$
4		rhmkerinj.z	$$⊢Z=0_S$$
5		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
6	1 2 3 4	kerf1ghm	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to \left(F:B\underset{1-1}{⟶}C\leftrightarrow F^{-1}\left[\left\{Z\right\}\right]=\left\{\underset{\dot{}}{0}\right\}\right)$$
7	5 6	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to \left(F:B\underset{1-1}{⟶}C\leftrightarrow F^{-1}\left[\left\{Z\right\}\right]=\left\{\underset{\dot{}}{0}\right\}\right)$$