MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mhm Structured version   Visualization version   GIF version

Definition df-mhm 17946
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
StepHypRef Expression
1 cmhm 17944 . 2 class MndHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cmnd 17901 . . 3 class Mnd
5 vx . . . . . . . . . . 11 setvar 𝑥
65cv 1527 . . . . . . . . . 10 class 𝑥
7 vy . . . . . . . . . . 11 setvar 𝑦
87cv 1527 . . . . . . . . . 10 class 𝑦
92cv 1527 . . . . . . . . . . 11 class 𝑠
10 cplusg 16555 . . . . . . . . . . 11 class +g
119, 10cfv 6349 . . . . . . . . . 10 class (+g𝑠)
126, 8, 11co 7145 . . . . . . . . 9 class (𝑥(+g𝑠)𝑦)
13 vf . . . . . . . . . 10 setvar 𝑓
1413cv 1527 . . . . . . . . 9 class 𝑓
1512, 14cfv 6349 . . . . . . . 8 class (𝑓‘(𝑥(+g𝑠)𝑦))
166, 14cfv 6349 . . . . . . . . 9 class (𝑓𝑥)
178, 14cfv 6349 . . . . . . . . 9 class (𝑓𝑦)
183cv 1527 . . . . . . . . . 10 class 𝑡
1918, 10cfv 6349 . . . . . . . . 9 class (+g𝑡)
2016, 17, 19co 7145 . . . . . . . 8 class ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2115, 20wceq 1528 . . . . . . 7 wff (𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
22 cbs 16473 . . . . . . . 8 class Base
239, 22cfv 6349 . . . . . . 7 class (Base‘𝑠)
2421, 7, 23wral 3138 . . . . . 6 wff 𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2524, 5, 23wral 3138 . . . . 5 wff 𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
26 c0g 16703 . . . . . . . 8 class 0g
279, 26cfv 6349 . . . . . . 7 class (0g𝑠)
2827, 14cfv 6349 . . . . . 6 class (𝑓‘(0g𝑠))
2918, 26cfv 6349 . . . . . 6 class (0g𝑡)
3028, 29wceq 1528 . . . . 5 wff (𝑓‘(0g𝑠)) = (0g𝑡)
3125, 30wa 396 . . . 4 wff (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))
3218, 22cfv 6349 . . . . 5 class (Base‘𝑡)
33 cmap 8396 . . . . 5 class m
3432, 23, 33co 7145 . . . 4 class ((Base‘𝑡) ↑m (Base‘𝑠))
3531, 13, 34crab 3142 . . 3 class {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))}
362, 3, 4, 4, 35cmpo 7147 . 2 class (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
371, 36wceq 1528 1 wff MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑m (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
Colors of variables: wff setvar class
This definition is referenced by:  ismhm  17948  mhmrcl1  17949  mhmrcl2  17950
  Copyright terms: Public domain W3C validator