MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  kerf1ghm Structured version   Visualization version   GIF version

Theorem kerf1ghm 20178
Description: A group homomorphism 𝐹 is injective if and only if its kernel is the singleton {𝑁}. (Contributed by Thierry Arnoux, 27-Oct-2017.) (Proof shortened by AV, 24-Oct-2019.) (Revised by Thierry Arnoux, 13-May-2023.)
Hypotheses
Ref Expression
kerf1ghm.a 𝐴 = (Base‘𝑅)
kerf1ghm.b 𝐵 = (Base‘𝑆)
kerf1ghm.n 𝑁 = (0g𝑅)
kerf1ghm.1 0 = (0g𝑆)
Assertion
Ref Expression
kerf1ghm (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹:𝐴1-1𝐵 ↔ (𝐹 “ { 0 }) = {𝑁}))

Proof of Theorem kerf1ghm
Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 simpl 484 . . . . . . 7 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥 ∈ (𝐹 “ { 0 })) → (𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵))
2 f1fn 6740 . . . . . . . . . . 11 (𝐹:𝐴1-1𝐵𝐹 Fn 𝐴)
32adantl 483 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → 𝐹 Fn 𝐴)
4 elpreima 7009 . . . . . . . . . 10 (𝐹 Fn 𝐴 → (𝑥 ∈ (𝐹 “ { 0 }) ↔ (𝑥𝐴 ∧ (𝐹𝑥) ∈ { 0 })))
53, 4syl 17 . . . . . . . . 9 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → (𝑥 ∈ (𝐹 “ { 0 }) ↔ (𝑥𝐴 ∧ (𝐹𝑥) ∈ { 0 })))
65biimpa 478 . . . . . . . 8 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥 ∈ (𝐹 “ { 0 })) → (𝑥𝐴 ∧ (𝐹𝑥) ∈ { 0 }))
76simpld 496 . . . . . . 7 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥 ∈ (𝐹 “ { 0 })) → 𝑥𝐴)
86simprd 497 . . . . . . . 8 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥 ∈ (𝐹 “ { 0 })) → (𝐹𝑥) ∈ { 0 })
9 fvex 6856 . . . . . . . . 9 (𝐹𝑥) ∈ V
109elsn 4602 . . . . . . . 8 ((𝐹𝑥) ∈ { 0 } ↔ (𝐹𝑥) = 0 )
118, 10sylib 217 . . . . . . 7 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥 ∈ (𝐹 “ { 0 })) → (𝐹𝑥) = 0 )
12 kerf1ghm.a . . . . . . . . . . 11 𝐴 = (Base‘𝑅)
13 kerf1ghm.b . . . . . . . . . . 11 𝐵 = (Base‘𝑆)
14 kerf1ghm.1 . . . . . . . . . . 11 0 = (0g𝑆)
15 kerf1ghm.n . . . . . . . . . . 11 𝑁 = (0g𝑅)
1612, 13, 14, 15f1ghm0to0 20175 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵𝑥𝐴) → ((𝐹𝑥) = 0𝑥 = 𝑁))
1716biimpd 228 . . . . . . . . 9 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵𝑥𝐴) → ((𝐹𝑥) = 0𝑥 = 𝑁))
18173expa 1119 . . . . . . . 8 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥𝐴) → ((𝐹𝑥) = 0𝑥 = 𝑁))
1918imp 408 . . . . . . 7 ((((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥𝐴) ∧ (𝐹𝑥) = 0 ) → 𝑥 = 𝑁)
201, 7, 11, 19syl21anc 837 . . . . . 6 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) ∧ 𝑥 ∈ (𝐹 “ { 0 })) → 𝑥 = 𝑁)
2120ex 414 . . . . 5 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → (𝑥 ∈ (𝐹 “ { 0 }) → 𝑥 = 𝑁))
22 velsn 4603 . . . . 5 (𝑥 ∈ {𝑁} ↔ 𝑥 = 𝑁)
2321, 22syl6ibr 252 . . . 4 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → (𝑥 ∈ (𝐹 “ { 0 }) → 𝑥 ∈ {𝑁}))
2423ssrdv 3951 . . 3 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → (𝐹 “ { 0 }) ⊆ {𝑁})
25 ghmgrp1 19011 . . . . . . 7 (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝑅 ∈ Grp)
2612, 15grpidcl 18779 . . . . . . 7 (𝑅 ∈ Grp → 𝑁𝐴)
2725, 26syl 17 . . . . . 6 (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝑁𝐴)
2815, 14ghmid 19015 . . . . . . 7 (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹𝑁) = 0 )
29 fvex 6856 . . . . . . . 8 (𝐹𝑁) ∈ V
3029elsn 4602 . . . . . . 7 ((𝐹𝑁) ∈ { 0 } ↔ (𝐹𝑁) = 0 )
3128, 30sylibr 233 . . . . . 6 (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹𝑁) ∈ { 0 })
3212, 13ghmf 19013 . . . . . . 7 (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝐹:𝐴𝐵)
33 ffn 6669 . . . . . . 7 (𝐹:𝐴𝐵𝐹 Fn 𝐴)
34 elpreima 7009 . . . . . . 7 (𝐹 Fn 𝐴 → (𝑁 ∈ (𝐹 “ { 0 }) ↔ (𝑁𝐴 ∧ (𝐹𝑁) ∈ { 0 })))
3532, 33, 343syl 18 . . . . . 6 (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝑁 ∈ (𝐹 “ { 0 }) ↔ (𝑁𝐴 ∧ (𝐹𝑁) ∈ { 0 })))
3627, 31, 35mpbir2and 712 . . . . 5 (𝐹 ∈ (𝑅 GrpHom 𝑆) → 𝑁 ∈ (𝐹 “ { 0 }))
3736snssd 4770 . . . 4 (𝐹 ∈ (𝑅 GrpHom 𝑆) → {𝑁} ⊆ (𝐹 “ { 0 }))
3837adantr 482 . . 3 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → {𝑁} ⊆ (𝐹 “ { 0 }))
3924, 38eqssd 3962 . 2 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝐹:𝐴1-1𝐵) → (𝐹 “ { 0 }) = {𝑁})
4032adantr 482 . . 3 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝐹 “ { 0 }) = {𝑁}) → 𝐹:𝐴𝐵)
41 simpl 484 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → 𝐹 ∈ (𝑅 GrpHom 𝑆))
42 simpr2l 1233 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → 𝑥𝐴)
43 simpr2r 1234 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → 𝑦𝐴)
44 simpr3 1197 . . . . . . . . . 10 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝐹𝑥) = (𝐹𝑦))
45 eqid 2737 . . . . . . . . . . . 12 (𝐹 “ { 0 }) = (𝐹 “ { 0 })
46 eqid 2737 . . . . . . . . . . . 12 (-g𝑅) = (-g𝑅)
4712, 14, 45, 46ghmeqker 19036 . . . . . . . . . . 11 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝑥𝐴𝑦𝐴) → ((𝐹𝑥) = (𝐹𝑦) ↔ (𝑥(-g𝑅)𝑦) ∈ (𝐹 “ { 0 })))
4847biimpa 478 . . . . . . . . . 10 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ 𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦)) → (𝑥(-g𝑅)𝑦) ∈ (𝐹 “ { 0 }))
4941, 42, 43, 44, 48syl31anc 1374 . . . . . . . . 9 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝑥(-g𝑅)𝑦) ∈ (𝐹 “ { 0 }))
50 simpr1 1195 . . . . . . . . 9 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝐹 “ { 0 }) = {𝑁})
5149, 50eleqtrd 2840 . . . . . . . 8 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝑥(-g𝑅)𝑦) ∈ {𝑁})
52 ovex 7391 . . . . . . . . 9 (𝑥(-g𝑅)𝑦) ∈ V
5352elsn 4602 . . . . . . . 8 ((𝑥(-g𝑅)𝑦) ∈ {𝑁} ↔ (𝑥(-g𝑅)𝑦) = 𝑁)
5451, 53sylib 217 . . . . . . 7 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → (𝑥(-g𝑅)𝑦) = 𝑁)
5541, 25syl 17 . . . . . . . 8 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → 𝑅 ∈ Grp)
5612, 15, 46grpsubeq0 18834 . . . . . . . 8 ((𝑅 ∈ Grp ∧ 𝑥𝐴𝑦𝐴) → ((𝑥(-g𝑅)𝑦) = 𝑁𝑥 = 𝑦))
5755, 42, 43, 56syl3anc 1372 . . . . . . 7 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → ((𝑥(-g𝑅)𝑦) = 𝑁𝑥 = 𝑦))
5854, 57mpbid 231 . . . . . 6 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ ((𝐹 “ { 0 }) = {𝑁} ∧ (𝑥𝐴𝑦𝐴) ∧ (𝐹𝑥) = (𝐹𝑦))) → 𝑥 = 𝑦)
59583anassrs 1361 . . . . 5 ((((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝐹 “ { 0 }) = {𝑁}) ∧ (𝑥𝐴𝑦𝐴)) ∧ (𝐹𝑥) = (𝐹𝑦)) → 𝑥 = 𝑦)
6059ex 414 . . . 4 (((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝐹 “ { 0 }) = {𝑁}) ∧ (𝑥𝐴𝑦𝐴)) → ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
6160ralrimivva 3198 . . 3 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝐹 “ { 0 }) = {𝑁}) → ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦))
62 dff13 7203 . . 3 (𝐹:𝐴1-1𝐵 ↔ (𝐹:𝐴𝐵 ∧ ∀𝑥𝐴𝑦𝐴 ((𝐹𝑥) = (𝐹𝑦) → 𝑥 = 𝑦)))
6340, 61, 62sylanbrc 584 . 2 ((𝐹 ∈ (𝑅 GrpHom 𝑆) ∧ (𝐹 “ { 0 }) = {𝑁}) → 𝐹:𝐴1-1𝐵)
6439, 63impbida 800 1 (𝐹 ∈ (𝑅 GrpHom 𝑆) → (𝐹:𝐴1-1𝐵 ↔ (𝐹 “ { 0 }) = {𝑁}))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wb 205  wa 397  w3a 1088   = wceq 1542  wcel 2107  wral 3065  wss 3911  {csn 4587  ccnv 5633  cima 5637   Fn wfn 6492  wf 6493  1-1wf1 6494  cfv 6497  (class class class)co 7358  Basecbs 17084  0gc0g 17322  Grpcgrp 18749  -gcsg 18751   GrpHom cghm 19006
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1798  ax-4 1812  ax-5 1914  ax-6 1972  ax-7 2012  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2155  ax-12 2172  ax-ext 2708  ax-rep 5243  ax-sep 5257  ax-nul 5264  ax-pow 5321  ax-pr 5385  ax-un 7673
This theorem depends on definitions:  df-bi 206  df-an 398  df-or 847  df-3an 1090  df-tru 1545  df-fal 1555  df-ex 1783  df-nf 1787  df-sb 2069  df-mo 2539  df-eu 2568  df-clab 2715  df-cleq 2729  df-clel 2815  df-nfc 2890  df-ne 2945  df-ral 3066  df-rex 3075  df-rmo 3354  df-reu 3355  df-rab 3409  df-v 3448  df-sbc 3741  df-csb 3857  df-dif 3914  df-un 3916  df-in 3918  df-ss 3928  df-nul 4284  df-if 4488  df-pw 4563  df-sn 4588  df-pr 4590  df-op 4594  df-uni 4867  df-iun 4957  df-br 5107  df-opab 5169  df-mpt 5190  df-id 5532  df-xp 5640  df-rel 5641  df-cnv 5642  df-co 5643  df-dm 5644  df-rn 5645  df-res 5646  df-ima 5647  df-iota 6449  df-fun 6499  df-fn 6500  df-f 6501  df-f1 6502  df-fo 6503  df-f1o 6504  df-fv 6505  df-riota 7314  df-ov 7361  df-oprab 7362  df-mpo 7363  df-1st 7922  df-2nd 7923  df-0g 17324  df-mgm 18498  df-sgrp 18547  df-mnd 18558  df-grp 18752  df-minusg 18753  df-sbg 18754  df-ghm 19007
This theorem is referenced by:  ghmqusker  32201  dimkerim  32325  zrhf1ker  32559
  Copyright terms: Public domain W3C validator