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={\mathrm{Base}}_R$$
	rhmadd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
	rhmadd.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
Assertion	rhmadd	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmadd.x	$$⊢X={\mathrm{Base}}_R$$
2		rhmadd.p	$$⊢\underset{\dot{}}{+}={+}_R$$
3		rhmadd.q	$$⊢\underset{\dot{}}{⨣}={+}_S$$
4		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
5		ghmmhm	$$⊢F\in \left(R\mathrm{GrpHom}S\right)\to F\in \left(R\mathrm{MndHom}S\right)$$
6	4 5	syl	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{MndHom}S\right)$$
7	1 2 3	mhmlin	$$⊢\left(F\in \left(R\mathrm{MndHom}S\right)\wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)$$
8	6 7	syl3an1	$$⊢\left(F\in \left(R\mathrm{RingHom}S\right)\wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{+}B\right)=F\left(A\right)\underset{\dot{}}{⨣}F\left(B\right)$$