Definition df-mgmhm 41569

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

Assertion

Ref	Expression
df-mgmhm	⊢ MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})

Distinct variable group:   𝑡,𝑠,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-mgmhm

Step	Hyp	Ref	Expression
1		cmgmhm 41567	. 2 class MgmHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cmgm 17063	. . 3 class Mgm
5		vx	. . . . . . . . . 10 setvar 𝑥
6	5	cv 1474	. . . . . . . . 9 class 𝑥
7		vy	. . . . . . . . . 10 setvar 𝑦
8	7	cv 1474	. . . . . . . . 9 class 𝑦
9	2	cv 1474	. . . . . . . . . 10 class 𝑠
10		cplusg 15768	. . . . . . . . . 10 class +g
11	9, 10	cfv 5804	. . . . . . . . 9 class (+g‘𝑠)
12	6, 8, 11	co 6549	. . . . . . . 8 class (𝑥(+g‘𝑠)𝑦)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1474	. . . . . . . 8 class 𝑓
15	12, 14	cfv 5804	. . . . . . 7 class (𝑓‘(𝑥(+g‘𝑠)𝑦))
16	6, 14	cfv 5804	. . . . . . . 8 class (𝑓‘𝑥)
17	8, 14	cfv 5804	. . . . . . . 8 class (𝑓‘𝑦)
18	3	cv 1474	. . . . . . . . 9 class 𝑡
19	18, 10	cfv 5804	. . . . . . . 8 class (+g‘𝑡)
20	16, 17, 19	co 6549	. . . . . . 7 class ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
21	15, 20	wceq 1475	. . . . . 6 wff (𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
22		cbs 15695	. . . . . . 7 class Base
23	9, 22	cfv 5804	. . . . . 6 class (Base‘𝑠)
24	21, 7, 23	wral 2896	. . . . 5 wff ∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
25	24, 5, 23	wral 2896	. . . 4 wff ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
26	18, 22	cfv 5804	. . . . 5 class (Base‘𝑡)
27		cmap 7744	. . . . 5 class ↑𝑚
28	26, 23, 27	co 6549	. . . 4 class ((Base‘𝑡) ↑𝑚 (Base‘𝑠))
29	25, 13, 28	crab 2900	. . 3 class {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))}
30	2, 3, 4, 4, 29	cmpt2 6551	. 2 class (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})
31	1, 30	wceq 1475	1 wff MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))})

This definition is referenced by:  mgmhmrcl  41571  ismgmhm  41573