This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.
Database BASIC ALGEBRAIC STRUCTURES Groups Abelian groups Definition and basic properties 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 )