# Metamath Proof Explorer

## Theorem elghomOLD

Description: Obsolete version of isghm as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H . (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses elghomOLD.1 ${⊢}{X}=\mathrm{ran}{G}$
elghomOLD.2 ${⊢}{W}=\mathrm{ran}{H}$
Assertion 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)$

### Proof

Step Hyp Ref Expression
1 elghomOLD.1 ${⊢}{X}=\mathrm{ran}{G}$
2 elghomOLD.2 ${⊢}{W}=\mathrm{ran}{H}$
3 eqid ${⊢}\left\{{f}|\left({f}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){H}{f}\left({y}\right)={f}\left({x}{G}{y}\right)\right)\right\}=\left\{{f}|\left({f}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{f}\left({x}\right){H}{f}\left({y}\right)={f}\left({x}{G}{y}\right)\right)\right\}$
4 3 elghomlem2OLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({F}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔\left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)\right)$
5 1 2 feq23i ${⊢}{F}:{X}⟶{W}↔{F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}$
6 1 raleqi ${⊢}\forall {y}\in {X}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)↔\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)$
7 1 6 raleqbii ${⊢}\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)↔\forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)$
8 5 7 anbi12i ${⊢}\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)↔\left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \forall {x}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}\forall {y}\in \mathrm{ran}{G}\phantom{\rule{.4em}{0ex}}{F}\left({x}\right){H}{F}\left({y}\right)={F}\left({x}{G}{y}\right)\right)$
9 4 8 syl6bbr ${⊢}\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)$