Metamath Proof Explorer

Theorem elghomOLD

Description: Obsolete version of isghm as of 15-Mar-2020. Membership in the set of group homomorphisms from G to H . (Contributed by Paul Chapman, 3-Mar-2008) (New usage is discouraged.) (Proof modification is discouraged.)

Ref Expression
Hypotheses elghomOLD.1 ⊢X=ran⁡G
elghomOLD.2 ⊢W=ran⁡H
Assertion elghomOLD ⊢G∈GrpOp∧H∈GrpOp→F∈GGrpOpHomH↔F:X⟶W∧∀x∈X∀y∈XF⁡xHF⁡y=F⁡xGy

Proof

Step Hyp Ref Expression
1 elghomOLD.1 ⊢X=ran⁡G
2 elghomOLD.2 ⊢W=ran⁡H
3 eqid ⊢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
4 3 elghomlem2OLD ⊢G∈GrpOp∧H∈GrpOp→F∈GGrpOpHomH↔F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
5 1 2 feq23i ⊢F:X⟶W↔F:ran⁡G⟶ran⁡H
6 1 raleqi ⊢∀y∈XF⁡xHF⁡y=F⁡xGy↔∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
7 1 6 raleqbii ⊢∀x∈X∀y∈XF⁡xHF⁡y=F⁡xGy↔∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
8 5 7 anbi12i ⊢F:X⟶W∧∀x∈X∀y∈XF⁡xHF⁡y=F⁡xGy↔F:ran⁡G⟶ran⁡H∧∀x∈ran⁡G∀y∈ran⁡GF⁡xHF⁡y=F⁡xGy
9 4 8 bitr4di ⊢G∈GrpOp∧H∈GrpOp→F∈GGrpOpHomH↔F:X⟶W∧∀x∈X∀y∈XF⁡xHF⁡y=F⁡xGy