Theorem rhm0

Description: A ring homomorphism preserves 0 . (Contributed by Jeff Madsen, 2-Jan-2011) (Revised by AV, 23-Jul-2026)

	Ref	Expression
Hypotheses	rhm0.0	$$⊢\underset{\dot{}}{0}=0_R$$
	rhm0.z	$$⊢Z=0_S$$
Assertion	rhm0	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=Z$$

Proof

Step	Hyp	Ref	Expression
1		rhm0.0	$$⊢\underset{\dot{}}{0}=0_R$$
2		rhm0.z	$$⊢Z=0_S$$
3		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
4		ghmmhm	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\in \left(R\mathrm{MndHom}S\right)$$
5	1 2	mhm0	$$⊢F\in \left(R\mathrm{MndHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=Z$$
6	3 4 5	3syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\left(\underset{\dot{}}{0}\right)=Z$$