MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-mhm Unicode version

Definition df-mhm 14431
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
StepHypRef Expression
1 cmhm 14429 . 2  class MndHom
2 vs . . 3  set  s
3 vt . . 3  set  t
4 cmnd 14377 . . 3  class  Mnd
5 vx . . . . . . . . . . 11  set  x
65cv 1631 . . . . . . . . . 10  class  x
7 vy . . . . . . . . . . 11  set  y
87cv 1631 . . . . . . . . . 10  class  y
92cv 1631 . . . . . . . . . . 11  class  s
10 cplusg 13224 . . . . . . . . . . 11  class  +g
119, 10cfv 5271 . . . . . . . . . 10  class  ( +g  `  s )
126, 8, 11co 5874 . . . . . . . . 9  class  ( x ( +g  `  s
) y )
13 vf . . . . . . . . . 10  set  f
1413cv 1631 . . . . . . . . 9  class  f
1512, 14cfv 5271 . . . . . . . 8  class  ( f `
 ( x ( +g  `  s ) y ) )
166, 14cfv 5271 . . . . . . . . 9  class  ( f `
 x )
178, 14cfv 5271 . . . . . . . . 9  class  ( f `
 y )
183cv 1631 . . . . . . . . . 10  class  t
1918, 10cfv 5271 . . . . . . . . 9  class  ( +g  `  t )
2016, 17, 19co 5874 . . . . . . . 8  class  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )
2115, 20wceq 1632 . . . . . . 7  wff  ( f `
 ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t ) ( f `
 y ) )
22 cbs 13164 . . . . . . . 8  class  Base
239, 22cfv 5271 . . . . . . 7  class  ( Base `  s )
2421, 7, 23wral 2556 . . . . . 6  wff  A. y  e.  ( Base `  s
) ( f `  ( x ( +g  `  s ) y ) )  =  ( ( f `  x ) ( +g  `  t
) ( f `  y ) )
2524, 5, 23wral 2556 . . . . 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 13416 . . . . . . . 8  class  0g
279, 26cfv 5271 . . . . . . 7  class  ( 0g
`  s )
2827, 14cfv 5271 . . . . . 6  class  ( f `
 ( 0g `  s ) )
2918, 26cfv 5271 . . . . . 6  class  ( 0g
`  t )
3028, 29wceq 1632 . . . . 5  wff  ( f `
 ( 0g `  s ) )  =  ( 0g `  t
)
3125, 30wa 358 . . . 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 ) )
3218, 22cfv 5271 . . . . 5  class  ( Base `  t )
33 cmap 6788 . . . . 5  class  ^m
3432, 23, 33co 5874 . . . 4  class  ( (
Base `  t )  ^m  ( Base `  s
) )
3531, 13, 34crab 2560 . . 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 ) ) }
362, 3, 4, 4, 35cmpt2 5876 . 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 ) ) } )
371, 36wceq 1632 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
) ) } )
Colors of variables: wff set class
This definition is referenced by:  ismhm  14433  mhmrcl1  14434  mhmrcl2  14435
  Copyright terms: Public domain W3C validator