Theorem rhmadd

Description: Ring homomorphisms preserve addition. (Contributed by Jeff Madsen, 3-Jan-2011) (Revised by AV, 10-Jan-2025)

	Ref	Expression
Hypotheses	rhmadd.x	|- X = ( Base ` R )
	rhmadd.p	|- .+ = ( +g ` R )
	rhmadd.q	|- .+^ = ( +g ` S )
Assertion	rhmadd	|- ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmadd.x	|- X = ( Base ` R )
2		rhmadd.p	|- .+ = ( +g ` R )
3		rhmadd.q	|- .+^ = ( +g ` S )
4		rhmghm	|- ( F e. ( R RingHom S ) -> F e. ( R GrpHom S ) )
5		ghmmhm	|- ( F e. ( R GrpHom S ) -> F e. ( R MndHom S ) )
6	4 5	syl	|- ( F e. ( R RingHom S ) -> F e. ( R MndHom S ) )
7	1 2 3	mhmlin	|- ( ( F e. ( R MndHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) )
8	6 7	syl3an1	|- ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .+ B ) ) = ( ( F ` A ) .+^ ( F ` B ) ) )