This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 = {Base}_{G}$
		ghmabl.y	$⊢ Y = {Base}_{H}$
		ghmabl.p	$⊢ \underset{˙}{+} = +_{G}$
		ghmabl.q	$⊢ \underset{˙}{⨣} = +_{H}$
		ghmabl.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
		ghmabl.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
		ghmabl.3	$⊢ φ \to G \in Abel$
	Assertion	ghmabl	$⊢ φ \to H \in Abel$

Proof

Step	Hyp	Ref	Expression
1		ghmabl.x	$⊢ X = {Base}_{G}$
2		ghmabl.y	$⊢ Y = {Base}_{H}$
3		ghmabl.p	$⊢ \underset{˙}{+} = +_{G}$
4		ghmabl.q	$⊢ \underset{˙}{⨣} = +_{H}$
5		ghmabl.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
6		ghmabl.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
7		ghmabl.3	$⊢ φ \to G \in Abel$
8		ablgrp	$⊢ G \in Abel \to G \in Grp$
9	7 8	syl	$⊢ φ \to G \in Grp$
10	5 1 2 3 4 6 9	ghmgrp	$⊢ φ \to H \in Grp$
11		ablcmn	$⊢ G \in Abel \to G \in CMnd$
12	7 11	syl	$⊢ φ \to G \in CMnd$
13	1 2 3 4 5 6 12	ghmcmn	$⊢ φ \to H \in CMnd$
14		isabl	$⊢ H \in Abel \leftrightarrow (H \in Grp \land H \in CMnd)$
15	10 13 14	sylanbrc	$⊢ φ \to H \in Abel$