Definition df-mhm 15945

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 15943	. 2 class MndHom
2		vs	. . 3 setvar s
3		vt	. . 3 setvar t
4		cmnd 15898	. . 3 class Mnd
5		vx	. . . . . . . . . . 11 setvar x
6	5	cv 1382	. . . . . . . . . 10 class x
7		vy	. . . . . . . . . . 11 setvar y
8	7	cv 1382	. . . . . . . . . 10 class y
9	2	cv 1382	. . . . . . . . . . 11 class s
10		cplusg 14679	. . . . . . . . . . 11 class +g
11	9, 10	cfv 5578	. . . . . . . . . 10 class ( +g ` s )
12	6, 8, 11	co 6281	. . . . . . . . 9 class ( x ( +g ` s ) y )
13		vf	. . . . . . . . . 10 setvar f
14	13	cv 1382	. . . . . . . . 9 class f
15	12, 14	cfv 5578	. . . . . . . 8 class ( f ` ( x ( +g ` s ) y ) )
16	6, 14	cfv 5578	. . . . . . . . 9 class ( f ` x )
17	8, 14	cfv 5578	. . . . . . . . 9 class ( f ` y )
18	3	cv 1382	. . . . . . . . . 10 class t
19	18, 10	cfv 5578	. . . . . . . . 9 class ( +g ` t )
20	16, 17, 19	co 6281	. . . . . . . 8 class ( ( f ` x ) ( +g ` t ) ( f ` y ) )
21	15, 20	wceq 1383	. . . . . . 7 wff ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
22		cbs 14614	. . . . . . . 8 class Base
23	9, 22	cfv 5578	. . . . . . 7 class ( Base ` s )
24	21, 7, 23	wral 2793	. . . . . 6 wff A. y e. ( Base ` s ) ( f ` ( x ( +g ` s ) y ) ) = ( ( f ` x ) ( +g ` t ) ( f ` y ) )
25	24, 5, 23	wral 2793	. . . . 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 14819	. . . . . . . 8 class 0g
27	9, 26	cfv 5578	. . . . . . 7 class ( 0g ` s )
28	27, 14	cfv 5578	. . . . . 6 class ( f ` ( 0g ` s ) )
29	18, 26	cfv 5578	. . . . . 6 class ( 0g ` t )
30	28, 29	wceq 1383	. . . . 5 wff ( f ` ( 0g ` s ) ) = ( 0g ` t )
31	25, 30	wa 369	. . . 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 5578	. . . . 5 class ( Base ` t )
33		cmap 7422	. . . . 5 class ^m
34	32, 23, 33	co 6281	. . . 4 class ( ( Base ` t ) ^m ( Base ` s ) )
35	31, 13, 34	crab 2797	. . 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	cmpt2 6283	. 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 1383	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  15947  mhmrcl1  15948  mhmrcl2  15949