Metamath Proof Explorer

Theorem ghomf

Description: Mapping property of a group homomorphism. (Contributed by Jeff Madsen, 1-Dec-2009)

Ref Expression
Hypotheses ghomf.1 ⊢ X = ran ⁡ G
ghomf.2 ⊢ W = ran ⁡ H
Assertion ghomf ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H → F : X ⟶ W

Proof

Step Hyp Ref Expression
1 ghomf.1 ⊢ X = ran ⁡ G
2 ghomf.2 ⊢ W = ran ⁡ H
3 1 2 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
4 3 simprbda ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H → F : X ⟶ W
5 4 3impa ⊢ G ∈ GrpOp ∧ H ∈ GrpOp ∧ F ∈ G GrpOpHom H → F : X ⟶ W