Theorem 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	$$⊢\left(\phi \wedge x\in X\wedge y\in X\right)\to F\left(x\underset{\dot{}}{+}y\right)=F\left(x\right)\underset{\dot{}}{⨣}F\left(y\right)$$
	ghmgrp.x	$$⊢X={\mathrm{Base}}_G$$
	ghmgrp.y	$$⊢Y={\mathrm{Base}}_H$$
	ghmgrp.p	$$⊢\underset{\dot{}}{+}={+}_G$$
	ghmgrp.q	$$⊢\underset{\dot{}}{⨣}={+}_H$$
	ghmgrp.1	$$⊢\phi \to F:X\underset{onto}{⟶}Y$$
	mhmmnd.3	$$⊢\phi \to G\in \mathrm{Mnd}$$
Assertion	mhmfmhm	$$⊢\phi \to F\in \left(G\mathrm{MndHom}H\right)$$

Proof

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