Theorem ghmf

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

	Ref	Expression
Hypotheses	ghmf.x	$$⊢X={\mathrm{Base}}_S$$
	ghmf.y	$$⊢Y={\mathrm{Base}}_T$$
Assertion	ghmf	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F:X⟶Y$$

Proof

Step	Hyp	Ref	Expression
1		ghmf.x	$$⊢X={\mathrm{Base}}_S$$
2		ghmf.y	$$⊢Y={\mathrm{Base}}_T$$
3		eqid	$$⊢{+}_S={+}_S$$
4		eqid	$$⊢{+}_T={+}_T$$
5	1 2 3 4	isghm	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\wedge \left(F:X⟶Y\wedge \forall y\in X\forall x\in XF\left(y{+}_{S}x\right)=F\left(y\right){+}_{T}F\left(x\right)\right)\right)$$
6	5	simprbi	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to \left(F:X⟶Y\wedge \forall y\in X\forall x\in XF\left(y{+}_{S}x\right)=F\left(y\right){+}_{T}F\left(x\right)\right)$$
7	6	simpld	$$⊢F\in \left(S\mathrm{GrpHom}T\right)\to F:X⟶Y$$