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	⊢ 𝑋 = ( Base ‘ 𝑅 )
	rhmsub.m	⊢ − = ( -g ‘ 𝑅 )
	rhmsub.n	⊢ 𝑁 = ( -g ‘ 𝑆 )
Assertion	rhmsub	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝑁 ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmsub.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		rhmsub.m	⊢ − = ( -g ‘ 𝑅 )
3		rhmsub.n	⊢ 𝑁 = ( -g ‘ 𝑆 )
4		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
5	1 2 3	ghmsub	⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝑁 ( 𝐹 ‘ 𝐵 ) ) )
6	4 5	syl3an1	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 − 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) 𝑁 ( 𝐹 ‘ 𝐵 ) ) )