# Metamath Proof Explorer

## Theorem ghomf

Description: Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009)

Ref Expression
Hypotheses ghomf.1 ${⊢}{X}=\mathrm{ran}{G}$
ghomf.2 ${⊢}{W}=\mathrm{ran}{H}$
Assertion ghomf ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}:{X}⟶{W}$

### Proof

Step Hyp Ref Expression
1 ghomf.1 ${⊢}{X}=\mathrm{ran}{G}$
2 ghomf.2 ${⊢}{W}=\mathrm{ran}{H}$
3 1 2 elghomOLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({F}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔\left({F}:{X}⟶{W}\wedge \forall {x}\in {X}\phantom{\rule{.4em}{0ex}}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)\right)$
4 3 simprbda ${⊢}\left(\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}:{X}⟶{W}$
5 4 3impa ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {F}\in \left({G}\mathrm{GrpOpHom}{H}\right)\right)\to {F}:{X}⟶{W}$