Theorem ghmabl

Description: The image of an abelian group G under a group homomorphism F is an abelian group. (Contributed by Mario Carneiro, 12-May-2014) (Revised 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$$
	ghmabl.3	$$⊢\phi \to G\in \mathrm{Abel}$$
Assertion	ghmabl	$$⊢\phi \to H\in \mathrm{Abel}$$

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		ghmabl.3	$$⊢\phi \to G\in \mathrm{Abel}$$
8		ablgrp	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{Grp}$$
9	7 8	syl	$$⊢\phi \to G\in \mathrm{Grp}$$
10	5 1 2 3 4 6 9	ghmgrp	$$⊢\phi \to H\in \mathrm{Grp}$$
11		ablcmn	$$⊢G\in \mathrm{Abel}\to G\in \mathrm{CMnd}$$
12	7 11	syl	$$⊢\phi \to G\in \mathrm{CMnd}$$
13	1 2 3 4 5 6 12	ghmcmn	$$⊢\phi \to H\in \mathrm{CMnd}$$
14		isabl	$$⊢H\in \mathrm{Abel}\leftrightarrow \left(H\in \mathrm{Grp}\wedge H\in \mathrm{CMnd}\right)$$
15	10 13 14	sylanbrc	$$⊢\phi \to H\in \mathrm{Abel}$$