Definition df-bj-mgmhom 38139

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 38138	. 2 class ⎯⎯⟶Mgm
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cmgm 18819	. . 3 class Mgm
5		vu	. . . . . . . . . 10 setvar 𝑢
6	5	cv 1568	. . . . . . . . 9 class 𝑢
7		vv	. . . . . . . . . 10 setvar 𝑣
8	7	cv 1568	. . . . . . . . 9 class 𝑣
9	2	cv 1568	. . . . . . . . . 10 class 𝑥
10		cplusg 17433	. . . . . . . . . 10 class +g
11	9, 10	cfv 6538	. . . . . . . . 9 class (+g‘𝑥)
12	6, 8, 11	co 7420	. . . . . . . 8 class (𝑢(+g‘𝑥)𝑣)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1568	. . . . . . . 8 class 𝑓
15	12, 14	cfv 6538	. . . . . . 7 class (𝑓‘(𝑢(+g‘𝑥)𝑣))
16	6, 14	cfv 6538	. . . . . . . 8 class (𝑓‘𝑢)
17	8, 14	cfv 6538	. . . . . . . 8 class (𝑓‘𝑣)
18	3	cv 1568	. . . . . . . . 9 class 𝑦
19	18, 10	cfv 6538	. . . . . . . 8 class (+g‘𝑦)
20	16, 17, 19	co 7420	. . . . . . 7 class ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
21	15, 20	wceq 1569	. . . . . 6 wff (𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
22		cbs 17392	. . . . . . 7 class Base
23	9, 22	cfv 6538	. . . . . 6 class (Base‘𝑥)
24	21, 7, 23	wral 3076	. . . . 5 wff ∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
25	24, 5, 23	wral 3076	. . . 4 wff ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
26	18, 22	cfv 6538	. . . . 5 class (Base‘𝑦)
27		csethom 38134	. . . . 5 class ⟶Set
28	23, 26, 27	co 7420	. . . 4 class ((Base‘𝑥) ⟶Set (Base‘𝑦))
29	25, 13, 28	crab 3412	. . 3 class {𝑓 ∈ ((Base‘𝑥) ⟶Set (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}
30	2, 3, 4, 4, 29	cmpo 7422	. 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) ⟶Set (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})
31	1, 30	wceq 1569	1 wff ⎯⎯⟶Mgm = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) ⟶Set (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})

This definition is used by: (None)