Theorem isghm3

Description: Property of a group homomorphism, similar to ismhm . (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Hypotheses	isghm.w	$$⊢X={\mathrm{Base}}_S$$
	isghm.x	$$⊢Y={\mathrm{Base}}_T$$
	isghm.a	$$⊢\underset{\dot{}}{+}={+}_S$$
	isghm.b	$$⊢\underset{\dot{}}{⨣}={+}_T$$
Assertion	isghm3	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\to \left(F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		isghm.w	$$⊢X={\mathrm{Base}}_S$$
2		isghm.x	$$⊢Y={\mathrm{Base}}_T$$
3		isghm.a	$$⊢\underset{\dot{}}{+}={+}_S$$
4		isghm.b	$$⊢\underset{\dot{}}{⨣}={+}_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 u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$
6	5	baib	$$⊢\left(S\in \mathrm{Grp}\wedge T\in \mathrm{Grp}\right)\to \left(F\in \left(S\mathrm{GrpHom}T\right)\leftrightarrow \left(F:X⟶Y\wedge \forall u\in X\forall v\in XF\left(u\underset{\dot{}}{+}v\right)=F\left(u\right)\underset{\dot{}}{⨣}F\left(v\right)\right)\right)$$