Definition df-mhm 13819

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 13817	. 2 class MndHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cmnd 13782	. . 3 class Mnd
5		vx	. . . . . . . . . . 11 setvar 𝑥
6	5	cv 1401	. . . . . . . . . 10 class 𝑥
7		vy	. . . . . . . . . . 11 setvar 𝑦
8	7	cv 1401	. . . . . . . . . 10 class 𝑦
9	2	cv 1401	. . . . . . . . . . 11 class 𝑠
10		cplusg 13484	. . . . . . . . . . 11 class +g
11	9, 10	cfv 5377	. . . . . . . . . 10 class (+g‘𝑠)
12	6, 8, 11	co 6085	. . . . . . . . 9 class (𝑥(+g‘𝑠)𝑦)
13		vf	. . . . . . . . . 10 setvar 𝑓
14	13	cv 1401	. . . . . . . . 9 class 𝑓
15	12, 14	cfv 5377	. . . . . . . 8 class (𝑓‘(𝑥(+g‘𝑠)𝑦))
16	6, 14	cfv 5377	. . . . . . . . 9 class (𝑓‘𝑥)
17	8, 14	cfv 5377	. . . . . . . . 9 class (𝑓‘𝑦)
18	3	cv 1401	. . . . . . . . . 10 class 𝑡
19	18, 10	cfv 5377	. . . . . . . . 9 class (+g‘𝑡)
20	16, 17, 19	co 6085	. . . . . . . 8 class ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
21	15, 20	wceq 1402	. . . . . . 7 wff (𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
22		cbs 13404	. . . . . . . 8 class Base
23	9, 22	cfv 5377	. . . . . . 7 class (Base‘𝑠)
24	21, 7, 23	wral 2528	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
25	24, 5, 23	wral 2528	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
26		c0g 13663	. . . . . . . 8 class 0g
27	9, 26	cfv 5377	. . . . . . 7 class (0g‘𝑠)
28	27, 14	cfv 5377	. . . . . 6 class (𝑓‘(0g‘𝑠))
29	18, 26	cfv 5377	. . . . . 6 class (0g‘𝑡)
30	28, 29	wceq 1402	. . . . 5 wff (𝑓‘(0g‘𝑠)) = (0g‘𝑡)
31	25, 30	wa 104	. . . 4 wff (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))
32	18, 22	cfv 5377	. . . . 5 class (Base‘𝑡)
33		cmap 6922	. . . . 5 class ↑𝑚
34	32, 23, 33	co 6085	. . . 4 class ((Base‘𝑡) ↑𝑚 (Base‘𝑠))
35	31, 13, 34	crab 2532	. . 3 class {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}
36	2, 3, 4, 4, 35	cmpo 6087	. 2 class (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
37	1, 36	wceq 1402	1 wff MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})

This definition is used by:  ismhm  13821  mhmex  13822  mhmrcl1  13823  mhmrcl2  13824