Theorem rhmsub

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

	Ref	Expression
Hypotheses	rhmsub.x	$$⊢X={\mathrm{Base}}_R$$
	rhmsub.m	$$⊢\underset{\dot{}}{-}={-}_R$$
	rhmsub.n	$$⊢N={-}_S$$
Assertion	rhmsub	$$⊢\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)NF\left(B\right)$$

Proof

Step	Hyp	Ref	Expression
1		rhmsub.x	$$⊢X={\mathrm{Base}}_R$$
2		rhmsub.m	$$⊢\underset{\dot{}}{-}={-}_R$$
3		rhmsub.n	$$⊢N={-}_S$$
4		rhmghm	$$⊢F\in \left(R\mathrm{RingHom}S\right)\to F\in \left(R\mathrm{GrpHom}S\right)$$
5	1 2 3	ghmsub	$$⊢\left(F\in \left(R\mathrm{GrpHom}S\right)\wedge A\in X\wedge B\in X\right)\to F\left(A\underset{\dot{}}{-}B\right)=F\left(A\right)NF\left(B\right)$$
6	4 5	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)NF\left(B\right)$$