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 34537
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 34536 . 2 class Mgm
2 vx . . 3 setvar 𝑥
3 vy . . 3 setvar 𝑦
4 cmgm 17845 . . 3 class Mgm
5 vu . . . . . . . . . 10 setvar 𝑢
65cv 1537 . . . . . . . . 9 class 𝑢
7 vv . . . . . . . . . 10 setvar 𝑣
87cv 1537 . . . . . . . . 9 class 𝑣
92cv 1537 . . . . . . . . . 10 class 𝑥
10 cplusg 16560 . . . . . . . . . 10 class +g
119, 10cfv 6328 . . . . . . . . 9 class (+g𝑥)
126, 8, 11co 7139 . . . . . . . 8 class (𝑢(+g𝑥)𝑣)
13 vf . . . . . . . . 9 setvar 𝑓
1413cv 1537 . . . . . . . 8 class 𝑓
1512, 14cfv 6328 . . . . . . 7 class (𝑓‘(𝑢(+g𝑥)𝑣))
166, 14cfv 6328 . . . . . . . 8 class (𝑓𝑢)
178, 14cfv 6328 . . . . . . . 8 class (𝑓𝑣)
183cv 1537 . . . . . . . . 9 class 𝑦
1918, 10cfv 6328 . . . . . . . 8 class (+g𝑦)
2016, 17, 19co 7139 . . . . . . 7 class ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2115, 20wceq 1538 . . . . . 6 wff (𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
22 cbs 16478 . . . . . . 7 class Base
239, 22cfv 6328 . . . . . 6 class (Base‘𝑥)
2421, 7, 23wral 3109 . . . . 5 wff 𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2524, 5, 23wral 3109 . . . 4 wff 𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))
2618, 22cfv 6328 . . . . 5 class (Base‘𝑦)
27 csethom 34532 . . . . 5 class Set
2823, 26, 27co 7139 . . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
2925, 13, 28crab 3113 . . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))}
302, 3, 4, 4, 29cmpo 7141 . 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g𝑥)𝑣)) = ((𝑓𝑢)(+g𝑦)(𝑓𝑣))})
311, 30wceq 1538 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