Metamath Proof Explorer

Table of Contents - 10.1. Monoids

1. Magmas
   1. cplusf
   2. cmgm
   3. df-plusf
   4. df-mgm
   5. ismgm
   6. ismgmn0
   7. mgmcl
   8. isnmgm
   9. mgmsscl
   10. plusffval
   11. plusfval
   12. plusfeq
   13. plusffn
   14. mgmplusf
   15. issstrmgm
   16. intopsn
   17. mgmb1mgm1
   18. mgm0
   19. mgm0b
   20. mgm1
   21. opifismgm
2. Identity elements
   1. mgmidmo
   2. grpidval
   3. grpidpropd
   4. fn0g
   5. 0g0
   6. ismgmid
   7. mgmidcl
   8. mgmlrid
   9. ismgmid2
   10. lidrideqd
   11. lidrididd
   12. grpidd
   13. mgmidsssn0
   14. grprinvlem
   15. grprinvd
   16. grpridd
3. Iterated sums in a magma
   1. gsumvalx
   2. gsumval
   3. gsumpropd
   4. gsumpropd2lem
   5. gsumpropd2
   6. gsummgmpropd
   7. gsumress
   8. gsumval1
   9. gsum0
   10. gsumval2a
   11. gsumval2
   12. gsumsplit1r
   13. gsumprval
   14. gsumpr12val
4. Semigroups
   1. csgrp
   2. df-sgrp
   3. issgrp
   4. issgrpv
   5. issgrpn0
   6. isnsgrp
   7. sgrpmgm
   8. sgrpass
   9. sgrp0
   10. sgrp0b
   11. sgrp1
5. Definition and basic properties of monoids
   1. cmnd
   2. df-mnd
   3. ismnddef
   4. ismnd
   5. isnmnd
   6. sgrpidmnd
   7. mndsgrp
   8. mndmgm
   9. mndcl
   10. mndass
   11. mndid
   12. mndideu
   13. mnd32g
   14. mnd12g
   15. mnd4g
   16. mndidcl
   17. mndbn0
   18. hashfinmndnn
   19. mndplusf
   20. mndlrid
   21. mndlid
   22. mndrid
   23. ismndd
   24. mndpfo
   25. mndfo
   26. mndpropd
   27. mndprop
   28. issubmnd
   29. ress0g
   30. submnd0
   31. mndinvmod
   32. prdsplusgcl
   33. prdsidlem
   34. prdsmndd
   35. prds0g
   36. pwsmnd
   37. pws0g
   38. imasmnd2
   39. imasmnd
   40. imasmndf1
   41. xpsmnd
   42. mnd1
   43. mnd1id
6. Monoid homomorphisms and submonoids
   1. cmhm
   2. csubmnd
   3. df-mhm
   4. df-submnd
   5. ismhm
   6. mhmrcl1
   7. mhmrcl2
   8. mhmf
   9. mhmpropd
   10. mhmlin
   11. mhm0
   12. idmhm
   13. mhmf1o
   14. submrcl
   15. issubm
   16. issubm2
   17. issubmndb
   18. issubmd
   19. mndissubm
   20. resmndismnd
   21. submss
   22. submid
   23. subm0cl
   24. submcl
   25. submmnd
   26. submbas
   27. subm0
   28. subsubm
   29. 0subm
   30. insubm
   31. 0mhm
   32. resmhm
   33. resmhm2
   34. resmhm2b
   35. mhmco
   36. mhmima
   37. mhmeql
   38. submacs
   39. mndind
   40. prdspjmhm
   41. pwspjmhm
   42. pwsdiagmhm
   43. pwsco1mhm
   44. pwsco2mhm
7. Iterated sums in a monoid
   1. gsumvallem2
   2. gsumsubm
   3. gsumz
   4. gsumwsubmcl
   5. gsumws1
   6. gsumwcl
   7. gsumsgrpccat
   8. gsumccatOLD
   9. gsumccat
   10. gsumws2
   11. gsumccatsn
   12. gsumspl
   13. gsumwmhm
   14. gsumwspan
8. Free monoids
   1. cfrmd
   2. cvrmd
   3. df-frmd
   4. df-vrmd
   5. frmdval
   6. frmdbas
   7. frmdelbas
   8. frmdplusg
   9. frmdadd
   10. vrmdfval
   11. vrmdval
   12. vrmdf
   13. frmdmnd
   14. frmd0
   15. frmdsssubm
   16. frmdgsum
   17. frmdss2
   18. frmdup1
   19. frmdup2
   20. frmdup3lem
   21. frmdup3
   22. Monoid of endofunctions
9. Examples and counterexamples for magmas, semigroups and monoids
   1. mgm2nsgrplem1
   2. mgm2nsgrplem2
   3. mgm2nsgrplem3
   4. mgm2nsgrplem4
   5. mgm2nsgrp
   6. sgrp2nmndlem1
   7. sgrp2nmndlem2
   8. sgrp2nmndlem3
   9. sgrp2rid2
   10. sgrp2rid2ex
   11. sgrp2nmndlem4
   12. sgrp2nmndlem5
   13. sgrp2nmnd
   14. mgmnsgrpex
   15. sgrpnmndex
   16. sgrpssmgm
   17. mndsssgrp
   18. pwmndgplus
   19. pwmndid
   20. pwmnd