Definition df-mhm 18796

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‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})

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

Detailed syntax breakdown of Definition df-mhm

Step	Hyp	Ref	Expression
1		cmhm 18794	. 2 class MndHom
2		vs	. . 3 setvar 𝑠
3		vt	. . 3 setvar 𝑡
4		cmnd 18747	. . 3 class Mnd
5		vx	. . . . . . . . . . 11 setvar 𝑥
6	5	cv 1539	. . . . . . . . . 10 class 𝑥
7		vy	. . . . . . . . . . 11 setvar 𝑦
8	7	cv 1539	. . . . . . . . . 10 class 𝑦
9	2	cv 1539	. . . . . . . . . . 11 class 𝑠
10		cplusg 17297	. . . . . . . . . . 11 class +g
11	9, 10	cfv 6561	. . . . . . . . . 10 class (+g‘𝑠)
12	6, 8, 11	co 7431	. . . . . . . . 9 class (𝑥(+g‘𝑠)𝑦)
13		vf	. . . . . . . . . 10 setvar 𝑓
14	13	cv 1539	. . . . . . . . 9 class 𝑓
15	12, 14	cfv 6561	. . . . . . . 8 class (𝑓‘(𝑥(+g‘𝑠)𝑦))
16	6, 14	cfv 6561	. . . . . . . . 9 class (𝑓‘𝑥)
17	8, 14	cfv 6561	. . . . . . . . 9 class (𝑓‘𝑦)
18	3	cv 1539	. . . . . . . . . 10 class 𝑡
19	18, 10	cfv 6561	. . . . . . . . 9 class (+g‘𝑡)
20	16, 17, 19	co 7431	. . . . . . . 8 class ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
21	15, 20	wceq 1540	. . . . . . 7 wff (𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
22		cbs 17247	. . . . . . . 8 class Base
23	9, 22	cfv 6561	. . . . . . 7 class (Base‘𝑠)
24	21, 7, 23	wral 3061	. . . . . 6 wff ∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
25	24, 5, 23	wral 3061	. . . . 5 wff ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦))
26		c0g 17484	. . . . . . . 8 class 0g
27	9, 26	cfv 6561	. . . . . . 7 class (0g‘𝑠)
28	27, 14	cfv 6561	. . . . . 6 class (𝑓‘(0g‘𝑠))
29	18, 26	cfv 6561	. . . . . 6 class (0g‘𝑡)
30	28, 29	wceq 1540	. . . . 5 wff (𝑓‘(0g‘𝑠)) = (0g‘𝑡)
31	25, 30	wa 395	. . . 4 wff (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))
32	18, 22	cfv 6561	. . . . 5 class (Base‘𝑡)
33		cmap 8866	. . . . 5 class ↑m
34	32, 23, 33	co 7431	. . . 4 class ((Base‘𝑡) ↑m (Base‘𝑠))
35	31, 13, 34	crab 3436	. . 3 class {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))}
36	2, 3, 4, 4, 35	cmpo 7433	. 2 class (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})
37	1, 36	wceq 1540	1 wff MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g‘𝑠)𝑦)) = ((𝑓‘𝑥)(+g‘𝑡)(𝑓‘𝑦)) ∧ (𝑓‘(0g‘𝑠)) = (0g‘𝑡))})

This definition is referenced by:  ismhm  18798  mhmrcl1  18800  mhmrcl2  18801