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	$⊢ MgmHom = (s \in Mgm, t \in Mgm ⟼ \{f \in ({Base}_{t}^{{Base}_{s}}) \| \forall x \in {Base}_{s} \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)\})$

Step	Hyp	Ref	Expression
0		cmgmhm	$class MgmHom$
1		vs	$setvar s$
2		cmgm	$class Mgm$
3		vt	$setvar t$
4		vf	$setvar f$
5		cbs	$class Base$
6	3	cv	$setvar t$
7	6 5	cfv	$class {Base}_{t}$
8		cmap	$class ↑_{𝑚}$
9	1	cv	$setvar s$
10	9 5	cfv	$class {Base}_{s}$
11	7 10 8	co	$class ({Base}_{t}^{{Base}_{s}})$
12		vx	$setvar x$
13		vy	$setvar y$
14	4	cv	$setvar f$
15	12	cv	$setvar x$
16		cplusg	$class +_{𝑔}$
17	9 16	cfv	$class +_{s}$
18	13	cv	$setvar y$
19	15 18 17	co	$class (x +_{s} y)$
20	19 14	cfv	$class f (x +_{s} y)$
21	15 14	cfv	$class f (x)$
22	6 16	cfv	$class +_{t}$
23	18 14	cfv	$class f (y)$
24	21 23 22	co	$class (f (x) +_{t} f (y))$
25	20 24	wceq	$wff f (x +_{s} y) = f (x) +_{t} f (y)$
26	25 13 10	wral	$wff \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)$
27	26 12 10	wral	$wff \forall x \in {Base}_{s} \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)$
28	27 4 11	crab	$class \{f \in ({Base}_{t}^{{Base}_{s}}) \| \forall x \in {Base}_{s} \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)\}$
29	1 3 2 2 28	cmpo	$class (s \in Mgm, t \in Mgm ⟼ \{f \in ({Base}_{t}^{{Base}_{s}}) \| \forall x \in {Base}_{s} \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)\})$
30	0 29	wceq	$wff MgmHom = (s \in Mgm, t \in Mgm ⟼ \{f \in ({Base}_{t}^{{Base}_{s}}) \| \forall x \in {Base}_{s} \forall y \in {Base}_{s} f (x +_{s} y) = f (x) +_{t} f (y)\})$

Metamath Proof Explorer