Theorem isghmd

Description: Deduction for a group homomorphism. (Contributed by Stefan O'Rear, 4-Feb-2015)

	Ref	Expression
Hypotheses	isghmd.x	$$⊢X={\mathrm{Base}}_S$$
	isghmd.y	$$⊢Y={\mathrm{Base}}_T$$
	isghmd.a	$$⊢\underset{\dot{}}{+}={+}_S$$
	isghmd.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
	isghmd.s	$$⊢\phi \to S\in \mathrm{Grp}$$
	isghmd.t	$$⊢\phi \to T\in \mathrm{Grp}$$
	isghmd.f	$$⊢\phi \to F:X⟶Y$$
	isghmd.l	$$⊢\left(\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
Assertion	isghmd	$$⊢\phi \to F\in \left(S\mathrm{GrpHom}T\right)$$

Proof

Step	Hyp	Ref	Expression
1		isghmd.x	$$⊢X={\mathrm{Base}}_S$$
2		isghmd.y	$$⊢Y={\mathrm{Base}}_T$$
3		isghmd.a	$$⊢\underset{\dot{}}{+}={+}_S$$
4		isghmd.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
5		isghmd.s	$$⊢\phi \to S\in \mathrm{Grp}$$
6		isghmd.t	$$⊢\phi \to T\in \mathrm{Grp}$$
7		isghmd.f	$$⊢\phi \to F:X⟶Y$$
8		isghmd.l	$$⊢\left(\phi \wedge \left(x\in X\wedge y\in X\right)\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
9	8	ralrimivva	$$⊢\phi \to \forall x\in X\forall y\in XF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
10	7 9	jca	$$⊢\phi \to \left(F:X⟶Y\wedge \forall x\in X\forall y\in XF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\right)$$
11	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 x\in X\forall y\in XF\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)\right)\right)$$
12	5 6 10 11	syl21anbrc	$$⊢\phi \to F\in \left(S\mathrm{GrpHom}T\right)$$