Definition df-mgmhm 41779

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

Assertion

Ref	Expression
df-mgmhm	|- MgmHom = ( s e. Mgm , t e. Mgm |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) } )

Distinct variable group:   t, s, f, x, y

Detailed syntax breakdown of Definition df-mgmhm

Step	Hyp	Ref	Expression
1		cmgmhm 41777	. 2 class MgmHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cmgm 17240	. . 3 class Mgm
5		vx	. . . . . . . . . 10 setvar x
6	5	cv 1482	. . . . . . . . 9 class x
7		vy	. . . . . . . . . 10 setvar y
8	7	cv 1482	. . . . . . . . 9 class y
9	2	cv 1482	. . . . . . . . . 10 class s
10		cplusg 15941	. . . . . . . . . 10 class +g
11	9, 10	cfv 5888	. . . . . . . . 9 class ( +g ` s )
12	6, 8, 11	co 6650	. . . . . . . 8 class ( x ( +g ` s ) y )
13		vf	. . . . . . . . 9 setvar f
14	13	cv 1482	. . . . . . . 8 class f
15	12, 14	cfv 5888	. . . . . . 7 class ( f ` ( x ( +g ` s ) y ) )
16	6, 14	cfv 5888	. . . . . . . 8 class ( f ` x )
17	8, 14	cfv 5888	. . . . . . . 8 class ( f ` y )
18	3	cv 1482	. . . . . . . . 9 class t
19	18, 10	cfv 5888	. . . . . . . 8 class ( +g ` t )
20	16, 17, 19	co 6650	. . . . . . 7 class ( ( f ` x ) ( +g ` t ) ( f ` y ) )
21	15, 20	wceq 1483	. . . . . 6 wff ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
22		cbs 15857	. . . . . . 7 class Base
23	9, 22	cfv 5888	. . . . . 6 class ( Base ` s )
24	21, 7, 23	wral 2912	. . . . 5 wff A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
25	24, 5, 23	wral 2912	. . . 4 wff A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
26	18, 22	cfv 5888	. . . . 5 class ( Base ` t )
27		cmap 7857	. . . . 5 class ^m
28	26, 23, 27	co 6650	. . . 4 class ( ( Base ` t ) ^m ( Base ` s ) )
29	25, 13, 28	crab 2916	. . 3 class { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) }
30	2, 3, 4, 4, 29	cmpt2 6652	. 2 class ( s e. Mgm , t e. Mgm |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) } )
31	1, 30	wceq 1483	1 wff MgmHom = ( s e. Mgm , t e. Mgm |-> { f e. ( ( Base ` t ) ^m ( Base ` s ) ) | A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) } )

This definition is referenced by:  mgmhmrcl  41781  ismgmhm  41783