# 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 ) ) } )`