Metamath Proof Explorer

Definition df-mgmhm

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

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 cmgmhm 
 |-  MgmHom
1 vs 
 |-  s
2 cmgm 
 |-  Mgm
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 27 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 ) ) }
29 1 3 2 2 28 cmpo 
 |-  ( 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 ) ) } )
30 0 29 wceq 
 |-  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 ) ) } )