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 ∈ G GrpOpHom H ↔ F : X ⟶ W ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y

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 ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y = f | f : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G f ⁡ x H f ⁡ y = f ⁡ x G y
4 3 elghomlem2OLD ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ G GrpOpHom H ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
5 1 2 feq23i ⊢ F : X ⟶ W ↔ F : ran ⁡ G ⟶ ran ⁡ H
6 1 raleqi ⊢ ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y ↔ ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
7 1 6 raleqbii ⊢ ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y ↔ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
8 5 7 anbi12i ⊢ F : X ⟶ W ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y ↔ F : ran ⁡ G ⟶ ran ⁡ H ∧ ∀ x ∈ ran ⁡ G ∀ y ∈ ran ⁡ G F ⁡ x H F ⁡ y = F ⁡ x G y
9 4 8 bitr4di ⊢ G ∈ GrpOp ∧ H ∈ GrpOp → F ∈ G GrpOpHom H ↔ F : X ⟶ W ∧ ∀ x ∈ X ∀ y ∈ X F ⁡ x H F ⁡ y = F ⁡ x G y