Definition df-mhm 13091

Description: A monoid homomorphism is a function on the base sets which preserves the binary operation and the identity. (Contributed by Mario Carneiro, 7-Mar-2015.)

Assertion

Ref	Expression
df-mhm	|- MndHom = ( s e. Mnd , t e. Mnd |-> { 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 ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )

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

Detailed syntax breakdown of Definition df-mhm

Step	Hyp	Ref	Expression
1		cmhm 13089	. 2 class MndHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cmnd 13057	. . 3 class Mnd
5		vx	. . . . . . . . . . 11 setvar x
6	5	cv 1363	. . . . . . . . . 10 class x
7		vy	. . . . . . . . . . 11 setvar y
8	7	cv 1363	. . . . . . . . . 10 class y
9	2	cv 1363	. . . . . . . . . . 11 class s
10		cplusg 12755	. . . . . . . . . . 11 class +g
11	9, 10	cfv 5258	. . . . . . . . . 10 class ( +g ` s )
12	6, 8, 11	co 5922	. . . . . . . . 9 class ( x ( +g ` s ) y )
13		vf	. . . . . . . . . 10 setvar f
14	13	cv 1363	. . . . . . . . 9 class f
15	12, 14	cfv 5258	. . . . . . . 8 class ( f ` ( x ( +g ` s ) y ) )
16	6, 14	cfv 5258	. . . . . . . . 9 class ( f ` x )
17	8, 14	cfv 5258	. . . . . . . . 9 class ( f ` y )
18	3	cv 1363	. . . . . . . . . 10 class t
19	18, 10	cfv 5258	. . . . . . . . 9 class ( +g ` t )
20	16, 17, 19	co 5922	. . . . . . . 8 class ( ( f ` x ) ( +g ` t ) ( f ` y ) )
21	15, 20	wceq 1364	. . . . . . 7 wff ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
22		cbs 12678	. . . . . . . 8 class Base
23	9, 22	cfv 5258	. . . . . . 7 class ( Base ` s )
24	21, 7, 23	wral 2475	. . . . . 6 wff A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
25	24, 5, 23	wral 2475	. . . . 5 wff A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
26		c0g 12927	. . . . . . . 8 class 0g
27	9, 26	cfv 5258	. . . . . . 7 class ( 0g ` s )
28	27, 14	cfv 5258	. . . . . 6 class ( f ` ( 0g ` s ) )
29	18, 26	cfv 5258	. . . . . 6 class ( 0g ` t )
30	28, 29	wceq 1364	. . . . 5 wff ( f ` ( 0g ` s ) ) = ( 0g ` t )
31	25, 30	wa 104	. . . 4 wff ( A. x e. ( Base ` s ) A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) )
32	18, 22	cfv 5258	. . . . 5 class ( Base ` t )
33		cmap 6707	. . . . 5 class ^m
34	32, 23, 33	co 5922	. . . 4 class ( ( Base ` t ) ^m ( Base ` s ) )
35	31, 13, 34	crab 2479	. . 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 ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) }
36	2, 3, 4, 4, 35	cmpo 5924	. 2 class ( s e. Mnd , t e. Mnd |-> { 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 ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )
37	1, 36	wceq 1364	1 wff MndHom = ( s e. Mnd , t e. Mnd |-> { 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 ) ) /\ ( f ` ( 0g ` s ) ) = ( 0g ` t ) ) } )

This definition is referenced by:  ismhm  13093  mhmex  13094  mhmrcl1  13095  mhmrcl2  13096