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	|- .0. = ( 0g ` R )
	rhm0.z	|- Z = ( 0g ` S )
Assertion	rhm0	|- ( F e. ( R RingHom S ) -> ( F ` .0. ) = Z )

Proof

Step	Hyp	Ref	Expression
1		rhm0.0	|- .0. = ( 0g ` R )
2		rhm0.z	|- Z = ( 0g ` S )
3		rhmghm	|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
4		ghmmhm	|- ( F e. ( R GrpHom S ) -> F e. ( R MndHom S ) )
5	1 2	mhm0	|- ( F e. ( R MndHom S ) -> ( F ` .0. ) = Z )
6	3 4 5	3syl	|- ( F e. ( R RingHom S ) -> ( F ` .0. ) = Z )