# Metamath Proof Explorer

## Theorem ghmgrp1

Description: A group homomorphism is only defined when the domain is a group. (Contributed by Stefan O'Rear, 31-Dec-2014)

Ref Expression
Assertion ghmgrp1 ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {S}\in \mathrm{Grp}$

### Proof

Step Hyp Ref Expression
1 eqid ${⊢}{\mathrm{Base}}_{{S}}={\mathrm{Base}}_{{S}}$
2 eqid ${⊢}{\mathrm{Base}}_{{T}}={\mathrm{Base}}_{{T}}$
3 eqid ${⊢}{+}_{{S}}={+}_{{S}}$
4 eqid ${⊢}{+}_{{T}}={+}_{{T}}$
5 1 2 3 4 isghm ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)↔\left(\left({S}\in \mathrm{Grp}\wedge {T}\in \mathrm{Grp}\right)\wedge \left({F}:{\mathrm{Base}}_{{S}}⟶{\mathrm{Base}}_{{T}}\wedge \forall {y}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}\forall {x}\in {\mathrm{Base}}_{{S}}\phantom{\rule{.4em}{0ex}}{F}\left({y}{+}_{{S}}{x}\right)={F}\left({y}\right){+}_{{T}}{F}\left({x}\right)\right)\right)$
6 5 simplbi ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to \left({S}\in \mathrm{Grp}\wedge {T}\in \mathrm{Grp}\right)$
7 6 simpld ${⊢}{F}\in \left({S}\mathrm{GrpHom}{T}\right)\to {S}\in \mathrm{Grp}$