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

Metamath Proof Explorer

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

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 ghmfghm.3 ⊢ ( 𝜑 → 𝐺 ∈ Grp )
8 5 1 2 3 4 6 7 ghmgrp ⊢ ( 𝜑 → 𝐻 ∈ Grp )
9 fof ⊢ ( 𝐹 : 𝑋 –onto→ 𝑌 → 𝐹 : 𝑋 ⟶ 𝑌 )
10 6 9 syl ⊢ ( 𝜑 → 𝐹 : 𝑋 ⟶ 𝑌 )
11 5 3expb ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋 ) ) → ( 𝐹 ‘ ( 𝑥 + 𝑦 ) ) = ( ( 𝐹 ‘ 𝑥 ) ⨣ ( 𝐹 ‘ 𝑦 ) ) )
12 1 2 3 4 7 8 10 11 isghmd ⊢ ( 𝜑 → 𝐹 ∈ ( 𝐺 GrpHom 𝐻 ) )