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 𝐻 ) )