Mathbox for Paul Chapman < Previous   Next > Nearby theorems Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  ghomgsg Structured version   Unicode version

Theorem ghomgsg 30306
 Description: A group homomorphism from to is also a group homomorphism from to its image in . (Contributed by Paul Chapman, 3-Mar-2008.)
Hypotheses
Ref Expression
ghomgsg.1
ghomgsg.2
Assertion
Ref Expression
ghomgsg GrpOpHom GrpOpHom

Proof of Theorem ghomgsg
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2422 . . . 4
2 ghomgsg.1 . . . 4
3 ghomgsg.2 . . . 4
4 eqid 2422 . . . 4
51, 2, 3, 4ghomfo 30304 . . 3 GrpOpHom
6 fof 5806 . . 3
75, 6syl 17 . 2 GrpOpHom
8 eqid 2422 . . . . . 6
91, 8elghomOLD 26076 . . . . 5 GrpOpHom
109biimp3a 1364 . . . 4 GrpOpHom
1110simprd 464 . . 3 GrpOpHom
12 ffvelrn 6031 . . . . . . . 8
13 ffvelrn 6031 . . . . . . . 8
1412, 13anim12dan 845 . . . . . . 7
157, 14sylan 473 . . . . . 6 GrpOpHom
162, 3ghomgrp 30303 . . . . . . 7 GrpOpHom
174subgoov 26018 . . . . . . 7
1816, 17sylan 473 . . . . . 6 GrpOpHom
1915, 18syldan 472 . . . . 5 GrpOpHom
2019eqeq1d 2424 . . . 4 GrpOpHom
21202ralbidva 2867 . . 3 GrpOpHom
2211, 21mpbird 235 . 2 GrpOpHom
23 issubgo 26016 . . . . 5
2416, 23sylib 199 . . . 4 GrpOpHom
2524simp2d 1018 . . 3 GrpOpHom
261, 4elghomOLD 26076 . . . . 5 GrpOpHom
2726biimprd 226 . . . 4 GrpOpHom
28273adant3 1025 . . 3 GrpOpHom GrpOpHom
2925, 28syld3an2 1311 . 2 GrpOpHom GrpOpHom
307, 22, 29mp2and 683 1 GrpOpHom GrpOpHom
 Colors of variables: wff setvar class Syntax hints:   wi 4   wa 370   w3a 982   wceq 1437   wcel 1868  wral 2775   wss 3436   cxp 4847   crn 4850   cres 4851  wf 5593  wfo 5595  cfv 5597  (class class class)co 6301  cgr 25899  csubgo 26014   GrpOpHom cghomOLD 26070 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1665  ax-4 1678  ax-5 1748  ax-6 1794  ax-7 1839  ax-8 1870  ax-9 1872  ax-10 1887  ax-11 1892  ax-12 1905  ax-13 2053  ax-ext 2400  ax-rep 4533  ax-sep 4543  ax-nul 4551  ax-pow 4598  ax-pr 4656  ax-un 6593 This theorem depends on definitions:  df-bi 188  df-or 371  df-an 372  df-3an 984  df-tru 1440  df-ex 1660  df-nf 1664  df-sb 1787  df-eu 2269  df-mo 2270  df-clab 2408  df-cleq 2414  df-clel 2417  df-nfc 2572  df-ne 2620  df-ral 2780  df-rex 2781  df-reu 2782  df-rab 2784  df-v 3083  df-sbc 3300  df-csb 3396  df-dif 3439  df-un 3441  df-in 3443  df-ss 3450  df-nul 3762  df-if 3910  df-pw 3981  df-sn 3997  df-pr 3999  df-op 4003  df-uni 4217  df-iun 4298  df-br 4421  df-opab 4480  df-mpt 4481  df-id 4764  df-xp 4855  df-rel 4856  df-cnv 4857  df-co 4858  df-dm 4859  df-rn 4860  df-res 4861  df-ima 4862  df-iota 5561  df-fun 5599  df-fn 5600  df-f 5601  df-f1 5602  df-fo 5603  df-f1o 5604  df-fv 5605  df-riota 6263  df-ov 6304  df-oprab 6305  df-mpt2 6306  df-grpo 25904  df-gid 25905  df-ginv 25906  df-subgo 26015  df-ghomOLD 26071 This theorem is referenced by: (None)
 Copyright terms: Public domain W3C validator