Definition df-bj-mgmhom 34990

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 34989	. 2 class Mgm⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cmgm 18084	. . 3 class Mgm
5		vu	. . . . . . . . . 10 setvar 𝑢
6	5	cv 1542	. . . . . . . . 9 class 𝑢
7		vv	. . . . . . . . . 10 setvar 𝑣
8	7	cv 1542	. . . . . . . . 9 class 𝑣
9	2	cv 1542	. . . . . . . . . 10 class 𝑥
10		cplusg 16767	. . . . . . . . . 10 class +g
11	9, 10	cfv 6369	. . . . . . . . 9 class (+g‘𝑥)
12	6, 8, 11	co 7202	. . . . . . . 8 class (𝑢(+g‘𝑥)𝑣)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1542	. . . . . . . 8 class 𝑓
15	12, 14	cfv 6369	. . . . . . 7 class (𝑓‘(𝑢(+g‘𝑥)𝑣))
16	6, 14	cfv 6369	. . . . . . . 8 class (𝑓‘𝑢)
17	8, 14	cfv 6369	. . . . . . . 8 class (𝑓‘𝑣)
18	3	cv 1542	. . . . . . . . 9 class 𝑦
19	18, 10	cfv 6369	. . . . . . . 8 class (+g‘𝑦)
20	16, 17, 19	co 7202	. . . . . . 7 class ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
21	15, 20	wceq 1543	. . . . . 6 wff (𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
22		cbs 16684	. . . . . . 7 class Base
23	9, 22	cfv 6369	. . . . . 6 class (Base‘𝑥)
24	21, 7, 23	wral 3054	. . . . 5 wff ∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
25	24, 5, 23	wral 3054	. . . 4 wff ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
26	18, 22	cfv 6369	. . . . 5 class (Base‘𝑦)
27		csethom 34985	. . . . 5 class Set⟶
28	23, 26, 27	co 7202	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
29	25, 13, 28	crab 3058	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}
30	2, 3, 4, 4, 29	cmpo 7204	. 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})
31	1, 30	wceq 1543	1 wff Mgm⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})

This definition is referenced by: (None)