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	$⊢ 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$
	ghmfghm.3	$⊢ φ \to G \in Grp$
Assertion	ghmfghm	$⊢ φ \to F \in (G GrpHom H)$

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		ghmfghm.3	$⊢ φ \to G \in Grp$
8	5 1 2 3 4 6 7	ghmgrp	$⊢ φ \to H \in Grp$
9		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
10	6 9	syl	$⊢ φ \to F : X ⟶ Y$
11	5	3expb	$⊢ (φ \land (x \in X \land y \in X)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
12	1 2 3 4 7 8 10 11	isghmd	$⊢ φ \to F \in (G GrpHom H)$

Metamath Proof Explorer