Definition df-mgmhm

Description: A magma homomorphism is a function on the base sets which preserves the binary operation. (Contributed by AV, 24-Feb-2020)

	Ref	Expression
Assertion	df-mgmhm	⊢ MgmHom = ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) } )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		cmgmhm	⊢ MgmHom
1		vs	⊢ 𝑠
2		cmgm	⊢ Mgm
3		vt	⊢ 𝑡
4		vf	⊢ 𝑓
5		cbs	⊢ Base
6	3	cv	⊢ 𝑡
7	6 5	cfv	⊢ ( Base ‘ 𝑡 )
8		cmap	⊢ ↑m
9	1	cv	⊢ 𝑠
10	9 5	cfv	⊢ ( Base ‘ 𝑠 )
11	7 10 8	co	⊢ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) )
12		vx	⊢ 𝑥
13		vy	⊢ 𝑦
14	4	cv	⊢ 𝑓
15	12	cv	⊢ 𝑥
16		cplusg	⊢ +g
17	9 16	cfv	⊢ ( +g ‘ 𝑠 )
18	13	cv	⊢ 𝑦
19	15 18 17	co	⊢ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 )
20	19 14	cfv	⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) )
21	15 14	cfv	⊢ ( 𝑓 ‘ 𝑥 )
22	6 16	cfv	⊢ ( +g ‘ 𝑡 )
23	18 14	cfv	⊢ ( 𝑓 ‘ 𝑦 )
24	21 23 22	co	⊢ ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
25	20 24	wceq	⊢ ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
26	25 13 10	wral	⊢ ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
27	26 12 10	wral	⊢ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) )
28	27 4 11	crab	⊢ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) }
29	1 3 2 2 28	cmpo	⊢ ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) } )
30	0 29	wceq	⊢ MgmHom = ( 𝑠 ∈ Mgm , 𝑡 ∈ Mgm ↦ { 𝑓 ∈ ( ( Base ‘ 𝑡 ) ↑m ( Base ‘ 𝑠 ) ) ∣ ∀ 𝑥 ∈ ( Base ‘ 𝑠 ) ∀ 𝑦 ∈ ( Base ‘ 𝑠 ) ( 𝑓 ‘ ( 𝑥 ( +g ‘ 𝑠 ) 𝑦 ) ) = ( ( 𝑓 ‘ 𝑥 ) ( +g ‘ 𝑡 ) ( 𝑓 ‘ 𝑦 ) ) } )