Metamath Proof Explorer

Theorem kerf1ghm

Description: A group homomorphism F is injective if and only if its kernel is the singleton { N } . (Contributed by Thierry Arnoux, 27-Oct-2017) (Proof shortened by AV, 24-Oct-2019) (Revised by Thierry Arnoux, 13-May-2023)

Ref Expression
Hypotheses f1ghm0to0.a 
|- A = ( Base ` R )
f1ghm0to0.b 
|- B = ( Base ` S )
f1ghm0to0.n 
|- N = ( 0g ` R )
f1ghm0to0.0 
|- .0. = ( 0g ` S )
Assertion kerf1ghm 
|- ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> ( `' F " { .0. } ) = { N } ) )

Proof

Step Hyp Ref Expression
1 f1ghm0to0.a 
 |-  A = ( Base ` R )
2 f1ghm0to0.b 
 |-  B = ( Base ` S )
3 f1ghm0to0.n 
 |-  N = ( 0g ` R )
4 f1ghm0to0.0 
 |-  .0. = ( 0g ` S )
5 simpl 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. ( `' F " { .0. } ) ) -> ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) )
6 f1fn 
 |-  ( F : A -1-1-> B -> F Fn A )
7 6 adantl 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> F Fn A )
8 elpreima 
 |-  ( F Fn A -> ( x e. ( `' F " { .0. } ) <-> ( x e. A /\ ( F ` x ) e. { .0. } ) ) )
9 7 8 syl 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> ( x e. ( `' F " { .0. } ) <-> ( x e. A /\ ( F ` x ) e. { .0. } ) ) )
10 9 biimpa 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. ( `' F " { .0. } ) ) -> ( x e. A /\ ( F ` x ) e. { .0. } ) )
11 10 simpld 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. ( `' F " { .0. } ) ) -> x e. A )
12 10 simprd 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. ( `' F " { .0. } ) ) -> ( F ` x ) e. { .0. } )
13 fvex 
 |-  ( F ` x ) e. _V
14 13 elsn 
 |-  ( ( F ` x ) e. { .0. } <-> ( F ` x ) = .0. )
15 12 14 sylib 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. ( `' F " { .0. } ) ) -> ( F ` x ) = .0. )
16 1 2 3 4 f1ghm0to0 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ x e. A ) -> ( ( F ` x ) = .0. <-> x = N ) )
17 16 biimpd 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B /\ x e. A ) -> ( ( F ` x ) = .0. -> x = N ) )
18 17 3expa 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. A ) -> ( ( F ` x ) = .0. -> x = N ) )
19 18 imp 
 |-  ( ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. A ) /\ ( F ` x ) = .0. ) -> x = N )
20 5 11 15 19 syl21anc 
 |-  ( ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) /\ x e. ( `' F " { .0. } ) ) -> x = N )
21 20 ex 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> ( x e. ( `' F " { .0. } ) -> x = N ) )
22 velsn 
 |-  ( x e. { N } <-> x = N )
23 21 22 imbitrrdi 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> ( x e. ( `' F " { .0. } ) -> x e. { N } ) )
24 23 ssrdv 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> ( `' F " { .0. } ) C_ { N } )
25 ghmgrp1 
 |-  ( F e. ( R GrpHom S ) -> R e. Grp )
26 1 3 grpidcl 
 |-  ( R e. Grp -> N e. A )
27 25 26 syl 
 |-  ( F e. ( R GrpHom S ) -> N e. A )
28 3 4 ghmid 
 |-  ( F e. ( R GrpHom S ) -> ( F ` N ) = .0. )
29 fvex 
 |-  ( F ` N ) e. _V
30 29 elsn 
 |-  ( ( F ` N ) e. { .0. } <-> ( F ` N ) = .0. )
31 28 30 sylibr 
 |-  ( F e. ( R GrpHom S ) -> ( F ` N ) e. { .0. } )
32 1 2 ghmf 
 |-  ( F e. ( R GrpHom S ) -> F : A --> B )
33 ffn 
 |-  ( F : A --> B -> F Fn A )
34 elpreima 
 |-  ( F Fn A -> ( N e. ( `' F " { .0. } ) <-> ( N e. A /\ ( F ` N ) e. { .0. } ) ) )
35 32 33 34 3syl 
 |-  ( F e. ( R GrpHom S ) -> ( N e. ( `' F " { .0. } ) <-> ( N e. A /\ ( F ` N ) e. { .0. } ) ) )
36 27 31 35 mpbir2and 
 |-  ( F e. ( R GrpHom S ) -> N e. ( `' F " { .0. } ) )
37 36 snssd 
 |-  ( F e. ( R GrpHom S ) -> { N } C_ ( `' F " { .0. } ) )
38 37 adantr 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> { N } C_ ( `' F " { .0. } ) )
39 24 38 eqssd 
 |-  ( ( F e. ( R GrpHom S ) /\ F : A -1-1-> B ) -> ( `' F " { .0. } ) = { N } )
40 32 adantr 
 |-  ( ( F e. ( R GrpHom S ) /\ ( `' F " { .0. } ) = { N } ) -> F : A --> B )
41 simpl 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> F e. ( R GrpHom S ) )
42 simpr2l 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> x e. A )
43 simpr2r 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> y e. A )
44 simpr3 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( F ` x ) = ( F ` y ) )
45 eqid 
 |-  ( `' F " { .0. } ) = ( `' F " { .0. } )
46 eqid 
 |-  ( -g ` R ) = ( -g ` R )
47 1 4 45 46 ghmeqker 
 |-  ( ( F e. ( R GrpHom S ) /\ x e. A /\ y e. A ) -> ( ( F ` x ) = ( F ` y ) <-> ( x ( -g ` R ) y ) e. ( `' F " { .0. } ) ) )
48 47 biimpa 
 |-  ( ( ( F e. ( R GrpHom S ) /\ x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) -> ( x ( -g ` R ) y ) e. ( `' F " { .0. } ) )
49 41 42 43 44 48 syl31anc 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( x ( -g ` R ) y ) e. ( `' F " { .0. } ) )
50 simpr1 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( `' F " { .0. } ) = { N } )
51 49 50 eleqtrd 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( x ( -g ` R ) y ) e. { N } )
52 ovex 
 |-  ( x ( -g ` R ) y ) e. _V
53 52 elsn 
 |-  ( ( x ( -g ` R ) y ) e. { N } <-> ( x ( -g ` R ) y ) = N )
54 51 53 sylib 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( x ( -g ` R ) y ) = N )
55 25 adantr 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> R e. Grp )
56 1 3 46 grpsubeq0 
 |-  ( ( R e. Grp /\ x e. A /\ y e. A ) -> ( ( x ( -g ` R ) y ) = N <-> x = y ) )
57 55 42 43 56 syl3anc 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> ( ( x ( -g ` R ) y ) = N <-> x = y ) )
58 54 57 mpbid 
 |-  ( ( F e. ( R GrpHom S ) /\ ( ( `' F " { .0. } ) = { N } /\ ( x e. A /\ y e. A ) /\ ( F ` x ) = ( F ` y ) ) ) -> x = y )
59 58 3anassrs 
 |-  ( ( ( ( F e. ( R GrpHom S ) /\ ( `' F " { .0. } ) = { N } ) /\ ( x e. A /\ y e. A ) ) /\ ( F ` x ) = ( F ` y ) ) -> x = y )
60 59 ex 
 |-  ( ( ( F e. ( R GrpHom S ) /\ ( `' F " { .0. } ) = { N } ) /\ ( x e. A /\ y e. A ) ) -> ( ( F ` x ) = ( F ` y ) -> x = y ) )
61 60 ralrimivva 
 |-  ( ( F e. ( R GrpHom S ) /\ ( `' F " { .0. } ) = { N } ) -> A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) )
62 dff13 
 |-  ( F : A -1-1-> B <-> ( F : A --> B /\ A. x e. A A. y e. A ( ( F ` x ) = ( F ` y ) -> x = y ) ) )
63 40 61 62 sylanbrc 
 |-  ( ( F e. ( R GrpHom S ) /\ ( `' F " { .0. } ) = { N } ) -> F : A -1-1-> B )
64 39 63 impbida 
 |-  ( F e. ( R GrpHom S ) -> ( F : A -1-1-> B <-> ( `' F " { .0. } ) = { N } ) )