Theorem ghmfghm

Description: The function fulfilling the conditions of ghmgrp is a group homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020)

	Ref	Expression
Hypotheses	ghmabl.x	$$⊢X={\mathrm{Base}}_G$$
	ghmabl.y	$$⊢Y={\mathrm{Base}}_H$$
	ghmabl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	ghmabl.q	$$⊢\underset{\dot{}}{⨣}={+}_H$$
	ghmabl.f	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
	ghmabl.1	$$⊢\phi \to F:X\underset{onto}{⟶}Y$$
	ghmfghm.3	$$⊢\phi \to G\in \mathrm{Grp}$$
Assertion	ghmfghm	$$⊢\phi \to F\in \left(G\mathrm{GrpHom}H\right)$$

Proof

Step	Hyp	Ref	Expression
1		ghmabl.x	$$⊢X={\mathrm{Base}}_G$$
2		ghmabl.y	$$⊢Y={\mathrm{Base}}_H$$
3		ghmabl.p	$$⊢\underset{\dot{}}{+}={+}_G$$
4		ghmabl.q	$$⊢\underset{\dot{}}{⨣}={+}_H$$
5		ghmabl.f	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
6		ghmabl.1	$$⊢\phi \to F:X\underset{onto}{⟶}Y$$
7		ghmfghm.3	$$⊢\phi \to G\in \mathrm{Grp}$$
8	5 1 2 3 4 6 7	ghmgrp	$$⊢\phi \to H\in \mathrm{Grp}$$
9		fof	$$⊢F:X\underset{onto}{⟶}Y\to F:X⟶Y$$
10	6 9	syl	$$⊢\phi \to F:X⟶Y$$
11	5	3expb	$$⊢\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)$$
12	1 2 3 4 7 8 10 11	isghmd	$$⊢\phi \to F\in \left(G\mathrm{GrpHom}H\right)$$