Definition df-bj-mgmhom 37178

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 37177	. 2 class Mgm⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cmgm 18552	. . 3 class Mgm
5		vu	. . . . . . . . . 10 setvar 𝑢
6	5	cv 1540	. . . . . . . . 9 class 𝑢
7		vv	. . . . . . . . . 10 setvar 𝑣
8	7	cv 1540	. . . . . . . . 9 class 𝑣
9	2	cv 1540	. . . . . . . . . 10 class 𝑥
10		cplusg 17167	. . . . . . . . . 10 class +g
11	9, 10	cfv 6487	. . . . . . . . 9 class (+g‘𝑥)
12	6, 8, 11	co 7352	. . . . . . . 8 class (𝑢(+g‘𝑥)𝑣)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1540	. . . . . . . 8 class 𝑓
15	12, 14	cfv 6487	. . . . . . 7 class (𝑓‘(𝑢(+g‘𝑥)𝑣))
16	6, 14	cfv 6487	. . . . . . . 8 class (𝑓‘𝑢)
17	8, 14	cfv 6487	. . . . . . . 8 class (𝑓‘𝑣)
18	3	cv 1540	. . . . . . . . 9 class 𝑦
19	18, 10	cfv 6487	. . . . . . . 8 class (+g‘𝑦)
20	16, 17, 19	co 7352	. . . . . . 7 class ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
21	15, 20	wceq 1541	. . . . . 6 wff (𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
22		cbs 17126	. . . . . . 7 class Base
23	9, 22	cfv 6487	. . . . . 6 class (Base‘𝑥)
24	21, 7, 23	wral 3047	. . . . 5 wff ∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
25	24, 5, 23	wral 3047	. . . 4 wff ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
26	18, 22	cfv 6487	. . . . 5 class (Base‘𝑦)
27		csethom 37173	. . . . 5 class Set⟶
28	23, 26, 27	co 7352	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
29	25, 13, 28	crab 3395	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}
30	2, 3, 4, 4, 29	cmpo 7354	. 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})
31	1, 30	wceq 1541	1 wff Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})

This definition is referenced by: (None)