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	⊢ 𝑋 = ( Base ‘ 𝐺 )
	ghmabl.y	⊢ 𝑌 = ( Base ‘ 𝐻 )
	ghmabl.p	⊢ + = ( +g ‘ 𝐺 )
	ghmabl.q	⊢ ⨣ = ( +g ‘ 𝐻 )
	ghmabl.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
	ghmabl.1	⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
	ghmabl.3	⊢ ( 𝜑 → 𝐺 ∈ Abel )
Assertion	ghmabl	⊢ ( 𝜑 → 𝐻 ∈ Abel )

Proof

Step	Hyp	Ref	Expression
1		ghmabl.x	⊢ 𝑋 = ( Base ‘ 𝐺 )
2		ghmabl.y	⊢ 𝑌 = ( Base ‘ 𝐻 )
3		ghmabl.p	⊢ + = ( +g ‘ 𝐺 )
4		ghmabl.q	⊢ ⨣ = ( +g ‘ 𝐻 )
5		ghmabl.f	⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
6		ghmabl.1	⊢ ( 𝜑 → 𝐹 : 𝑋 –onto→ 𝑌 )
7		ghmabl.3	⊢ ( 𝜑 → 𝐺 ∈ Abel )
8		ablgrp	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
9	7 8	syl	⊢ ( 𝜑 → 𝐺 ∈ Grp )
10	5 1 2 3 4 6 9	ghmgrp	⊢ ( 𝜑 → 𝐻 ∈ Grp )
11		ablcmn	⊢ ( 𝐺 ∈ Abel → 𝐺 ∈ CMnd )
12	7 11	syl	⊢ ( 𝜑 → 𝐺 ∈ CMnd )
13	1 2 3 4 5 6 12	ghmcmn	⊢ ( 𝜑 → 𝐻 ∈ CMnd )
14		isabl	⊢ ( 𝐻 ∈ Abel ↔ ( 𝐻 ∈ Grp ∧ 𝐻 ∈ CMnd ) )
15	10 13 14	sylanbrc	⊢ ( 𝜑 → 𝐻 ∈ Abel )