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 R RngHomo S R Rng S Rng F R GrpHom S F 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
5 eqid S = S
6 3 4 5 isrnghm F R RngHomo S R Rng S Rng F R GrpHom S x Base R y Base R F x R y = F x S F y
7 1 rngmgp Could not format ( R e. Rng -> M e. Smgrp ) : No typesetting found for |- ( R e. Rng -> M e. Smgrp ) with typecode |-
8 sgrpmgm Could not format ( M e. Smgrp -> M e. Mgm ) : No typesetting found for |- ( M e. Smgrp -> M e. Mgm ) with typecode |-
9 7 8 syl R Rng M Mgm
10 2 rngmgp Could not format ( S e. Rng -> N e. Smgrp ) : No typesetting found for |- ( S e. Rng -> N e. Smgrp ) with typecode |-
11 sgrpmgm Could not format ( N e. Smgrp -> N e. Mgm ) : No typesetting found for |- ( N e. Smgrp -> N e. Mgm ) with typecode |-
12 10 11 syl S Rng N Mgm
13 9 12 anim12i R Rng S Rng M Mgm N Mgm
14 eqid Base S = Base S
15 3 14 ghmf F R GrpHom S F : Base R Base S
16 13 15 anim12i R Rng S Rng F R GrpHom S M Mgm N Mgm F : Base R Base S
17 16 biantrurd R Rng S Rng F R GrpHom S x Base R y Base R F x R y = F x S F y M Mgm N Mgm F : Base R Base S x Base R y Base R F x R y = F x S F y
18 anass M Mgm N Mgm F : Base R Base S x Base R y Base R F x R y = F x S F y M Mgm N Mgm F : Base R Base S x Base R y Base R F x R y = F x S F y
19 17 18 bitrdi R Rng S Rng F R GrpHom S x Base R y Base R F x R y = F x S F y M Mgm N Mgm F : Base R Base S x Base R y Base R F x R y = F x S F y
20 1 3 mgpbas Base R = Base M
21 2 14 mgpbas Base S = Base N
22 1 4 mgpplusg R = + M
23 2 5 mgpplusg S = + N
24 20 21 22 23 ismgmhm F M MgmHom N M Mgm N Mgm F : Base R Base S x Base R y Base R F x R y = F x S F y
25 19 24 bitr4di R Rng S Rng F R GrpHom S x Base R y Base R F x R y = F x S F y F M MgmHom N
26 25 pm5.32da R Rng S Rng F R GrpHom S x Base R y Base R F x R y = F x S F y F R GrpHom S F M MgmHom N
27 26 pm5.32i R Rng S Rng F R GrpHom S x Base R y Base R F x R y = F x S F y R Rng S Rng F R GrpHom S F M MgmHom N
28 6 27 bitri F R RngHomo S R Rng S Rng F R GrpHom S F M MgmHom N