Definition df-mhm 12683

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.)

Assertion

Ref	Expression
df-mhm	⊢ MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})

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

Detailed syntax breakdown of Definition df-mhm

Step	Hyp	Ref	Expression
1		cmhm 12681	. 2 class MndHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cmnd 12652	. . 3 class Mnd
5		vx	. . . . . . . . . . 11 setvar 𝑥
6	5	cv 1347	. . . . . . . . . 10 class 𝑥
7		vy	. . . . . . . . . . 11 setvar 𝑦
8	7	cv 1347	. . . . . . . . . 10 class 𝑦
9	2	cv 1347	. . . . . . . . . . 11 class 𝑠
10		cplusg 12480	. . . . . . . . . . 11 class +g
11	9, 10	cfv 5198	. . . . . . . . . 10 class (+g‘𝑠)
12	6, 8, 11	co 5853	. . . . . . . . 9 class (𝑥(+g‘𝑠)𝑦)
13		vf	. . . . . . . . . 10 setvar 𝑓
14	13	cv 1347	. . . . . . . . 9 class 𝑓
15	12, 14	cfv 5198	. . . . . . . 8 class (𝑓‘(𝑥(+g‘𝑠)𝑦))
16	6, 14	cfv 5198	. . . . . . . . 9 class (𝑓‘𝑥)
17	8, 14	cfv 5198	. . . . . . . . 9 class (𝑓‘𝑦)
18	3	cv 1347	. . . . . . . . . 10 class 𝑡
19	18, 10	cfv 5198	. . . . . . . . 9 class (+g‘𝑡)
20	16, 17, 19	co 5853	. . . . . . . 8 class ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
21	15, 20	wceq 1348	. . . . . . 7 wff (𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
22		cbs 12416	. . . . . . . 8 class Base
23	9, 22	cfv 5198	. . . . . . 7 class (Base‘𝑠)
24	21, 7, 23	wral 2448	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
25	24, 5, 23	wral 2448	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
26		c0g 12596	. . . . . . . 8 class 0g
27	9, 26	cfv 5198	. . . . . . 7 class (0g‘𝑠)
28	27, 14	cfv 5198	. . . . . 6 class (𝑓‘(0g‘𝑠))
29	18, 26	cfv 5198	. . . . . 6 class (0g‘𝑡)
30	28, 29	wceq 1348	. . . . 5 wff (𝑓‘(0g‘𝑠)) = (0g‘𝑡)
31	25, 30	wa 103	. . . 4 wff (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))
32	18, 22	cfv 5198	. . . . 5 class (Base‘𝑡)
33		cmap 6626	. . . . 5 class ↑𝑚
34	32, 23, 33	co 5853	. . . 4 class ((Base‘𝑡) ↑𝑚 (Base‘𝑠))
35	31, 13, 34	crab 2452	. . 3 class {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}
36	2, 3, 4, 4, 35	cmpo 5855	. 2 class (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
37	1, 36	wceq 1348	1 wff MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})

This definition is referenced by:  ismhm  12685  mhmrcl1  12686  mhmrcl2  12687