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 ‘ 𝑅 )
	rhm0.z	⊢ 𝑍 = ( 0g ‘ 𝑆 )
Assertion	rhm0	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ 0 ) = 𝑍 )

Proof

Step	Hyp	Ref	Expression
1		rhm0.0	⊢ 0 = ( 0g ‘ 𝑅 )
2		rhm0.z	⊢ 𝑍 = ( 0g ‘ 𝑆 )
3		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
4		ghmmhm	⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) )
5	1 2	mhm0	⊢ ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) → ( 𝐹 ‘ 0 ) = 𝑍 )
6	3 4 5	3syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → ( 𝐹 ‘ 0 ) = 𝑍 )