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 17107
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
StepHypRef Expression
1 cmhm 17105 . 2 class MndHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cmnd 17066 . . 3 class Mnd
5 vx . . . . . . . . . . 11 setvar 𝑥
65cv 1474 . . . . . . . . . 10 class 𝑥
7 vy . . . . . . . . . . 11 setvar 𝑦
87cv 1474 . . . . . . . . . 10 class 𝑦
92cv 1474 . . . . . . . . . . 11 class 𝑠
10 cplusg 15717 . . . . . . . . . . 11 class +g
119, 10cfv 5790 . . . . . . . . . 10 class (+g𝑠)
126, 8, 11co 6527 . . . . . . . . 9 class (𝑥(+g𝑠)𝑦)
13 vf . . . . . . . . . 10 setvar 𝑓
1413cv 1474 . . . . . . . . 9 class 𝑓
1512, 14cfv 5790 . . . . . . . 8 class (𝑓‘(𝑥(+g𝑠)𝑦))
166, 14cfv 5790 . . . . . . . . 9 class (𝑓𝑥)
178, 14cfv 5790 . . . . . . . . 9 class (𝑓𝑦)
183cv 1474 . . . . . . . . . 10 class 𝑡
1918, 10cfv 5790 . . . . . . . . 9 class (+g𝑡)
2016, 17, 19co 6527 . . . . . . . 8 class ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2115, 20wceq 1475 . . . . . . 7 wff (𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
22 cbs 15644 . . . . . . . 8 class Base
239, 22cfv 5790 . . . . . . 7 class (Base‘𝑠)
2421, 7, 23wral 2896 . . . . . 6 wff 𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2524, 5, 23wral 2896 . . . . 5 wff 𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
26 c0g 15872 . . . . . . . 8 class 0g
279, 26cfv 5790 . . . . . . 7 class (0g𝑠)
2827, 14cfv 5790 . . . . . 6 class (𝑓‘(0g𝑠))
2918, 26cfv 5790 . . . . . 6 class (0g𝑡)
3028, 29wceq 1475 . . . . 5 wff (𝑓‘(0g𝑠)) = (0g𝑡)
3125, 30wa 383 . . . 4 wff (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))
3218, 22cfv 5790 . . . . 5 class (Base‘𝑡)
33 cmap 7722 . . . . 5 class 𝑚
3432, 23, 33co 6527 . . . 4 class ((Base‘𝑡) ↑𝑚 (Base‘𝑠))
3531, 13, 34crab 2900 . . 3 class {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))}
362, 3, 4, 4, 35cmpt2 6529 . 2 class (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
371, 36wceq 1475 1 wff MndHom = (𝑠 ∈ Mnd, 𝑡 ∈ Mnd ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ (∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦)) ∧ (𝑓‘(0g𝑠)) = (0g𝑡))})
Colors of variables: wff setvar class
This definition is referenced by:  ismhm  17109  mhmrcl1  17110  mhmrcl2  17111
  Copyright terms: Public domain W3C validator