Users' Mathboxes Mathbox for Alexander van der Vekens < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-mgmhm Structured version   Visualization version   GIF version

Definition df-mgmhm 41564
Description: A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020.)
Assertion
Ref Expression
df-mgmhm MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))})
Distinct variable group:   𝑡,𝑠,𝑓,𝑥,𝑦

Detailed syntax breakdown of Definition df-mgmhm
StepHypRef Expression
1 cmgmhm 41562 . 2 class MgmHom
2 vs . . 3 setvar 𝑠
3 vt . . 3 setvar 𝑡
4 cmgm 17009 . . 3 class Mgm
5 vx . . . . . . . . . 10 setvar 𝑥
65cv 1473 . . . . . . . . 9 class 𝑥
7 vy . . . . . . . . . 10 setvar 𝑦
87cv 1473 . . . . . . . . 9 class 𝑦
92cv 1473 . . . . . . . . . 10 class 𝑠
10 cplusg 15714 . . . . . . . . . 10 class +g
119, 10cfv 5790 . . . . . . . . 9 class (+g𝑠)
126, 8, 11co 6527 . . . . . . . 8 class (𝑥(+g𝑠)𝑦)
13 vf . . . . . . . . 9 setvar 𝑓
1413cv 1473 . . . . . . . 8 class 𝑓
1512, 14cfv 5790 . . . . . . 7 class (𝑓‘(𝑥(+g𝑠)𝑦))
166, 14cfv 5790 . . . . . . . 8 class (𝑓𝑥)
178, 14cfv 5790 . . . . . . . 8 class (𝑓𝑦)
183cv 1473 . . . . . . . . 9 class 𝑡
1918, 10cfv 5790 . . . . . . . 8 class (+g𝑡)
2016, 17, 19co 6527 . . . . . . 7 class ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2115, 20wceq 1474 . . . . . 6 wff (𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
22 cbs 15641 . . . . . . 7 class Base
239, 22cfv 5790 . . . . . 6 class (Base‘𝑠)
2421, 7, 23wral 2895 . . . . 5 wff 𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2524, 5, 23wral 2895 . . . 4 wff 𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))
2618, 22cfv 5790 . . . . 5 class (Base‘𝑡)
27 cmap 7721 . . . . 5 class 𝑚
2826, 23, 27co 6527 . . . 4 class ((Base‘𝑡) ↑𝑚 (Base‘𝑠))
2925, 13, 28crab 2899 . . 3 class {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))}
302, 3, 4, 4, 29cmpt2 6529 . 2 class (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))})
311, 30wceq 1474 1 wff MgmHom = (𝑠 ∈ Mgm, 𝑡 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑡) ↑𝑚 (Base‘𝑠)) ∣ ∀𝑥 ∈ (Base‘𝑠)∀𝑦 ∈ (Base‘𝑠)(𝑓‘(𝑥(+g𝑠)𝑦)) = ((𝑓𝑥)(+g𝑡)(𝑓𝑦))})
Colors of variables: wff setvar class
This definition is referenced by:  mgmhmrcl  41566  ismgmhm  41568
  Copyright terms: Public domain W3C validator