Theorem ghmf 19203

Description: A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014.)

Hypotheses

Ref	Expression
ghmf.x	⊢ 𝑋 = (Base‘𝑆)
ghmf.y	⊢ 𝑌 = (Base‘𝑇)

Assertion

Ref	Expression
ghmf	⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌)

Proof of Theorem ghmf

Dummy variables 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		ghmf.x	. . . 4 ⊢ 𝑋 = (Base‘𝑆)
2		ghmf.y	. . . 4 ⊢ 𝑌 = (Base‘𝑇)
3		eqid 2735	. . . 4 ⊢ (+g‘𝑆) = (+g‘𝑆)
4		eqid 2735	. . . 4 ⊢ (+g‘𝑇) = (+g‘𝑇)
5	1, 2, 3, 4	isghm 19198	. . 3 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) ↔ ((𝑆 ∈ Grp ∧ 𝑇 ∈ Grp) ∧ (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘(𝑦(+g‘𝑆)𝑥)) = ((𝐹‘𝑦)(+g‘𝑇)(𝐹‘𝑥)))))
6	5	simprbi 496	. 2 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → (𝐹:𝑋⟶𝑌 ∧ ∀𝑦 ∈ 𝑋 ∀𝑥 ∈ 𝑋 (𝐹‘(𝑦(+g‘𝑆)𝑥)) = ((𝐹‘𝑦)(+g‘𝑇)(𝐹‘𝑥))))
7	6	simpld 494	1 ⊢ (𝐹 ∈ (𝑆 GrpHom 𝑇) → 𝐹:𝑋⟶𝑌)

Syntax hints:   → wi 4   ∧ wa 395   = wceq 1540   ∈ wcel 2108  ∀wral 3051  ⟶wf 6527  ‘cfv 6531  (class class class)co 7405  Basecbs 17228  +_gcplusg 17271  Grpcgrp 18916   GrpHom cghm 19195

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1795  ax-4 1809  ax-5 1910  ax-6 1967  ax-7 2007  ax-8 2110  ax-9 2118  ax-10 2141  ax-11 2157  ax-12 2177  ax-ext 2707  ax-sep 5266  ax-nul 5276  ax-pow 5335  ax-pr 5402  ax-un 7729

This theorem depends on definitions:  df-bi 207  df-an 396  df-or 848  df-3an 1088  df-tru 1543  df-fal 1553  df-ex 1780  df-nf 1784  df-sb 2065  df-mo 2539  df-eu 2568  df-clab 2714  df-cleq 2727  df-clel 2809  df-nfc 2885  df-ne 2933  df-ral 3052  df-rex 3061  df-rab 3416  df-v 3461  df-sbc 3766  df-csb 3875  df-dif 3929  df-un 3931  df-in 3933  df-ss 3943  df-nul 4309  df-if 4501  df-pw 4577  df-sn 4602  df-pr 4604  df-op 4608  df-uni 4884  df-iun 4969  df-br 5120  df-opab 5182  df-mpt 5202  df-id 5548  df-xp 5660  df-rel 5661  df-cnv 5662  df-co 5663  df-dm 5664  df-rn 5665  df-res 5666  df-ima 5667  df-iota 6484  df-fun 6533  df-fn 6534  df-f 6535  df-fv 6539  df-ov 7408  df-oprab 7409  df-mpo 7410  df-1st 7988  df-2nd 7989  df-map 8842  df-ghm 19196

This theorem is referenced by:  ghmid  19205  ghminv  19206  ghmsub  19207  ghmmhm  19209  ghmmulg  19211  ghmrn  19212  resghm  19215  ghmpreima  19221  ghmeql  19222  ghmnsgima  19223  ghmnsgpreima  19224  ghmeqker  19226  ghmf1  19229  kerf1ghm  19230  ghmf1o  19231  gimcnv  19250  ghmqusnsglem1  19263  ghmqusnsg  19265  ghmquskerlem1  19266  ghmquskerco  19267  ghmquskerlem3  19269  ghmqusker  19270  lactghmga  19386  frgpup3lem  19758  frgpup3  19759  ghmplusg  19827  isrnghmmul  20402  rnghmf  20408  rhmf  20445  isrhm2d  20447  lmhmf  20992  lmhmpropd  21031  frgpcyg  21534  psgninv  21542  zrhpsgninv  21545  evpmss  21546  psgnevpmb  21547  psgnodpm  21548  zrhpsgnevpm  21551  zrhpsgnodpm  21552  evlslem2  22037  nmoi  24667  nmoix  24668  nmoi2  24669  nmoleub  24670  nmoeq0  24675  nmoco  24676  nmotri  24678  nmods  24683  nghmcn  24684  aks6d1c1p2  42122  aks6d1c1p3  42123  aks6d1c5lem1  42149