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	⊢ 𝑋 = ( Base ‘ 𝑅 )
	rhmadd.p	⊢ + = ( +g ‘ 𝑅 )
	rhmadd.q	⊢ ⨣ = ( +g ‘ 𝑆 )
Assertion	rhmadd	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmadd.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		rhmadd.p	⊢ + = ( +g ‘ 𝑅 )
3		rhmadd.q	⊢ ⨣ = ( +g ‘ 𝑆 )
4		rhmghm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
5		ghmmhm	⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) )
6	4 5	syl	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) )
7	1 2 3	mhmlin	⊢ ( ( 𝐹 ∈ ( 𝑅 MndHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) )
8	6 7	syl3an1	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 + 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) ⨣ ( 𝐹 ‘ 𝐵 ) ) )