Metamath Proof Explorer

Theorem grpokerinj

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

Ref Expression
Hypotheses grpkerinj.1 
|- X = ran G
grpkerinj.2 
|- W = ( GId ` G )
grpkerinj.3 
|- Y = ran H
grpkerinj.4 
|- U = ( GId ` H )
Assertion grpokerinj 
|- ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F : X -1-1-> Y <-> ( `' F " { U } ) = { W } ) )

Proof

Step Hyp Ref Expression
1 grpkerinj.1 
 |-  X = ran G
2 grpkerinj.2 
 |-  W = ( GId ` G )
3 grpkerinj.3 
 |-  Y = ran H
4 grpkerinj.4 
 |-  U = ( GId ` H )
5 2 4 ghomidOLD 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F ` W ) = U )
6 5 sneqd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> { ( F ` W ) } = { U } )
7 1 3 ghomf 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F : X --> Y )
8 7 ffnd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> F Fn X )
9 1 2 grpoidcl 
 |-  ( G e. GrpOp -> W e. X )
10 9 3ad2ant1 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> W e. X )
11 fnsnfv 
 |-  ( ( F Fn X /\ W e. X ) -> { ( F ` W ) } = ( F " { W } ) )
12 8 10 11 syl2anc 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> { ( F ` W ) } = ( F " { W } ) )
13 6 12 eqtr3d 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> { U } = ( F " { W } ) )
14 13 imaeq2d 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( `' F " { U } ) = ( `' F " ( F " { W } ) ) )
15 14 adantl 
 |-  ( ( F : X -1-1-> Y /\ ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) ) -> ( `' F " { U } ) = ( `' F " ( F " { W } ) ) )
16 9 snssd 
 |-  ( G e. GrpOp -> { W } C_ X )
17 16 3ad2ant1 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> { W } C_ X )
18 f1imacnv 
 |-  ( ( F : X -1-1-> Y /\ { W } C_ X ) -> ( `' F " ( F " { W } ) ) = { W } )
19 17 18 sylan2 
 |-  ( ( F : X -1-1-> Y /\ ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) ) -> ( `' F " ( F " { W } ) ) = { W } )
20 15 19 eqtrd 
 |-  ( ( F : X -1-1-> Y /\ ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) ) -> ( `' F " { U } ) = { W } )
21 20 expcom 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F : X -1-1-> Y -> ( `' F " { U } ) = { W } ) )
22 7 adantr 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) -> F : X --> Y )
23 simpl2 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> H e. GrpOp )
24 7 ffvelcdmda 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ x e. X ) -> ( F ` x ) e. Y )
25 24 adantrr 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( F ` x ) e. Y )
26 7 ffvelcdmda 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ y e. X ) -> ( F ` y ) e. Y )
27 26 adantrl 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( F ` y ) e. Y )
28 eqid 
 |-  ( /g ` H ) = ( /g ` H )
29 3 4 28 grpoeqdivid 
 |-  ( ( H e. GrpOp /\ ( F ` x ) e. Y /\ ( F ` y ) e. Y ) -> ( ( F ` x ) = ( F ` y ) <-> ( ( F ` x ) ( /g ` H ) ( F ` y ) ) = U ) )
30 23 25 27 29 syl3anc 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( ( F ` x ) ( /g ` H ) ( F ` y ) ) = U ) )
31 30 adantlr 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) <-> ( ( F ` x ) ( /g ` H ) ( F ` y ) ) = U ) )
32 eqid 
 |-  ( /g ` G ) = ( /g ` G )
33 1 32 28 ghomdiv 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x ( /g ` G ) y ) ) = ( ( F ` x ) ( /g ` H ) ( F ` y ) ) )
34 33 adantlr 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( F ` ( x ( /g ` G ) y ) ) = ( ( F ` x ) ( /g ` H ) ( F ` y ) ) )
35 34 eqeq1d 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` ( x ( /g ` G ) y ) ) = U <-> ( ( F ` x ) ( /g ` H ) ( F ` y ) ) = U ) )
36 4 fvexi 
 |-  U e. _V
37 36 snid 
 |-  U e. { U }
38 eleq1 
 |-  ( ( F ` ( x ( /g ` G ) y ) ) = U -> ( ( F ` ( x ( /g ` G ) y ) ) e. { U } <-> U e. { U } ) )
39 37 38 mpbiri 
 |-  ( ( F ` ( x ( /g ` G ) y ) ) = U -> ( F ` ( x ( /g ` G ) y ) ) e. { U } )
40 7 ffund 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> Fun F )
41 40 adantr 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> Fun F )
42 1 32 grpodivcl 
 |-  ( ( G e. GrpOp /\ x e. X /\ y e. X ) -> ( x ( /g ` G ) y ) e. X )
43 42 3expb 
 |-  ( ( G e. GrpOp /\ ( x e. X /\ y e. X ) ) -> ( x ( /g ` G ) y ) e. X )
44 43 3ad2antl1 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( x ( /g ` G ) y ) e. X )
45 7 fdmd 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> dom F = X )
46 45 adantr 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> dom F = X )
47 44 46 eleqtrrd 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( x ( /g ` G ) y ) e. dom F )
48 fvimacnv 
 |-  ( ( Fun F /\ ( x ( /g ` G ) y ) e. dom F ) -> ( ( F ` ( x ( /g ` G ) y ) ) e. { U } <-> ( x ( /g ` G ) y ) e. ( `' F " { U } ) ) )
49 41 47 48 syl2anc 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` ( x ( /g ` G ) y ) ) e. { U } <-> ( x ( /g ` G ) y ) e. ( `' F " { U } ) ) )
50 eleq2 
 |-  ( ( `' F " { U } ) = { W } -> ( ( x ( /g ` G ) y ) e. ( `' F " { U } ) <-> ( x ( /g ` G ) y ) e. { W } ) )
51 49 50 sylan9bb 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) /\ ( `' F " { U } ) = { W } ) -> ( ( F ` ( x ( /g ` G ) y ) ) e. { U } <-> ( x ( /g ` G ) y ) e. { W } ) )
52 51 an32s 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` ( x ( /g ` G ) y ) ) e. { U } <-> ( x ( /g ` G ) y ) e. { W } ) )
53 elsni 
 |-  ( ( x ( /g ` G ) y ) e. { W } -> ( x ( /g ` G ) y ) = W )
54 1 2 32 grpoeqdivid 
 |-  ( ( G e. GrpOp /\ x e. X /\ y e. X ) -> ( x = y <-> ( x ( /g ` G ) y ) = W ) )
55 54 biimprd 
 |-  ( ( G e. GrpOp /\ x e. X /\ y e. X ) -> ( ( x ( /g ` G ) y ) = W -> x = y ) )
56 55 3expb 
 |-  ( ( G e. GrpOp /\ ( x e. X /\ y e. X ) ) -> ( ( x ( /g ` G ) y ) = W -> x = y ) )
57 56 3ad2antl1 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( /g ` G ) y ) = W -> x = y ) )
58 53 57 syl5 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( /g ` G ) y ) e. { W } -> x = y ) )
59 58 adantlr 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( x ( /g ` G ) y ) e. { W } -> x = y ) )
60 52 59 sylbid 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` ( x ( /g ` G ) y ) ) e. { U } -> x = y ) )
61 39 60 syl5 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` ( x ( /g ` G ) y ) ) = U -> x = y ) )
62 35 61 sylbird 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( ( F ` x ) ( /g ` H ) ( F ` y ) ) = U -> x = y ) )
63 31 62 sylbid 
 |-  ( ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) /\ ( x e. X /\ y e. X ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
64 63 ralrimivva 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) -> A. x e. X A. y e. X ( ( F ` x ) = ( F ` y ) -> x = y ) )
65 dff13 
 |-  ( F : X -1-1-> Y <-> ( F : X --> Y /\ A. x e. X A. y e. X ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
66 22 64 65 sylanbrc 
 |-  ( ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) /\ ( `' F " { U } ) = { W } ) -> F : X -1-1-> Y )
67 66 ex 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( ( `' F " { U } ) = { W } -> F : X -1-1-> Y ) )
68 21 67 impbid 
 |-  ( ( G e. GrpOp /\ H e. GrpOp /\ F e. ( G GrpOpHom H ) ) -> ( F : X -1-1-> Y <-> ( `' F " { U } ) = { W } ) )