Theorem ghmf

Description: A group homomorphism is a function. (Contributed by Stefan O'Rear, 31-Dec-2014)

	Ref	Expression
Hypotheses	ghmf.x	|- X = ( Base ` S )
	ghmf.y	|- Y = ( Base ` T )
Assertion	ghmf	|- ( F e. ( S GrpHom T ) -> F : X --> Y )

Proof

Step	Hyp	Ref	Expression
1		ghmf.x	|- X = ( Base ` S )
2		ghmf.y	|- Y = ( Base ` T )
3		eqid	|- ( +g ` S ) = ( +g ` S )
4		eqid	|- ( +g ` T ) = ( +g ` T )
5	1 2 3 4	isghm	|- ( F e. ( S GrpHom T ) <-> ( ( S e. Grp /\ T e. Grp ) /\ ( F : X --> Y /\ A. y e. X A. x e. X ( F ` ( y ( +g ` S ) x ) ) = ( ( F ` y ) ( +g ` T ) ( F ` x ) ) ) ) )
6	5	simprbi	|- ( F e. ( S GrpHom T ) -> ( F : X --> Y /\ A. y e. X A. x e. X ( F ` ( y ( +g ` S ) x ) ) = ( ( F ` y ) ( +g ` T ) ( F ` x ) ) ) )
7	6	simpld	|- ( F e. ( S GrpHom T ) -> F : X --> Y )