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 RingOpsHom 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 RingOpsHom S ) ) -> F : ran G --> ran J )
6 1 3 2 rngohomadd 
 |-  ( ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom 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 RingOpsHom S ) ) -> F e. ( G GrpOpHom J ) )