Step |
Hyp |
Ref |
Expression |
1 |
|
rngkerinj.1 |
|- G = ( 1st ` R ) |
2 |
|
rngkerinj.2 |
|- X = ran G |
3 |
|
rngkerinj.3 |
|- W = ( GId ` G ) |
4 |
|
rngkerinj.4 |
|- J = ( 1st ` S ) |
5 |
|
rngkerinj.5 |
|- Y = ran J |
6 |
|
rngkerinj.6 |
|- Z = ( GId ` J ) |
7 |
|
eqid |
|- ( 1st ` R ) = ( 1st ` R ) |
8 |
7
|
rngogrpo |
|- ( R e. RingOps -> ( 1st ` R ) e. GrpOp ) |
9 |
8
|
3ad2ant1 |
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( 1st ` R ) e. GrpOp ) |
10 |
|
eqid |
|- ( 1st ` S ) = ( 1st ` S ) |
11 |
10
|
rngogrpo |
|- ( S e. RingOps -> ( 1st ` S ) e. GrpOp ) |
12 |
11
|
3ad2ant2 |
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( 1st ` S ) e. GrpOp ) |
13 |
7 10
|
rngogrphom |
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> F e. ( ( 1st ` R ) GrpOpHom ( 1st ` S ) ) ) |
14 |
1
|
rneqi |
|- ran G = ran ( 1st ` R ) |
15 |
2 14
|
eqtri |
|- X = ran ( 1st ` R ) |
16 |
1
|
fveq2i |
|- ( GId ` G ) = ( GId ` ( 1st ` R ) ) |
17 |
3 16
|
eqtri |
|- W = ( GId ` ( 1st ` R ) ) |
18 |
4
|
rneqi |
|- ran J = ran ( 1st ` S ) |
19 |
5 18
|
eqtri |
|- Y = ran ( 1st ` S ) |
20 |
4
|
fveq2i |
|- ( GId ` J ) = ( GId ` ( 1st ` S ) ) |
21 |
6 20
|
eqtri |
|- Z = ( GId ` ( 1st ` S ) ) |
22 |
15 17 19 21
|
grpokerinj |
|- ( ( ( 1st ` R ) e. GrpOp /\ ( 1st ` S ) e. GrpOp /\ F e. ( ( 1st ` R ) GrpOpHom ( 1st ` S ) ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) ) |
23 |
9 12 13 22
|
syl3anc |
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) ) |