Definition df-bj-mgmhom 37069

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

Step	Hyp	Ref	Expression
1		cmgmhom 37068	. 2 class Mgm⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cmgm 18625	. . 3 class Mgm
5		vu	. . . . . . . . . 10 setvar 𝑢
6	5	cv 1538	. . . . . . . . 9 class 𝑢
7		vv	. . . . . . . . . 10 setvar 𝑣
8	7	cv 1538	. . . . . . . . 9 class 𝑣
9	2	cv 1538	. . . . . . . . . 10 class 𝑥
10		cplusg 17277	. . . . . . . . . 10 class +g
11	9, 10	cfv 6542	. . . . . . . . 9 class (+g‘𝑥)
12	6, 8, 11	co 7414	. . . . . . . 8 class (𝑢(+g‘𝑥)𝑣)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1538	. . . . . . . 8 class 𝑓
15	12, 14	cfv 6542	. . . . . . 7 class (𝑓‘(𝑢(+g‘𝑥)𝑣))
16	6, 14	cfv 6542	. . . . . . . 8 class (𝑓‘𝑢)
17	8, 14	cfv 6542	. . . . . . . 8 class (𝑓‘𝑣)
18	3	cv 1538	. . . . . . . . 9 class 𝑦
19	18, 10	cfv 6542	. . . . . . . 8 class (+g‘𝑦)
20	16, 17, 19	co 7414	. . . . . . 7 class ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
21	15, 20	wceq 1539	. . . . . 6 wff (𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
22		cbs 17230	. . . . . . 7 class Base
23	9, 22	cfv 6542	. . . . . 6 class (Base‘𝑥)
24	21, 7, 23	wral 3050	. . . . 5 wff ∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
25	24, 5, 23	wral 3050	. . . 4 wff ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
26	18, 22	cfv 6542	. . . . 5 class (Base‘𝑦)
27		csethom 37064	. . . . 5 class Set⟶
28	23, 26, 27	co 7414	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
29	25, 13, 28	crab 3420	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}
30	2, 3, 4, 4, 29	cmpo 7416	. 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})
31	1, 30	wceq 1539	1 wff Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})

This definition is referenced by: (None)