Definition df-mhm

Description: A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015)

	Ref	Expression
Assertion	df-mhm	$$⊢\mathrm{MndHom}=\left(s\in \mathrm{Mnd},t\in \mathrm{Mnd}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\left(\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\wedge f\left(0_s\right)=0_t\right)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmhm	$$class\mathrm{MndHom}$$
1		vs	$$setvars$$
2		cmnd	$$class\mathrm{Mnd}$$
3		vt	$$setvart$$
4		vf	$$setvarf$$
5		cbs	$$class\mathrm{Base}$$
6	3	cv	$$setvart$$
7	6 5	cfv	$$class{\mathrm{Base}}_t$$
8		cmap	$$class{\uparrow }_{𝑚}$$
9	1	cv	$$setvars$$
10	9 5	cfv	$$class{\mathrm{Base}}_s$$
11	7 10 8	co	$$class\left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)$$
12		vx	$$setvarx$$
13		vy	$$setvary$$
14	4	cv	$$setvarf$$
15	12	cv	$$setvarx$$
16		cplusg	$$class{+}_{𝑔}$$
17	9 16	cfv	$$class{+}_s$$
18	13	cv	$$setvary$$
19	15 18 17	co	$$class\left(x{+}_{s}y\right)$$
20	19 14	cfv	$$classf\left(x{+}_{s}y\right)$$
21	15 14	cfv	$$classf\left(x\right)$$
22	6 16	cfv	$$class{+}_t$$
23	18 14	cfv	$$classf\left(y\right)$$
24	21 23 22	co	$$class\left(f\left(x\right){+}_{t}f\left(y\right)\right)$$
25	20 24	wceq	$$wfff\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)$$
26	25 13 10	wral	$$wff\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)$$
27	26 12 10	wral	$$wff\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)$$
28		c0g	$$class{0}_{𝑔}$$
29	9 28	cfv	$$class{0}_s$$
30	29 14	cfv	$$classf\left(0_s\right)$$
31	6 28	cfv	$$class{0}_t$$
32	30 31	wceq	$$wfff\left(0_s\right)=0_t$$
33	27 32	wa	$$wff\left(\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\wedge f\left(0_s\right)=0_t\right)$$
34	33 4 11	crab	$$class\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\left(\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\wedge f\left(0_s\right)=0_t\right)\right\}$$
35	1 3 2 2 34	cmpo	$$class\left(s\in \mathrm{Mnd},t\in \mathrm{Mnd}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\left(\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\wedge f\left(0_s\right)=0_t\right)\right\}\right)$$
36	0 35	wceq	$$wff\mathrm{MndHom}=\left(s\in \mathrm{Mnd},t\in \mathrm{Mnd}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\left(\forall x\in {\mathrm{Base}}_s\forall y\in {\mathrm{Base}}_{s}f\left(x{+}_{s}y\right)=f\left(x\right){+}_{t}f\left(y\right)\wedge f\left(0_s\right)=0_t\right)\right\}\right)$$