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 ) ) |