# Metamath Proof Explorer

## Theorem elghomlem2OLD

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 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)$

### 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 1 elghomlem1OLD ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to {G}\mathrm{GrpOpHom}{H}={S}$
3 2 eleq2d ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({F}\in \left({G}\mathrm{GrpOpHom}{H}\right)↔{F}\in {S}\right)$
4 elex ${⊢}{F}\in {S}\to {F}\in \mathrm{V}$
5 feq1 ${⊢}{f}={F}\to \left({f}:\mathrm{ran}{G}⟶\mathrm{ran}{H}↔{F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\right)$
6 fveq1 ${⊢}{f}={F}\to {f}\left({x}\right)={F}\left({x}\right)$
7 fveq1 ${⊢}{f}={F}\to {f}\left({y}\right)={F}\left({y}\right)$
8 6 7 oveq12d ${⊢}{f}={F}\to {f}\left({x}\right){H}{f}\left({y}\right)={F}\left({x}\right){H}{F}\left({y}\right)$
9 fveq1 ${⊢}{f}={F}\to {f}\left({x}{G}{y}\right)={F}\left({x}{G}{y}\right)$
10 8 9 eqeq12d ${⊢}{f}={F}\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 10 2ralbidv ${⊢}{f}={F}\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)$
12 5 11 anbi12d ${⊢}{f}={F}\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)$
13 12 1 elab2g ${⊢}{F}\in \mathrm{V}\to \left({F}\in {S}↔\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 biimpd ${⊢}{F}\in \mathrm{V}\to \left({F}\in {S}\to \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 4 14 mpcom ${⊢}{F}\in {S}\to \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)$
16 rnexg ${⊢}{G}\in \mathrm{GrpOp}\to \mathrm{ran}{G}\in \mathrm{V}$
17 fex ${⊢}\left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\wedge \mathrm{ran}{G}\in \mathrm{V}\right)\to {F}\in \mathrm{V}$
18 17 expcom ${⊢}\mathrm{ran}{G}\in \mathrm{V}\to \left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\to {F}\in \mathrm{V}\right)$
19 16 18 syl ${⊢}{G}\in \mathrm{GrpOp}\to \left({F}:\mathrm{ran}{G}⟶\mathrm{ran}{H}\to {F}\in \mathrm{V}\right)$
20 19 adantrd ${⊢}{G}\in \mathrm{GrpOp}\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)\to {F}\in \mathrm{V}\right)$
21 13 biimprd ${⊢}{F}\in \mathrm{V}\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)\to {F}\in {S}\right)$
22 20 21 syli ${⊢}{G}\in \mathrm{GrpOp}\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)\to {F}\in {S}\right)$
23 15 22 impbid2 ${⊢}{G}\in \mathrm{GrpOp}\to \left({F}\in {S}↔\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)$
24 23 adantr ${⊢}\left({G}\in \mathrm{GrpOp}\wedge {H}\in \mathrm{GrpOp}\right)\to \left({F}\in {S}↔\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 3 24 bitrd ${⊢}\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)$