Users' Mathboxes Mathbox for BJ < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >   Mathboxes  >  df-bj-mgmhom Structured version   Visualization version   GIF version

Definition df-bj-mgmhom 36003
Description: Define the set of magma morphisms between two magmas. If domain and codomain are semigroups, monoids, or groups, then one obtains the set of morphisms of these structures. (Contributed by BJ, 10-Feb-2022.)
Assertion
Ref Expression
df-bj-mgmhom Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))})
Distinct variable group:   𝑥,𝑓,𝑦,𝑢,𝑣

Detailed syntax breakdown of Definition df-bj-mgmhom
StepHypRef Expression
1 cmgmhom 36002 . 2 class Mgm
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cmgm 18558 . . 3 class Mgm
5 vu . . . . . . . . . 10 setvar 𝑢
65cv 1540 . . . . . . . . 9 class 𝑢
7 vv . . . . . . . . . 10 setvar 𝑣
87cv 1540 . . . . . . . . 9 class 𝑣
92cv 1540 . . . . . . . . . 10 class 𝑥
10 cplusg 17196 . . . . . . . . . 10 class +g
119, 10cfv 6543 . . . . . . . . 9 class (+g𝑥)
126, 8, 11co 7408 . . . . . . . 8 class (𝑢(+g𝑥)𝑣)
13 vf . . . . . . . . 9 setvar 𝑓
1413cv 1540 . . . . . . . 8 class 𝑓
1512, 14cfv 6543 . . . . . . 7 class (𝑓‘(𝑢(+g𝑥)𝑣))
166, 14cfv 6543 . . . . . . . 8 class (𝑓𝑢)
178, 14cfv 6543 . . . . . . . 8 class (𝑓𝑣)
183cv 1540 . . . . . . . . 9 class 𝑦
1918, 10cfv 6543 . . . . . . . 8 class (+g𝑦)
2016, 17, 19co 7408 . . . . . . 7 class ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2115, 20wceq 1541 . . . . . 6 wff (𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
22 cbs 17143 . . . . . . 7 class Base
239, 22cfv 6543 . . . . . 6 class (Base‘𝑥)
2421, 7, 23wral 3061 . . . . 5 wff 𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2524, 5, 23wral 3061 . . . 4 wff 𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2618, 22cfv 6543 . . . . 5 class (Base‘𝑦)
27 csethom 35998 . . . . 5 class Set
2823, 26, 27co 7408 . . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
2925, 13, 28crab 3432 . . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))}
302, 3, 4, 4, 29cmpo 7410 . 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))})
311, 30wceq 1541 1 wff Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))})
Colors of variables: wff setvar class
This definition is referenced by: (None)
  Copyright terms: Public domain W3C validator