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 RingOpsHom 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 RingOpsHom 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 RingOpsHom S ) ) -> ( 1st ` S ) e. GrpOp )
13 7 10 rngogrphom 
 |-  ( ( R e. RingOps /\ S e. RingOps /\ F e. ( R RingOpsHom 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 RingOpsHom S ) ) -> ( F : X -1-1-> Y <-> ( `' F " { Z } ) = { W } ) )