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 = ( 1st ` R )
rnggrphom.2
|- J = ( 1st ` S )
Assertion rngogrphom
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F e. ( G GrpOpHom J ) )

Proof

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