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

Definition df-mhm 16660
 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 16658 . 2 MndHom
2 vs . . 3
3 vt . . 3
4 cmnd 16613 . . 3
5 vx . . . . . . . . . . 11
65cv 1451 . . . . . . . . . 10
7 vy . . . . . . . . . . 11
87cv 1451 . . . . . . . . . 10
92cv 1451 . . . . . . . . . . 11
10 cplusg 15268 . . . . . . . . . . 11
119, 10cfv 5589 . . . . . . . . . 10
126, 8, 11co 6308 . . . . . . . . 9
13 vf . . . . . . . . . 10
1413cv 1451 . . . . . . . . 9
1512, 14cfv 5589 . . . . . . . 8
166, 14cfv 5589 . . . . . . . . 9
178, 14cfv 5589 . . . . . . . . 9
183cv 1451 . . . . . . . . . 10
1918, 10cfv 5589 . . . . . . . . 9
2016, 17, 19co 6308 . . . . . . . 8
2115, 20wceq 1452 . . . . . . 7
22 cbs 15199 . . . . . . . 8
239, 22cfv 5589 . . . . . . 7
2421, 7, 23wral 2756 . . . . . 6
2524, 5, 23wral 2756 . . . . 5
26 c0g 15416 . . . . . . . 8
279, 26cfv 5589 . . . . . . 7
2827, 14cfv 5589 . . . . . 6
2918, 26cfv 5589 . . . . . 6
3028, 29wceq 1452 . . . . 5
3125, 30wa 376 . . . 4
3218, 22cfv 5589 . . . . 5
33 cmap 7490 . . . . 5
3432, 23, 33co 6308 . . . 4
3531, 13, 34crab 2760 . . 3
362, 3, 4, 4, 35cmpt2 6310 . 2
371, 36wceq 1452 1 MndHom
 Colors of variables: wff setvar class This definition is referenced by:  ismhm  16662  mhmrcl1  16663  mhmrcl2  16664
 Copyright terms: Public domain W3C validator