Definition df-bj-mgmhom

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)

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

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgmhom	⊢ Mgm⟶
1		vx	⊢ 𝑥
2		cmgm	⊢ Mgm
3		vy	⊢ 𝑦
4		vf	⊢ 𝑓
5		cbs	⊢ Base
6	1	cv	⊢ 𝑥
7	6 5	cfv	⊢ ( Base ‘ 𝑥 )
8		csethom	⊢ Set⟶
9	3	cv	⊢ 𝑦
10	9 5	cfv	⊢ ( Base ‘ 𝑦 )
11	7 10 8	co	⊢ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) )
12		vu	⊢ 𝑢
13		vv	⊢ 𝑣
14	4	cv	⊢ 𝑓
15	12	cv	⊢ 𝑢
16		cplusg	⊢ +g
17	6 16	cfv	⊢ ( +g ‘ 𝑥 )
18	13	cv	⊢ 𝑣
19	15 18 17	co	⊢ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 )
20	19 14	cfv	⊢ ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) )
21	15 14	cfv	⊢ ( 𝑓 ‘ 𝑢 )
22	9 16	cfv	⊢ ( +g ‘ 𝑦 )
23	18 14	cfv	⊢ ( 𝑓 ‘ 𝑣 )
24	21 23 22	co	⊢ ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) )
25	20 24	wceq	⊢ ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) )
26	25 13 7	wral	⊢ ∀ 𝑣 ∈ ( Base ‘ 𝑥 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) )
27	26 12 7	wral	⊢ ∀ 𝑢 ∈ ( Base ‘ 𝑥 ) ∀ 𝑣 ∈ ( Base ‘ 𝑥 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) )
28	27 4 11	crab	⊢ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( Base ‘ 𝑥 ) ∀ 𝑣 ∈ ( Base ‘ 𝑥 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) ) }
29	1 3 2 2 28	cmpo	⊢ ( 𝑥 ∈ Mgm , 𝑦 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( Base ‘ 𝑥 ) ∀ 𝑣 ∈ ( Base ‘ 𝑥 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) ) } )
30	0 29	wceq	⊢ Mgm⟶ = ( 𝑥 ∈ Mgm , 𝑦 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑥 ) Set⟶ ( Base ‘ 𝑦 ) ) ∣ ∀ 𝑢 ∈ ( Base ‘ 𝑥 ) ∀ 𝑣 ∈ ( Base ‘ 𝑥 ) ( 𝑓 ‘ ( 𝑢 ( +g ‘ 𝑥 ) 𝑣 ) ) = ( ( 𝑓 ‘ 𝑢 ) ( +g ‘ 𝑦 ) ( 𝑓 ‘ 𝑣 ) ) } )