Metamath Proof Explorer

Theorem isrnghmmul

Description: A function is a non-unital ring homomorphism iff it preserves both addition and multiplication. (Contributed by AV, 27-Feb-2020)

Ref Expression
Hypotheses isrnghmmul.m 
|- M = ( mulGrp ` R )
isrnghmmul.n 
|- N = ( mulGrp ` S )
Assertion isrnghmmul 
|- ( F e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MgmHom N ) ) ) )

Proof

Step Hyp Ref Expression
1 isrnghmmul.m 
 |-  M = ( mulGrp ` R )
2 isrnghmmul.n 
 |-  N = ( mulGrp ` S )
3 eqid 
 |-  ( Base ` R ) = ( Base ` R )
4 eqid 
 |-  ( .r ` R ) = ( .r ` R )
5 eqid 
 |-  ( .r ` S ) = ( .r ` S )
6 3 4 5 isrnghm 
 |-  ( F e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) )
7 1 rngmgp 
 |-  ( R e. Rng -> M e. Smgrp )
8 sgrpmgm 
 |-  ( M e. Smgrp -> M e. Mgm )
9 7 8 syl 
 |-  ( R e. Rng -> M e. Mgm )
10 2 rngmgp 
 |-  ( S e. Rng -> N e. Smgrp )
11 sgrpmgm 
 |-  ( N e. Smgrp -> N e. Mgm )
12 10 11 syl 
 |-  ( S e. Rng -> N e. Mgm )
13 9 12 anim12i 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( M e. Mgm /\ N e. Mgm ) )
14 eqid 
 |-  ( Base ` S ) = ( Base ` S )
15 3 14 ghmf 
 |-  ( F e. ( R GrpHom S ) -> F : ( Base ` R ) --> ( Base ` S ) )
16 13 15 anim12i 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ F e. ( R GrpHom S ) ) -> ( ( M e. Mgm /\ N e. Mgm ) /\ F : ( Base ` R ) --> ( Base ` S ) ) )
17 16 biantrurd 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ F e. ( R GrpHom S ) ) -> ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) <-> ( ( ( M e. Mgm /\ N e. Mgm ) /\ F : ( Base ` R ) --> ( Base ` S ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) )
18 anass 
 |-  ( ( ( ( M e. Mgm /\ N e. Mgm ) /\ F : ( Base ` R ) --> ( Base ` S ) ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) <-> ( ( M e. Mgm /\ N e. Mgm ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) )
19 17 18 bitrdi 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ F e. ( R GrpHom S ) ) -> ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) <-> ( ( M e. Mgm /\ N e. Mgm ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) ) )
20 1 3 mgpbas 
 |-  ( Base ` R ) = ( Base ` M )
21 2 14 mgpbas 
 |-  ( Base ` S ) = ( Base ` N )
22 1 4 mgpplusg 
 |-  ( .r ` R ) = ( +g ` M )
23 2 5 mgpplusg 
 |-  ( .r ` S ) = ( +g ` N )
24 20 21 22 23 ismgmhm 
 |-  ( F e. ( M MgmHom N ) <-> ( ( M e. Mgm /\ N e. Mgm ) /\ ( F : ( Base ` R ) --> ( Base ` S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) )
25 19 24 bitr4di 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ F e. ( R GrpHom S ) ) -> ( A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) <-> F e. ( M MgmHom N ) ) )
26 25 pm5.32da 
 |-  ( ( R e. Rng /\ S e. Rng ) -> ( ( F e. ( R GrpHom S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) <-> ( F e. ( R GrpHom S ) /\ F e. ( M MgmHom N ) ) ) )
27 26 pm5.32i 
 |-  ( ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ A. x e. ( Base ` R ) A. y e. ( Base ` R ) ( F ` ( x ( .r ` R ) y ) ) = ( ( F ` x ) ( .r ` S ) ( F ` y ) ) ) ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MgmHom N ) ) ) )
28 6 27 bitri 
 |-  ( F e. ( R RngHom S ) <-> ( ( R e. Rng /\ S e. Rng ) /\ ( F e. ( R GrpHom S ) /\ F e. ( M MgmHom N ) ) ) )