Definition df-bj-magmahom 33080

Description: Define the set of magma morphisms between two magmas. (Contributed by BJ, 10-Feb-2022.)

Assertion

Ref	Expression
df-bj-magmahom	⊢ Magma⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})

Distinct variable group:   𝑥,𝑓,𝑦,𝑢,𝑣

Detailed syntax breakdown of Definition df-bj-magmahom

Step	Hyp	Ref	Expression
1		cmagmahom 33077	. 2 class Magma⟶
2		vx	. . 3 setvar 𝑥
3		vy	. . 3 setvar 𝑦
4		cmgm 17240	. . 3 class Mgm
5		vu	. . . . . . . . . 10 setvar 𝑢
6	5	cv 1482	. . . . . . . . 9 class 𝑢
7		vv	. . . . . . . . . 10 setvar 𝑣
8	7	cv 1482	. . . . . . . . 9 class 𝑣
9	2	cv 1482	. . . . . . . . . 10 class 𝑥
10		cplusg 15941	. . . . . . . . . 10 class +g
11	9, 10	cfv 5888	. . . . . . . . 9 class (+g‘𝑥)
12	6, 8, 11	co 6650	. . . . . . . 8 class (𝑢(+g‘𝑥)𝑣)
13		vf	. . . . . . . . 9 setvar 𝑓
14	13	cv 1482	. . . . . . . 8 class 𝑓
15	12, 14	cfv 5888	. . . . . . 7 class (𝑓‘(𝑢(+g‘𝑥)𝑣))
16	6, 14	cfv 5888	. . . . . . . 8 class (𝑓‘𝑢)
17	8, 14	cfv 5888	. . . . . . . 8 class (𝑓‘𝑣)
18	3	cv 1482	. . . . . . . . 9 class 𝑦
19	18, 10	cfv 5888	. . . . . . . 8 class (+g‘𝑦)
20	16, 17, 19	co 6650	. . . . . . 7 class ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
21	15, 20	wceq 1483	. . . . . 6 wff (𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
22		cbs 15857	. . . . . . 7 class Base
23	9, 22	cfv 5888	. . . . . 6 class (Base‘𝑥)
24	21, 7, 23	wral 2912	. . . . 5 wff ∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
25	24, 5, 23	wral 2912	. . . 4 wff ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))
26	18, 22	cfv 5888	. . . . 5 class (Base‘𝑦)
27		csethom 33075	. . . . 5 class Set⟶
28	23, 26, 27	co 6650	. . . 4 class ((Base‘𝑥) Set⟶ (Base‘𝑦))
29	25, 13, 28	crab 2916	. . 3 class {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))}
30	2, 3, 4, 4, 29	cmpt2 6652	. 2 class (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})
31	1, 30	wceq 1483	1 wff Magma⟶ = (𝑥 ∈ Mgm, 𝑦 ∈ Mgm ↦ {𝑓 ∈ ((Base‘𝑥) Set⟶ (Base‘𝑦)) ∣ ∀𝑢 ∈ (Base‘𝑥)∀𝑣 ∈ (Base‘𝑥)(𝑓‘(𝑢(+g‘𝑥)𝑣)) = ((𝑓‘𝑢)(+g‘𝑦)(𝑓‘𝑣))})

This definition is referenced by: (None)