Metamath Proof Explorer


Theorem isrhm

Description: A function is a ring homomorphism iff it preserves both addition and multiplication. (Contributed by Stefan O'Rear, 7-Mar-2015)

Ref Expression
Hypotheses isrhm.m M = mulGrp R
isrhm.n N = mulGrp S
Assertion isrhm F R RingHom S R Ring S Ring F R GrpHom S F M MndHom N

Proof

Step Hyp Ref Expression
1 isrhm.m M = mulGrp R
2 isrhm.n N = mulGrp S
3 dfrhm2 RingHom = r Ring , s Ring r GrpHom s mulGrp r MndHom mulGrp s
4 3 elmpocl F R RingHom S R Ring S Ring
5 oveq12 r = R s = S r GrpHom s = R GrpHom S
6 fveq2 r = R mulGrp r = mulGrp R
7 fveq2 s = S mulGrp s = mulGrp S
8 6 7 oveqan12d r = R s = S mulGrp r MndHom mulGrp s = mulGrp R MndHom mulGrp S
9 5 8 ineq12d r = R s = S r GrpHom s mulGrp r MndHom mulGrp s = R GrpHom S mulGrp R MndHom mulGrp S
10 ovex R GrpHom S V
11 10 inex1 R GrpHom S mulGrp R MndHom mulGrp S V
12 9 3 11 ovmpoa R Ring S Ring R RingHom S = R GrpHom S mulGrp R MndHom mulGrp S
13 12 eleq2d R Ring S Ring F R RingHom S F R GrpHom S mulGrp R MndHom mulGrp S
14 elin F R GrpHom S mulGrp R MndHom mulGrp S F R GrpHom S F mulGrp R MndHom mulGrp S
15 1 2 oveq12i M MndHom N = mulGrp R MndHom mulGrp S
16 15 eqcomi mulGrp R MndHom mulGrp S = M MndHom N
17 16 eleq2i F mulGrp R MndHom mulGrp S F M MndHom N
18 17 anbi2i F R GrpHom S F mulGrp R MndHom mulGrp S F R GrpHom S F M MndHom N
19 14 18 bitri F R GrpHom S mulGrp R MndHom mulGrp S F R GrpHom S F M MndHom N
20 13 19 bitrdi R Ring S Ring F R RingHom S F R GrpHom S F M MndHom N
21 4 20 biadanii F R RingHom S R Ring S Ring F R GrpHom S F M MndHom N