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

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 1 elghomlem1OLD ⊢G∈GrpOp∧H∈GrpOp→GGrpOpHomH=S
3 2 eleq2d ⊢G∈GrpOp∧H∈GrpOp→F∈GGrpOpHomH↔F∈S
4 elex ⊢F∈S→F∈V
5 feq1 ⊢f=F→f:ran⁡G⟶ran⁡H↔F:ran⁡G⟶ran⁡H
6 fveq1 ⊢f=F→f⁡x=F⁡x
7 fveq1 ⊢f=F→f⁡y=F⁡y
8 6 7 oveq12d ⊢f=F→f⁡xHf⁡y=F⁡xHF⁡y
9 fveq1 ⊢f=F→f⁡xGy=F⁡xGy
10 8 9 eqeq12d ⊢f=F→f⁡xHf⁡y=f⁡xGy↔F⁡xHF⁡y=F⁡xGy
11 10 2ralbidv ⊢f=F→∀x∈ran⁡G∀y∈ran⁡Gf⁡xHf⁡y=f⁡xGy↔∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
12 5 11 anbi12d ⊢f=F→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
13 12 1 elab2g ⊢F∈V→F∈S↔F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
14 13 biimpd ⊢F∈V→F∈S→F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
15 4 14 mpcom ⊢F∈S→F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
16 rnexg ⊢G∈GrpOp→ran⁡G∈V
17 fex ⊢F:ran⁡G⟶ran⁡H∧ran⁡G∈V→F∈V
18 17 expcom ⊢ran⁡G∈V→F:ran⁡G⟶ran⁡H→F∈V
19 16 18 syl ⊢G∈GrpOp→F:ran⁡G⟶ran⁡H→F∈V
20 19 adantrd ⊢G∈GrpOp→F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy→F∈V
21 13 biimprd ⊢F∈V→F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy→F∈S
22 20 21 syli ⊢G∈GrpOp→F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy→F∈S
23 15 22 impbid2 ⊢G∈GrpOp→F∈S↔F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
24 23 adantr ⊢G∈GrpOp∧H∈GrpOp→F∈S↔F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
25 3 24 bitrd ⊢G∈GrpOp∧H∈GrpOp→F∈GGrpOpHomH↔F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy