Metamath Proof Explorer


Theorem rngogrphom

Description: A ring homomorphism is a group homomorphism. (Contributed by Jeff Madsen, 2-Jan-2011)

Ref Expression
Hypotheses rnggrphom.1 G = 1 st R
rnggrphom.2 J = 1 st S
Assertion rngogrphom R RingOps S RingOps F R RngHom S F G GrpOpHom J

Proof

Step Hyp Ref Expression
1 rnggrphom.1 G = 1 st R
2 rnggrphom.2 J = 1 st S
3 eqid ran G = ran G
4 eqid ran J = ran J
5 1 3 2 4 rngohomf R RingOps S RingOps F R RngHom S F : ran G ran J
6 1 3 2 rngohomadd R RingOps S RingOps F R RngHom S x ran G y ran G F x G y = F x J F y
7 6 eqcomd R RingOps S RingOps F R RngHom S x ran G y ran G F x J F y = F x G y
8 7 ralrimivva R RingOps S RingOps F R RngHom S x ran G y ran G F x J F y = F x G y
9 1 rngogrpo R RingOps G GrpOp
10 2 rngogrpo S RingOps J GrpOp
11 3 4 elghomOLD G GrpOp J GrpOp F G GrpOpHom J F : ran G ran J x ran G y ran G F x J F y = F x G y
12 9 10 11 syl2an R RingOps S RingOps F G GrpOpHom J F : ran G ran J x ran G y ran G F x J F y = F x G y
13 12 3adant3 R RingOps S RingOps F R RngHom S F G GrpOpHom J F : ran G ran J x ran G y ran G F x J F y = F x G y
14 5 8 13 mpbir2and R RingOps S RingOps F R RngHom S F G GrpOpHom J