# Metamath Proof Explorer

## Theorem elghomlem1OLD

Description: Obsolete as of 15-Mar-2020. Lemma for elghomOLD . (Contributed by Paul Chapman, 25-Feb-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypothesis elghomlem1OLD.1 ${⊢}{S}=\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\}$
Assertion elghomlem1OLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to {G}\mathrm{GrpOpHom}{H}={S}$

### Proof

Step Hyp Ref Expression
1 elghomlem1OLD.1 ${⊢}{S}=\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\}$
2 rnexg ${⊢}{G}\in \mathrm{GrpOp}\to \mathrm{ran}{G}\in \mathrm{V}$
3 rnexg ${⊢}{H}\in \mathrm{GrpOp}\to \mathrm{ran}{H}\in \mathrm{V}$
4 1 fabexg ${⊢}\left(\mathrm{ran}{G}\in \mathrm{V}\wedge \mathrm{ran}{H}\in \mathrm{V}\right)\to {S}\in \mathrm{V}$
5 2 3 4 syl2an ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to {S}\in \mathrm{V}$
6 rneq ${⊢}{g}={G}\to \mathrm{ran}{g}=\mathrm{ran}{G}$
7 6 feq2d ${⊢}{g}={G}\to \left({f}:\mathrm{ran}{g}⟶\mathrm{ran}{h}↔{f}:\mathrm{ran}{G}⟶\mathrm{ran}{h}\right)$
8 oveq ${⊢}{g}={G}\to {x}{g}{y}={x}{G}{y}$
9 8 fveq2d ${⊢}{g}={G}\to {f}\left({x}{g}{y}\right)={f}\left({x}{G}{y}\right)$
10 9 eqeq2d ${⊢}{g}={G}\to \left({f}\left({x}\right){h}{f}\left({y}\right)={f}\left({x}{g}{y}\right)↔{f}\left({x}\right){h}{f}\left({y}\right)={f}\left({x}{G}{y}\right)\right)$
11 6 10 raleqbidv ${⊢}{g}={G}\to \left(\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)↔\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)$
12 6 11 raleqbidv ${⊢}{g}={G}\to \left(\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)↔\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)$
13 7 12 anbi12d ${⊢}{g}={G}\to \left(\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)↔\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)$
14 13 abbidv ${⊢}{g}={G}\to \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\}$
15 rneq ${⊢}{h}={H}\to \mathrm{ran}{h}=\mathrm{ran}{H}$
16 15 feq3d ${⊢}{h}={H}\to \left({f}:\mathrm{ran}{G}⟶\mathrm{ran}{h}↔{f}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\right)$
17 oveq ${⊢}{h}={H}\to {f}\left({x}\right){h}{f}\left({y}\right)={f}\left({x}\right){H}{f}\left({y}\right)$
18 17 eqeq1d ${⊢}{h}={H}\to \left({f}\left({x}\right){h}{f}\left({y}\right)={f}\left({x}{G}{y}\right)↔{f}\left({x}\right){H}{f}\left({y}\right)={f}\left({x}{G}{y}\right)\right)$
19 18 2ralbidv ${⊢}{h}={H}\to \left(\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)↔\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)$
20 16 19 anbi12d ${⊢}{h}={H}\to \left(\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)↔\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)$
21 20 abbidv ${⊢}{h}={H}\to \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\}$
22 21 1 eqtr4di ${⊢}{h}={H}\to \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\}={S}$
23 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)$
24 14 22 23 ovmpog ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\wedge {S}\in \mathrm{V}\right)\to {G}\mathrm{GrpOpHom}{H}={S}$
25 5 24 mpd3an3 ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to {G}\mathrm{GrpOpHom}{H}={S}$