MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  ghmgrp1 Structured version   Unicode version

Theorem ghmgrp1 15738
Description: A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Assertion
Ref Expression
ghmgrp1  |-  ( F  e.  ( S  GrpHom  T )  ->  S  e.  Grp )

Proof of Theorem ghmgrp1
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 eqid 2437 . . . 4  |-  ( Base `  S )  =  (
Base `  S )
2 eqid 2437 . . . 4  |-  ( Base `  T )  =  (
Base `  T )
3 eqid 2437 . . . 4  |-  ( +g  `  S )  =  ( +g  `  S )
4 eqid 2437 . . . 4  |-  ( +g  `  T )  =  ( +g  `  T )
51, 2, 3, 4isghm 15736 . . 3  |-  ( F  e.  ( S  GrpHom  T )  <->  ( ( S  e.  Grp  /\  T  e.  Grp )  /\  ( F : ( Base `  S
) --> ( Base `  T
)  /\  A. y  e.  ( Base `  S
) A. x  e.  ( Base `  S
) ( F `  ( y ( +g  `  S ) x ) )  =  ( ( F `  y ) ( +g  `  T
) ( F `  x ) ) ) ) )
65simplbi 460 . 2  |-  ( F  e.  ( S  GrpHom  T )  ->  ( S  e.  Grp  /\  T  e. 
Grp ) )
76simpld 459 1  |-  ( F  e.  ( S  GrpHom  T )  ->  S  e.  Grp )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 369    = wceq 1369    e. wcel 1756   A.wral 2709   -->wf 5407   ` cfv 5411  (class class class)co 6086   Basecbs 14166   +g cplusg 14230   Grpcgrp 15402    GrpHom cghm 15733
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1591  ax-4 1602  ax-5 1670  ax-6 1708  ax-7 1728  ax-8 1758  ax-9 1760  ax-10 1775  ax-11 1780  ax-12 1792  ax-13 1943  ax-ext 2418  ax-rep 4396  ax-sep 4406  ax-nul 4414  ax-pow 4463  ax-pr 4524  ax-un 6367
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3an 967  df-tru 1372  df-ex 1587  df-nf 1590  df-sb 1701  df-eu 2256  df-mo 2257  df-clab 2424  df-cleq 2430  df-clel 2433  df-nfc 2562  df-ne 2602  df-ral 2714  df-rex 2715  df-reu 2716  df-rab 2718  df-v 2968  df-sbc 3180  df-csb 3282  df-dif 3324  df-un 3326  df-in 3328  df-ss 3335  df-nul 3631  df-if 3785  df-pw 3855  df-sn 3871  df-pr 3873  df-op 3877  df-uni 4085  df-iun 4166  df-br 4286  df-opab 4344  df-mpt 4345  df-id 4628  df-xp 4838  df-rel 4839  df-cnv 4840  df-co 4841  df-dm 4842  df-rn 4843  df-res 4844  df-ima 4845  df-iota 5374  df-fun 5413  df-fn 5414  df-f 5415  df-f1 5416  df-fo 5417  df-f1o 5418  df-fv 5419  df-ov 6089  df-oprab 6090  df-mpt2 6091  df-ghm 15734
This theorem is referenced by:  ghmid  15742  ghminv  15743  ghmsub  15744  ghmmhm  15746  ghmmulg  15748  ghmrn  15749  resghm2  15753  resghm2b  15754  ghmco  15755  ghmpreima  15757  ghmeql  15758  ghmnsgima  15759  ghmnsgpreima  15760  ghmeqker  15762  ghmf1  15764  ghmf1o  15765  ghmpropd  15773  isgim  15779  giclcl  15789  lactghmga  15898  invghm  16307  ghmplusg  16317  evl1addd  17744  evl1subd  17745  ghmcnp  19654  gicabl  29397
  Copyright terms: Public domain W3C validator