Metamath Proof Explorer

Theorem rhmmul

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

Ref Expression
Hypotheses rhmmul.x 
|- X = ( Base ` R )
rhmmul.m 
|- .x. = ( .r ` R )
rhmmul.n 
|- .X. = ( .r ` S )
Assertion rhmmul 
|- ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .x. B ) ) = ( ( F ` A ) .X. ( F ` B ) ) )

Proof

Step Hyp Ref Expression
1 rhmmul.x 
 |-  X = ( Base ` R )
2 rhmmul.m 
 |-  .x. = ( .r ` R )
3 rhmmul.n 
 |-  .X. = ( .r ` S )
4 eqid 
 |-  ( mulGrp ` R ) = ( mulGrp ` R )
5 eqid 
 |-  ( mulGrp ` S ) = ( mulGrp ` S )
6 4 5 rhmmhm 
 |-  ( F e. ( R RingHom S ) -> F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) )
7 4 1 mgpbas 
 |-  X = ( Base ` ( mulGrp ` R ) )
8 4 2 mgpplusg 
 |-  .x. = ( +g ` ( mulGrp ` R ) )
9 5 3 mgpplusg 
 |-  .X. = ( +g ` ( mulGrp ` S ) )
10 7 8 9 mhmlin 
 |-  ( ( F e. ( ( mulGrp ` R ) MndHom ( mulGrp ` S ) ) /\ A e. X /\ B e. X ) -> ( F ` ( A .x. B ) ) = ( ( F ` A ) .X. ( F ` B ) ) )
11 6 10 syl3an1 
 |-  ( ( F e. ( R RingHom S ) /\ A e. X /\ B e. X ) -> ( F ` ( A .x. B ) ) = ( ( F ` A ) .X. ( F ` B ) ) )