Mathbox for Jeff Madsen < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  grpokerinj Unicode version

Theorem grpokerinj 26575
 Description: A group homomorphism is injective if and only if its kernel is zero. (Contributed by Jeff Madsen, 16-Jun-2011.)
Hypotheses
Ref Expression
grpkerinj.1
grpkerinj.2 GId
grpkerinj.3
grpkerinj.4 GId
Assertion
Ref Expression
grpokerinj GrpOpHom

Proof of Theorem grpokerinj
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 grpkerinj.2 . . . . . . . . 9 GId
2 grpkerinj.4 . . . . . . . . 9 GId
31, 2ghomid 21032 . . . . . . . 8 GrpOpHom
43sneqd 3653 . . . . . . 7 GrpOpHom
5 grpkerinj.1 . . . . . . . . . 10
6 grpkerinj.3 . . . . . . . . . 10
75, 6ghomf 26572 . . . . . . . . 9 GrpOpHom
8 ffn 5389 . . . . . . . . 9
97, 8syl 15 . . . . . . . 8 GrpOpHom
105, 1grpoidcl 20884 . . . . . . . . 9
11103ad2ant1 976 . . . . . . . 8 GrpOpHom
12 fnsnfv 5582 . . . . . . . 8
139, 11, 12syl2anc 642 . . . . . . 7 GrpOpHom
144, 13eqtr3d 2317 . . . . . 6 GrpOpHom
1514imaeq2d 5012 . . . . 5 GrpOpHom
1615adantl 452 . . . 4 GrpOpHom
1710snssd 3760 . . . . . 6
18173ad2ant1 976 . . . . 5 GrpOpHom
19 f1imacnv 5489 . . . . 5
2018, 19sylan2 460 . . . 4 GrpOpHom
2116, 20eqtrd 2315 . . 3 GrpOpHom
2221expcom 424 . 2 GrpOpHom
237adantr 451 . . . 4 GrpOpHom
24 simpl2 959 . . . . . . . 8 GrpOpHom
25 ffvelrn 5663 . . . . . . . . . 10
267, 25sylan 457 . . . . . . . . 9 GrpOpHom
2726adantrr 697 . . . . . . . 8 GrpOpHom
28 ffvelrn 5663 . . . . . . . . . 10
297, 28sylan 457 . . . . . . . . 9 GrpOpHom
3029adantrl 696 . . . . . . . 8 GrpOpHom
31 eqid 2283 . . . . . . . . 9
326, 2, 31grpoeqdivid 26571 . . . . . . . 8
3324, 27, 30, 32syl3anc 1182 . . . . . . 7 GrpOpHom
3433adantlr 695 . . . . . 6 GrpOpHom
35 eqid 2283 . . . . . . . . . 10
365, 35, 31ghomdiv 26574 . . . . . . . . 9 GrpOpHom
3736adantlr 695 . . . . . . . 8 GrpOpHom
3837eqeq1d 2291 . . . . . . 7 GrpOpHom
39 fvex 5539 . . . . . . . . . . 11 GId
402, 39eqeltri 2353 . . . . . . . . . 10
4140snid 3667 . . . . . . . . 9
42 eleq1 2343 . . . . . . . . 9
4341, 42mpbiri 224 . . . . . . . 8
44 ffun 5391 . . . . . . . . . . . . . 14
457, 44syl 15 . . . . . . . . . . . . 13 GrpOpHom
4645adantr 451 . . . . . . . . . . . 12 GrpOpHom
475, 35grpodivcl 20914 . . . . . . . . . . . . . . 15
48473expb 1152 . . . . . . . . . . . . . 14
49483ad2antl1 1117 . . . . . . . . . . . . 13 GrpOpHom
50 fdm 5393 . . . . . . . . . . . . . . 15
517, 50syl 15 . . . . . . . . . . . . . 14 GrpOpHom
5251adantr 451 . . . . . . . . . . . . 13 GrpOpHom
5349, 52eleqtrrd 2360 . . . . . . . . . . . 12 GrpOpHom
54 fvimacnv 5640 . . . . . . . . . . . 12
5546, 53, 54syl2anc 642 . . . . . . . . . . 11 GrpOpHom
56 eleq2 2344 . . . . . . . . . . 11
5755, 56sylan9bb 680 . . . . . . . . . 10 GrpOpHom
5857an32s 779 . . . . . . . . 9 GrpOpHom
59 elsni 3664 . . . . . . . . . . 11
605, 1, 35grpoeqdivid 26571 . . . . . . . . . . . . . 14
6160biimprd 214 . . . . . . . . . . . . 13
62613expb 1152 . . . . . . . . . . . 12
63623ad2antl1 1117 . . . . . . . . . . 11 GrpOpHom
6459, 63syl5 28 . . . . . . . . . 10 GrpOpHom
6564adantlr 695 . . . . . . . . 9 GrpOpHom
6658, 65sylbid 206 . . . . . . . 8 GrpOpHom
6743, 66syl5 28 . . . . . . 7 GrpOpHom
6838, 67sylbird 226 . . . . . 6 GrpOpHom
6934, 68sylbid 206 . . . . 5 GrpOpHom
7069ralrimivva 2635 . . . 4 GrpOpHom
71 dff13 5783 . . . 4
7223, 70, 71sylanbrc 645 . . 3 GrpOpHom
7372ex 423 . 2 GrpOpHom
7422, 73impbid 183 1 GrpOpHom
 Colors of variables: wff set class Syntax hints:   wi 4   wb 176   wa 358   w3a 934   wceq 1623   wcel 1684  wral 2543  cvv 2788   wss 3152  csn 3640  ccnv 4688   cdm 4689   crn 4690  cima 4692   wfun 5249   wfn 5250  wf 5251  wf1 5252  cfv 5255  (class class class)co 5858  cgr 20853  GIdcgi 20854   cgs 20856   GrpOpHom cghom 21024 This theorem is referenced by:  rngokerinj  26606 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1533  ax-5 1544  ax-17 1603  ax-9 1635  ax-8 1643  ax-13 1686  ax-14 1688  ax-6 1703  ax-7 1708  ax-11 1715  ax-12 1866  ax-ext 2264  ax-rep 4131  ax-sep 4141  ax-nul 4149  ax-pow 4188  ax-pr 4214  ax-un 4512 This theorem depends on definitions:  df-bi 177  df-or 359  df-an 360  df-3an 936  df-tru 1310  df-ex 1529  df-nf 1532  df-sb 1630  df-eu 2147  df-mo 2148  df-clab 2270  df-cleq 2276  df-clel 2279  df-nfc 2408  df-ne 2448  df-ral 2548  df-rex 2549  df-reu 2550  df-rab 2552  df-v 2790  df-sbc 2992  df-csb 3082  df-dif 3155  df-un 3157  df-in 3159  df-ss 3166  df-nul 3456  df-if 3566  df-pw 3627  df-sn 3646  df-pr 3647  df-op 3649  df-uni 3828  df-iun 3907  df-br 4024  df-opab 4078  df-mpt 4079  df-id 4309  df-xp 4695  df-rel 4696  df-cnv 4697  df-co 4698  df-dm 4699  df-rn 4700  df-res 4701  df-ima 4702  df-iota 5219  df-fun 5257  df-fn 5258  df-f 5259  df-f1 5260  df-fo 5261  df-f1o 5262  df-fv 5263  df-ov 5861  df-oprab 5862  df-mpt2 5863  df-1st 6122  df-2nd 6123  df-riota 6304  df-grpo 20858  df-gid 20859  df-ginv 20860  df-gdiv 20861  df-ghom 21025
 Copyright terms: Public domain W3C validator