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

Definition df-mhm 14743
 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
Distinct variable group:   ,,,,

Detailed syntax breakdown of Definition df-mhm
StepHypRef Expression
1 cmhm 14741 . 2 MndHom
2 vs . . 3
3 vt . . 3
4 cmnd 14689 . . 3
5 vx . . . . . . . . . . 11
65cv 1652 . . . . . . . . . 10
7 vy . . . . . . . . . . 11
87cv 1652 . . . . . . . . . 10
92cv 1652 . . . . . . . . . . 11
10 cplusg 13534 . . . . . . . . . . 11
119, 10cfv 5457 . . . . . . . . . 10
126, 8, 11co 6084 . . . . . . . . 9
13 vf . . . . . . . . . 10
1413cv 1652 . . . . . . . . 9
1512, 14cfv 5457 . . . . . . . 8
166, 14cfv 5457 . . . . . . . . 9
178, 14cfv 5457 . . . . . . . . 9
183cv 1652 . . . . . . . . . 10
1918, 10cfv 5457 . . . . . . . . 9
2016, 17, 19co 6084 . . . . . . . 8
2115, 20wceq 1653 . . . . . . 7
22 cbs 13474 . . . . . . . 8
239, 22cfv 5457 . . . . . . 7
2421, 7, 23wral 2707 . . . . . 6
2524, 5, 23wral 2707 . . . . 5
26 c0g 13728 . . . . . . . 8
279, 26cfv 5457 . . . . . . 7
2827, 14cfv 5457 . . . . . 6
2918, 26cfv 5457 . . . . . 6
3028, 29wceq 1653 . . . . 5
3125, 30wa 360 . . . 4
3218, 22cfv 5457 . . . . 5
33 cmap 7021 . . . . 5
3432, 23, 33co 6084 . . . 4
3531, 13, 34crab 2711 . . 3
362, 3, 4, 4, 35cmpt2 6086 . 2
371, 36wceq 1653 1 MndHom
 Colors of variables: wff set class This definition is referenced by:  ismhm  14745  mhmrcl1  14746  mhmrcl2  14747
 Copyright terms: Public domain W3C validator