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 35913
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 35912 . 2 class Mgm
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cmgm 18546 . . 3 class Mgm
5 vu . . . . . . . . . 10 setvar 𝑢
65cv 1541 . . . . . . . . 9 class 𝑢
7 vv . . . . . . . . . 10 setvar 𝑣
87cv 1541 . . . . . . . . 9 class 𝑣
92cv 1541 . . . . . . . . . 10 class 𝑥
10 cplusg 17184 . . . . . . . . . 10 class +g
119, 10cfv 6535 . . . . . . . . 9 class (+g𝑥)
126, 8, 11co 7396 . . . . . . . 8 class (𝑢(+g𝑥)𝑣)
13 vf . . . . . . . . 9 setvar 𝑓
1413cv 1541 . . . . . . . 8 class 𝑓
1512, 14cfv 6535 . . . . . . 7 class (𝑓‘(𝑢(+g𝑥)𝑣))
166, 14cfv 6535 . . . . . . . 8 class (𝑓𝑢)
178, 14cfv 6535 . . . . . . . 8 class (𝑓𝑣)
183cv 1541 . . . . . . . . 9 class 𝑦
1918, 10cfv 6535 . . . . . . . 8 class (+g𝑦)
2016, 17, 19co 7396 . . . . . . 7 class ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2115, 20wceq 1542 . . . . . 6 wff (𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
22 cbs 17131 . . . . . . 7 class Base
239, 22cfv 6535 . . . . . 6 class (Base‘𝑥)
2421, 7, 23wral 3062 . . . . 5 wff 𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2524, 5, 23wral 3062 . . . 4 wff 𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2618, 22cfv 6535 . . . . 5 class (Base‘𝑦)
27 csethom 35908 . . . . 5 class Set
2823, 26, 27co 7396 . . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
2925, 13, 28crab 3433 . . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))}
302, 3, 4, 4, 29cmpo 7398 . 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))})
311, 30wceq 1542 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