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=f|f:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xHf⁡y=f⁡xGy
Assertion elghomlem1OLD ⊢G∈GrpOp∧H∈GrpOp→GGrpOpHomH=S

Proof

Step Hyp Ref Expression
1 elghomlem1OLD.1 ⊢S=f|f:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xHf⁡y=f⁡xGy
2 rnexg ⊢G∈GrpOp→ran⁡G∈V
3 rnexg ⊢H∈GrpOp→ran⁡H∈V
4 1 fabexg ⊢ran⁡G∈V∧ran⁡H∈V→S∈V
5 2 3 4 syl2an ⊢G∈GrpOp∧H∈GrpOp→S∈V
6 rneq ⊢g=G→ran⁡g=ran⁡G
7 6 feq2d ⊢g=G→f:ran⁡g⟶ran⁡h↔f:ran⁡G⟶ran⁡h
8 oveq ⊢g=G→xgy=xGy
9 8 fveq2d ⊢g=G→f⁡xgy=f⁡xGy
10 9 eqeq2d ⊢g=G→f⁡xhf⁡y=f⁡xgy↔f⁡xhf⁡y=f⁡xGy
11 6 10 raleqbidv ⊢g=G→∀y∈ran⁡gf⁡xhf⁡y=f⁡xgy↔∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy
12 6 11 raleqbidv ⊢g=G→∀x∈ran⁡g∀y∈ran⁡gf⁡xhf⁡y=f⁡xgy↔∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy
13 7 12 anbi12d ⊢g=G→f:ran⁡g⟶ran⁡h∧∀x∈ran⁡g∀y∈ran⁡gf⁡xhf⁡y=f⁡xgy↔f:ran⁡G⟶ran⁡h∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy
14 13 abbidv ⊢g=G→f|f:ran⁡g⟶ran⁡h∧∀x∈ran⁡g∀y∈ran⁡gf⁡xhf⁡y=f⁡xgy=f|f:ran⁡G⟶ran⁡h∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy
15 rneq ⊢h=H→ran⁡h=ran⁡H
16 15 feq3d ⊢h=H→f:ran⁡G⟶ran⁡h↔f:ran⁡G⟶ran⁡H
17 oveq ⊢h=H→f⁡xhf⁡y=f⁡xHf⁡y
18 17 eqeq1d ⊢h=H→f⁡xhf⁡y=f⁡xGy↔f⁡xHf⁡y=f⁡xGy
19 18 2ralbidv ⊢h=H→∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy↔∀x∈ran⁡G∀y∈ran⁡Gf⁡xHf⁡y=f⁡xGy
20 16 19 anbi12d ⊢h=H→f:ran⁡G⟶ran⁡h∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy↔f:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xHf⁡y=f⁡xGy
21 20 abbidv ⊢h=H→f|f:ran⁡G⟶ran⁡h∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy=f|f:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xHf⁡y=f⁡xGy
22 21 1 eqtr4di ⊢h=H→f|f:ran⁡G⟶ran⁡h∧∀x∈ran⁡G∀y∈ran⁡Gf⁡xhf⁡y=f⁡xGy=S
23 df-ghomOLD ⊢GrpOpHom=g∈GrpOp,h∈GrpOp⟼f|f:ran⁡g⟶ran⁡h∧∀x∈ran⁡g∀y∈ran⁡gf⁡xhf⁡y=f⁡xgy
24 14 22 23 ovmpog ⊢G∈GrpOp∧H∈GrpOp∧S∈V→GGrpOpHomH=S
25 5 24 mpd3an3 ⊢G∈GrpOp∧H∈GrpOp→GGrpOpHomH=S