# Metamath Proof Explorer

## Definition df-ghomOLD

Description: Obsolete version of df-ghm as of 15-Mar-2020. Define the set of group homomorphisms from g to h . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.)

Ref Expression
Assertion df-ghomOLD ${⊢}\mathrm{GrpOpHom}=\left({g}\in \mathrm{GrpOp},{h}\in \mathrm{GrpOp}⟼\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\}\right)$

### Detailed syntax breakdown

Step Hyp Ref Expression
0 cghomOLD ${class}\mathrm{GrpOpHom}$
1 vg ${setvar}{g}$
2 cgr ${class}\mathrm{GrpOp}$
3 vh ${setvar}{h}$
4 vf ${setvar}{f}$
5 4 cv ${setvar}{f}$
6 1 cv ${setvar}{g}$
7 6 crn ${class}\mathrm{ran}{g}$
8 3 cv ${setvar}{h}$
9 8 crn ${class}\mathrm{ran}{h}$
10 7 9 5 wf ${wff}{f}:\mathrm{ran}{g}⟶\mathrm{ran}{h}$
11 vx ${setvar}{x}$
12 vy ${setvar}{y}$
13 11 cv ${setvar}{x}$
14 13 5 cfv ${class}{f}\left({x}\right)$
15 12 cv ${setvar}{y}$
16 15 5 cfv ${class}{f}\left({y}\right)$
17 14 16 8 co ${class}\left({f}\left({x}\right){h}{f}\left({y}\right)\right)$
18 13 15 6 co ${class}\left({x}{g}{y}\right)$
19 18 5 cfv ${class}{f}\left({x}{g}{y}\right)$
20 17 19 wceq ${wff}{f}\left({x}\right){h}{f}\left({y}\right)={f}\left({x}{g}{y}\right)$
21 20 12 7 wral ${wff}\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)$
22 21 11 7 wral ${wff}\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)$
23 10 22 wa ${wff}\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)$
24 23 4 cab ${class}\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\}$
25 1 3 2 2 24 cmpo ${class}\left({g}\in \mathrm{GrpOp},{h}\in \mathrm{GrpOp}⟼\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\}\right)$
26 0 25 wceq ${wff}\mathrm{GrpOpHom}=\left({g}\in \mathrm{GrpOp},{h}\in \mathrm{GrpOp}⟼\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\}\right)$