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

Theorem ghmf 16593
Description: A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)
Hypotheses
Ref Expression
ghmf.x  |-  X  =  ( Base `  S
)
ghmf.y  |-  Y  =  ( Base `  T
)
Assertion
Ref Expression
ghmf  |-  ( F  e.  ( S  GrpHom  T )  ->  F : X
--> Y )

Proof of Theorem ghmf
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 ghmf.x . . . 4  |-  X  =  ( Base `  S
)
2 ghmf.y . . . 4  |-  Y  =  ( Base `  T
)
3 eqid 2402 . . . 4  |-  ( +g  `  S )  =  ( +g  `  S )
4 eqid 2402 . . . 4  |-  ( +g  `  T )  =  ( +g  `  T )
51, 2, 3, 4isghm 16589 . . 3  |-  ( F  e.  ( S  GrpHom  T )  <->  ( ( S  e.  Grp  /\  T  e.  Grp )  /\  ( F : X --> Y  /\  A. y  e.  X  A. x  e.  X  ( F `  ( y
( +g  `  S ) x ) )  =  ( ( F `  y ) ( +g  `  T ) ( F `
 x ) ) ) ) )
65simprbi 462 . 2  |-  ( F  e.  ( S  GrpHom  T )  ->  ( F : X --> Y  /\  A. y  e.  X  A. x  e.  X  ( F `  ( y
( +g  `  S ) x ) )  =  ( ( F `  y ) ( +g  `  T ) ( F `
 x ) ) ) )
76simpld 457 1  |-  ( F  e.  ( S  GrpHom  T )  ->  F : X
--> Y )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    /\ wa 367    = wceq 1405    e. wcel 1842   A.wral 2753   -->wf 5564   ` cfv 5568  (class class class)co 6277   Basecbs 14839   +g cplusg 14907   Grpcgrp 16375    GrpHom cghm 16586
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1639  ax-4 1652  ax-5 1725  ax-6 1771  ax-7 1814  ax-8 1844  ax-9 1846  ax-10 1861  ax-11 1866  ax-12 1878  ax-13 2026  ax-ext 2380  ax-rep 4506  ax-sep 4516  ax-nul 4524  ax-pow 4571  ax-pr 4629  ax-un 6573
This theorem depends on definitions:  df-bi 185  df-or 368  df-an 369  df-3an 976  df-tru 1408  df-ex 1634  df-nf 1638  df-sb 1764  df-eu 2242  df-mo 2243  df-clab 2388  df-cleq 2394  df-clel 2397  df-nfc 2552  df-ne 2600  df-ral 2758  df-rex 2759  df-reu 2760  df-rab 2762  df-v 3060  df-sbc 3277  df-csb 3373  df-dif 3416  df-un 3418  df-in 3420  df-ss 3427  df-nul 3738  df-if 3885  df-pw 3956  df-sn 3972  df-pr 3974  df-op 3978  df-uni 4191  df-iun 4272  df-br 4395  df-opab 4453  df-mpt 4454  df-id 4737  df-xp 4828  df-rel 4829  df-cnv 4830  df-co 4831  df-dm 4832  df-rn 4833  df-res 4834  df-ima 4835  df-iota 5532  df-fun 5570  df-fn 5571  df-f 5572  df-f1 5573  df-fo 5574  df-f1o 5575  df-fv 5576  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-ghm 16587
This theorem is referenced by:  ghmid  16595  ghminv  16596  ghmsub  16597  ghmmhm  16599  ghmmulg  16601  ghmrn  16602  resghm  16605  ghmpreima  16610  ghmeql  16611  ghmnsgima  16612  ghmnsgpreima  16613  ghmeqker  16615  ghmf1  16617  ghmf1o  16618  gimcnv  16637  lactghmga  16751  frgpup3lem  17117  frgpup3  17118  ghmplusg  17174  rhmf  17693  isrhm2d  17695  lmhmf  17998  lmhmpropd  18037  evlslem2  18498  frgpcyg  18908  psgninv  18914  zrhpsgninv  18917  evpmss  18918  psgnevpmb  18919  psgnodpm  18920  zrhpsgnevpm  18923  zrhpsgnodpm  18924  nmoi  21525  nmoix  21526  nmoi2  21527  nmoleub  21528  nmoeq0  21533  nmoco  21534  nmotri  21536  nmods  21541  nghmcn  21542  isrnghmmul  38191  rnghmf  38197
  Copyright terms: Public domain W3C validator