Metamath Proof Explorer


Theorem rngokerinj

Description: A ring homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011)

Ref Expression
Hypotheses rngkerinj.1
|- G = ( 1st ` R )
rngkerinj.2
|- X = ran G
rngkerinj.3
|- W = ( GId ` G )
rngkerinj.4
|- J = ( 1st ` S )
rngkerinj.5
|- Y = ran J
rngkerinj.6
|- Z = ( GId ` J )
Assertion rngokerinj
|- ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RngHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) )

Proof

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