mhmfmhm

Description: The function fulfilling the conditions of mhmmnd is a monoid homomorphism. (Contributed by Thierry Arnoux, 26-Jan-2020)

	Ref	Expression
Hypotheses	ghmgrp.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
	ghmgrp.x	$⊢ X = {Base}_{G}$
	ghmgrp.y	$⊢ Y = {Base}_{H}$
	ghmgrp.p	$⊢ \underset{˙}{+} = +_{G}$
	ghmgrp.q	$⊢ \underset{˙}{⨣} = +_{H}$
	ghmgrp.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
	mhmmnd.3	$⊢ φ \to G \in Mnd$
Assertion	mhmfmhm	$⊢ φ \to F \in (G MndHom H)$

Step	Hyp	Ref	Expression
1		ghmgrp.f	$⊢ (φ \land x \in X \land y \in X) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
2		ghmgrp.x	$⊢ X = {Base}_{G}$
3		ghmgrp.y	$⊢ Y = {Base}_{H}$
4		ghmgrp.p	$⊢ \underset{˙}{+} = +_{G}$
5		ghmgrp.q	$⊢ \underset{˙}{⨣} = +_{H}$
6		ghmgrp.1	$⊢ φ \to F : X \underset{onto}{⟶} Y$
7		mhmmnd.3	$⊢ φ \to G \in Mnd$
8	1 2 3 4 5 6 7	mhmmnd	$⊢ φ \to H \in Mnd$
9		fof	$⊢ F : X \underset{onto}{⟶} Y \to F : X ⟶ Y$
10	6 9	syl	$⊢ φ \to F : X ⟶ Y$
11	1	3expb	$⊢ (φ \land (x \in X \land y \in X)) \to F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
12	11	ralrimivva	$⊢ φ \to \forall x \in X \forall y \in X F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y)$
13		eqid	$⊢ 0_{G} = 0_{G}$
14	1 2 3 4 5 6 7 13	mhmid	$⊢ φ \to F (0_{G}) = 0_{H}$
15	10 12 14	3jca	$⊢ φ \to (F : X ⟶ Y \land \forall x \in X \forall y \in X F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y) \land F (0_{G}) = 0_{H})$
16		eqid	$⊢ 0_{H} = 0_{H}$
17	2 3 4 5 13 16	ismhm	$⊢ F \in (G MndHom H) \leftrightarrow ((G \in Mnd \land H \in Mnd) \land (F : X ⟶ Y \land \forall x \in X \forall y \in X F (x \underset{˙}{+} y) = F (x) \underset{˙}{⨣} F (y) \land F (0_{G}) = 0_{H}))$
18	7 8 15 17	syl21anbrc	$⊢ φ \to F \in (G MndHom H)$

Metamath Proof Explorer