Definition df-mgmhm

Description: A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020)

	Ref	Expression
Assertion	df-mgmhm	$$⊢\mathrm{MgmHom}=\left(s\in \mathrm{Mgm},t\in \mathrm{Mgm}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}\right)$$

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgmhm	$$class\mathrm{MgmHom}$$
1		vs	$$setvars$$
2		cmgm	$$class\mathrm{Mgm}$$
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	27 4 11	crab	$$class\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}$$
29	1 3 2 2 28	cmpo	$$class\left(s\in \mathrm{Mgm},t\in \mathrm{Mgm}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}\right)$$
30	0 29	wceq	$$wff\mathrm{MgmHom}=\left(s\in \mathrm{Mgm},t\in \mathrm{Mgm}⟼\left\{f\in \left({{\mathrm{Base}}_t}^{{\mathrm{Base}}_s}\right)|\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)\right\}\right)$$