Theorem rhmmul

Description: A homomorphism of rings preserves multiplication. (Contributed by Mario Carneiro, 12-Jun-2015)

	Ref	Expression
Hypotheses	rhmmul.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
	rhmmul.m	⊢ · = ( .r ‘ 𝑅 )
	rhmmul.n	⊢ × = ( .r ‘ 𝑆 )
Assertion	rhmmul	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) × ( 𝐹 ‘ 𝐵 ) ) )

Proof

Step	Hyp	Ref	Expression
1		rhmmul.x	⊢ 𝑋 = ( Base ‘ 𝑅 )
2		rhmmul.m	⊢ · = ( .r ‘ 𝑅 )
3		rhmmul.n	⊢ × = ( .r ‘ 𝑆 )
4		eqid	⊢ ( mulGrp ‘ 𝑅 ) = ( mulGrp ‘ 𝑅 )
5		eqid	⊢ ( mulGrp ‘ 𝑆 ) = ( mulGrp ‘ 𝑆 )
6	4 5	rhmmhm	⊢ ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) → 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) )
7	4 1	mgpbas	⊢ 𝑋 = ( Base ‘ ( mulGrp ‘ 𝑅 ) )
8	4 2	mgpplusg	⊢ · = ( +g ‘ ( mulGrp ‘ 𝑅 ) )
9	5 3	mgpplusg	⊢ × = ( +g ‘ ( mulGrp ‘ 𝑆 ) )
10	7 8 9	mhmlin	⊢ ( ( 𝐹 ∈ ( ( mulGrp ‘ 𝑅 ) MndHom ( mulGrp ‘ 𝑆 ) ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) × ( 𝐹 ‘ 𝐵 ) ) )
11	6 10	syl3an1	⊢ ( ( 𝐹 ∈ ( 𝑅 RingHom 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) × ( 𝐹 ‘ 𝐵 ) ) )