Definition df-bj-mgmhom 35298

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 35297	. 2 class Mgm⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cmgm 18324	. . 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 16962	. . . . . . . . . 10 class +g
11	9, 10	cfv 6433	. . . . . . . . 9 class (+g‘𝑥)
12	6, 8, 11	co 7275	. . . . . . . 8 class (𝑢(+g‘𝑥)𝑣)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1538	. . . . . . . 8 class 𝑓
15	12, 14	cfv 6433	. . . . . . 7 class (𝑓‘(𝑢(+g‘𝑥)𝑣))
16	6, 14	cfv 6433	. . . . . . . 8 class (𝑓‘𝑢)
17	8, 14	cfv 6433	. . . . . . . 8 class (𝑓‘𝑣)
18	3	cv 1538	. . . . . . . . 9 class 𝑦
19	18, 10	cfv 6433	. . . . . . . 8 class (+g‘𝑦)
20	16, 17, 19	co 7275	. . . . . . 7 class ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
21	15, 20	wceq 1539	. . . . . 6 wff (𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
22		cbs 16912	. . . . . . 7 class Base
23	9, 22	cfv 6433	. . . . . 6 class (Base‘𝑥)
24	21, 7, 23	wral 3064	. . . . 5 wff ∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
25	24, 5, 23	wral 3064	. . . 4 wff ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
26	18, 22	cfv 6433	. . . . 5 class (Base‘𝑦)
27		csethom 35293	. . . . 5 class Set⟶
28	23, 26, 27	co 7275	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
29	25, 13, 28	crab 3068	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}
30	2, 3, 4, 4, 29	cmpo 7277	. 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)