This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Definition df-mhm

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)

Ref Expression
Assertion 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 ) ) } )

Detailed syntax breakdown

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