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 \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F : X ⟶ W$

Step	Hyp	Ref	Expression
1		ghomf.1	$⊢ X = ran G$
2		ghomf.2	$⊢ W = ran H$
3	1 2	elghomOLD	$⊢ (G \in GrpOp \land H \in GrpOp) \to (F \in (G GrpOpHom H) \leftrightarrow (F : X ⟶ W \land \forall x \in X \forall y \in X F (x) H F (y) = F (x G y)))$
4	3	simprbda	$⊢ ((G \in GrpOp \land H \in GrpOp) \land F \in (G GrpOpHom H)) \to F : X ⟶ W$
5	4	3impa	$⊢ (G \in GrpOp \land H \in GrpOp \land F \in (G GrpOpHom H)) \to F : X ⟶ W$