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. mgmpropd
   16. ismgmd
   17. issstrmgm
   18. intopsn
   19. mgmb1mgm1
   20. mgm0
   21. mgm0b
   22. mgm1
   23. 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. grpinvalem
   15. grpinva
   16. grprida
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. Magma homomorphisms and submagmas
   1. cmgmhm
   2. csubmgm
   3. df-mgmhm
   4. df-submgm
   5. mgmhmrcl
   6. submgmrcl
   7. ismgmhm
   8. mgmhmf
   9. mgmhmpropd
   10. mgmhmlin
   11. mgmhmf1o
   12. idmgmhm
   13. issubmgm
   14. issubmgm2
   15. rabsubmgmd
   16. submgmss
   17. submgmid
   18. submgmcl
   19. submgmmgm
   20. submgmbas
   21. subsubmgm
   22. resmgmhm
   23. resmgmhm2
   24. resmgmhm2b
   25. mgmhmco
   26. mgmhmima
   27. mgmhmeql
   28. submgmacs
5. Semigroups
   1. csgrp
   2. df-sgrp
   3. issgrp
   4. issgrpv
   5. issgrpn0
   6. isnsgrp
   7. sgrpmgm
   8. sgrpass
   9. sgrpcl
   10. sgrp0
   11. sgrp0b
   12. sgrp1
   13. issgrpd
   14. sgrppropd
   15. prdsplusgsgrpcl
   16. prdssgrpd
6. 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. mndpsuppss
   33. mndpsuppfi
   34. mndpfsupp
   35. prdsplusgcl
   36. prdsidlem
   37. prdsmndd
   38. prds0g
   39. pwsmnd
   40. pws0g
   41. imasmnd2
   42. imasmnd
   43. imasmndf1
   44. xpsmnd
   45. xpsmnd0
   46. mnd1
   47. mnd1id
7. Monoid homomorphisms and submonoids
   1. cmhm
   2. csubmnd
   3. df-mhm
   4. df-submnd
   5. ismhm
   6. ismhmd
   7. mhmrcl1
   8. mhmrcl2
   9. mhmf
   10. ismhm0
   11. mhmismgmhm
   12. mhmpropd
   13. mhmlin
   14. mhm0
   15. idmhm
   16. mhmf1o
   17. mndvcl
   18. mndvass
   19. mndvlid
   20. mndvrid
   21. mhmvlin
   22. submrcl
   23. issubm
   24. issubm2
   25. issubmndb
   26. issubmd
   27. mndissubm
   28. resmndismnd
   29. submss
   30. submid
   31. subm0cl
   32. submcl
   33. submmnd
   34. submbas
   35. subm0
   36. subsubm
   37. 0subm
   38. insubm
   39. 0mhm
   40. resmhm
   41. resmhm2
   42. resmhm2b
   43. mhmco
   44. mhmimalem
   45. mhmima
   46. mhmeql
   47. submacs
   48. mndind
   49. prdspjmhm
   50. pwspjmhm
   51. pwsdiagmhm
   52. pwsco1mhm
   53. pwsco2mhm
8. Iterated sums in a monoid
   1. gsumvallem2
   2. gsumsubm
   3. gsumz
   4. gsumwsubmcl
   5. gsumws1
   6. gsumwcl
   7. gsumsgrpccat
   8. gsumccat
   9. gsumws2
   10. gsumccatsn
   11. gsumspl
   12. gsumwmhm
   13. gsumwspan
9. 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
10. 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