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 kerf1ghm.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
kerf1ghm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
kerf1ghm.n ⊢ 𝑁 = ( 0g ‘ 𝑅 )
kerf1ghm.1 ⊢ 0 = ( 0g ‘ 𝑆 )
Assertion kerf1ghm ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) )

Proof

Step Hyp Ref Expression
1 kerf1ghm.a ⊢ 𝐴 = ( Base ‘ 𝑅 )
2 kerf1ghm.b ⊢ 𝐵 = ( Base ‘ 𝑆 )
3 kerf1ghm.n ⊢ 𝑁 = ( 0g ‘ 𝑅 )
4 kerf1ghm.1 ⊢ 0 = ( 0g ‘ 𝑆 )
5 simpl ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) )
6 f1fn ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 → 𝐹 Fn 𝐴 )
7 6 adantl ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → 𝐹 Fn 𝐴 )
8 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ) ) )
9 7 8 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ) ) )
10 9 biimpa ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → ( 𝑥 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ) )
11 10 simpld ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → 𝑥 ∈ 𝐴 )
12 10 simprd ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → ( 𝐹 ‘ 𝑥 ) ∈ { 0 } )
13 fvex ⊢ ( 𝐹 ‘ 𝑥 ) ∈ V
14 13 elsn ⊢ ( ( 𝐹 ‘ 𝑥 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝑥 ) = 0 )
15 12 14 sylib ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → ( 𝐹 ‘ 𝑥 ) = 0 )
16 1 2 4 3 f1ghm0to0 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 ↔ 𝑥 = 𝑁 ) )
17 16 biimpd ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 → 𝑥 = 𝑁 ) )
18 17 3expa ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = 0 → 𝑥 = 𝑁 ) )
19 18 imp ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = 0 ) → 𝑥 = 𝑁 )
20 5 11 15 19 syl21anc ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) ∧ 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) ) → 𝑥 = 𝑁 )
21 20 ex ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) → 𝑥 = 𝑁 ) )
22 velsn ⊢ ( 𝑥 ∈ { 𝑁 } ↔ 𝑥 = 𝑁 )
23 21 22 syl6ibr ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( 𝑥 ∈ ( ◡ 𝐹 “ { 0 } ) → 𝑥 ∈ { 𝑁 } ) )
24 23 ssrdv ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ◡ 𝐹 “ { 0 } ) ⊆ { 𝑁 } )
25 ghmgrp1 ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑅 ∈ Grp )
26 1 3 grpidcl ⊢ ( 𝑅 ∈ Grp → 𝑁 ∈ 𝐴 )
27 25 26 syl ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑁 ∈ 𝐴 )
28 3 4 ghmid ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 𝑁 ) = 0 )
29 fvex ⊢ ( 𝐹 ‘ 𝑁 ) ∈ V
30 29 elsn ⊢ ( ( 𝐹 ‘ 𝑁 ) ∈ { 0 } ↔ ( 𝐹 ‘ 𝑁 ) = 0 )
31 28 30 sylibr ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 ‘ 𝑁 ) ∈ { 0 } )
32 1 2 ghmf ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝐹 : 𝐴 ⟶ 𝐵 )
33 ffn ⊢ ( 𝐹 : 𝐴 ⟶ 𝐵 → 𝐹 Fn 𝐴 )
34 elpreima ⊢ ( 𝐹 Fn 𝐴 → ( 𝑁 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑁 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑁 ) ∈ { 0 } ) ) )
35 32 33 34 3syl ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝑁 ∈ ( ◡ 𝐹 “ { 0 } ) ↔ ( 𝑁 ∈ 𝐴 ∧ ( 𝐹 ‘ 𝑁 ) ∈ { 0 } ) ) )
36 27 31 35 mpbir2and ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → 𝑁 ∈ ( ◡ 𝐹 “ { 0 } ) )
37 36 snssd ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → { 𝑁 } ⊆ ( ◡ 𝐹 “ { 0 } ) )
38 37 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → { 𝑁 } ⊆ ( ◡ 𝐹 “ { 0 } ) )
39 24 38 eqssd ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝐹 : 𝐴 –1-1→ 𝐵 ) → ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } )
40 32 adantr ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) → 𝐹 : 𝐴 ⟶ 𝐵 )
41 simpl ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) )
42 simpr2l ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 ∈ 𝐴 )
43 simpr2r ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑦 ∈ 𝐴 )
44 simpr3 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) )
45 eqid ⊢ ( ◡ 𝐹 “ { 0 } ) = ( ◡ 𝐹 “ { 0 } )
46 eqid ⊢ ( -g ‘ 𝑅 ) = ( -g ‘ 𝑅 )
47 1 4 45 46 ghmeqker ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ↔ ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) ∈ ( ◡ 𝐹 “ { 0 } ) ) )
48 47 biimpa ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) ∈ ( ◡ 𝐹 “ { 0 } ) )
49 41 42 43 44 48 syl31anc ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) ∈ ( ◡ 𝐹 “ { 0 } ) )
50 simpr1 ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } )
51 49 50 eleqtrd ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) ∈ { 𝑁 } )
52 ovex ⊢ ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) ∈ V
53 52 elsn ⊢ ( ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) ∈ { 𝑁 } ↔ ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = 𝑁 )
54 51 53 sylib ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = 𝑁 )
55 41 25 syl ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑅 ∈ Grp )
56 1 3 46 grpsubeq0 ⊢ ( ( 𝑅 ∈ Grp ∧ 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) → ( ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = 𝑁 ↔ 𝑥 = 𝑦 ) )
57 55 42 43 56 syl3anc ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → ( ( 𝑥 ( -g ‘ 𝑅 ) 𝑦 ) = 𝑁 ↔ 𝑥 = 𝑦 ) )
58 54 57 mpbid ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) ) → 𝑥 = 𝑦 )
59 58 3anassrs ⊢ ( ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) ∧ ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) ) → 𝑥 = 𝑦 )
60 59 ex ⊢ ( ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) ∧ ( 𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ) ) → ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
61 60 ralrimivva ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) → ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) )
62 dff13 ⊢ ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( 𝐹 : 𝐴 ⟶ 𝐵 ∧ ∀ 𝑥 ∈ 𝐴 ∀ 𝑦 ∈ 𝐴 ( ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝑦 ) → 𝑥 = 𝑦 ) ) )
63 40 61 62 sylanbrc ⊢ ( ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) ∧ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) → 𝐹 : 𝐴 –1-1→ 𝐵 )
64 39 63 impbida ⊢ ( 𝐹 ∈ ( 𝑅 GrpHom 𝑆 ) → ( 𝐹 : 𝐴 –1-1→ 𝐵 ↔ ( ◡ 𝐹 “ { 0 } ) = { 𝑁 } ) )