This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 𝑆 ) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝐴 · 𝐵 ) ) = ( ( 𝐹 ‘ 𝐴 ) × ( 𝐹 ‘ 𝐵 ) ) )