Metamath Proof Explorer

Table of Contents - 10.5. Left modules

1. Definition and basic properties
   1. clmod
   2. cscaf
   3. df-lmod
   4. df-scaf
   5. islmod
   6. lmodlema
   7. islmodd
   8. lmodgrp
   9. lmodring
   10. lmodfgrp
   11. lmodgrpd
   12. lmodbn0
   13. lmodacl
   14. lmodmcl
   15. lmodsn0
   16. lmodvacl
   17. lmodass
   18. lmodlcan
   19. lmodvscl
   20. lmodvscld
   21. scaffval
   22. scafval
   23. scafeq
   24. scaffn
   25. lmodscaf
   26. lmodvsdi
   27. lmodvsdir
   28. lmodvsass
   29. lmod0cl
   30. lmod1cl
   31. lmodvs1
   32. lmod0vcl
   33. lmod0vlid
   34. lmod0vrid
   35. lmod0vid
   36. lmod0vs
   37. lmodvs0
   38. lmodvsmmulgdi
   39. lmodfopnelem1
   40. lmodfopnelem2
   41. lmodfopne
   42. lcomf
   43. lcomfsupp
   44. lmodvnegcl
   45. lmodvnegid
   46. lmodvneg1
   47. lmodvsneg
   48. lmodvsubcl
   49. lmodcom
   50. lmodabl
   51. lmodcmn
   52. lmodnegadd
   53. lmod4
   54. lmodvsubadd
   55. lmodvaddsub4
   56. lmodvpncan
   57. lmodvnpcan
   58. lmodvsubval2
   59. lmodsubvs
   60. lmodsubdi
   61. lmodsubdir
   62. lmodsubeq0
   63. lmodsubid
   64. lmodvsghm
   65. lmodprop2d
   66. lmodpropd
   67. gsumvsmul
   68. mptscmfsupp0
   69. mptscmfsuppd
   70. rmodislmodlem
   71. rmodislmod
2. Subspaces and spans in a left module
   1. clss
   2. df-lss
   3. lssset
   4. islss
   5. islssd
   6. lssss
   7. lssel
   8. lss1
   9. lssuni
   10. lssn0
   11. 00lss
   12. lsscl
   13. lssvacl
   14. lssvsubcl
   15. lssvancl1
   16. lssvancl2
   17. lss0cl
   18. lsssn0
   19. lss0ss
   20. lssle0
   21. lssne0
   22. lssvneln0
   23. lssneln0
   24. lssssr
   25. lssvscl
   26. lssvnegcl
   27. lsssubg
   28. lsssssubg
   29. islss3
   30. lsslmod
   31. lsslss
   32. islss4
   33. lss1d
   34. lssintcl
   35. lssincl
   36. lssmre
   37. lssacs
   38. prdsvscacl
   39. prdslmodd
   40. pwslmod
   41. clspn
   42. df-lsp
   43. lspfval
   44. lspf
   45. lspval
   46. lspcl
   47. lspsncl
   48. lspprcl
   49. lsptpcl
   50. lspsnsubg
   51. 00lsp
   52. lspid
   53. lspssv
   54. lspss
   55. lspssid
   56. lspidm
   57. lspun
   58. lspssp
   59. mrclsp
   60. lspsnss
   61. ellspsn3
   62. lspprss
   63. lspsnid
   64. ellspsn6
   65. ellspsn5b
   66. ellspsn5
   67. lspprid1
   68. lspprid2
   69. lspprvacl
   70. lssats2
   71. ellspsni
   72. lspsn
   73. ellspsn
   74. lspsnvsi
   75. lspsnss2
   76. lspsnneg
   77. lspsnsub
   78. lspsn0
   79. lsp0
   80. lspuni0
   81. lspun0
   82. lspsneq0
   83. lspsneq0b
   84. lmodindp1
   85. lsslsp
   86. lsslspOLD
   87. lss0v
   88. lsspropd
   89. lsppropd
3. Homomorphisms and isomorphisms of left modules
   1. clmhm
   2. clmim
   3. clmic
   4. df-lmhm
   5. df-lmim
   6. df-lmic
   7. reldmlmhm
   8. lmimfn
   9. islmhm
   10. islmhm3
   11. lmhmlem
   12. lmhmsca
   13. lmghm
   14. lmhmlmod2
   15. lmhmlmod1
   16. lmhmf
   17. lmhmlin
   18. lmodvsinv
   19. lmodvsinv2
   20. islmhm2
   21. islmhmd
   22. 0lmhm
   23. idlmhm
   24. invlmhm
   25. lmhmco
   26. lmhmplusg
   27. lmhmvsca
   28. lmhmf1o
   29. lmhmima
   30. lmhmpreima
   31. lmhmlsp
   32. lmhmrnlss
   33. lmhmkerlss
   34. reslmhm
   35. reslmhm2
   36. reslmhm2b
   37. lmhmeql
   38. lspextmo
   39. pwsdiaglmhm
   40. pwssplit0
   41. pwssplit1
   42. pwssplit2
   43. pwssplit3
   44. islmim
   45. lmimf1o
   46. lmimlmhm
   47. lmimgim
   48. islmim2
   49. lmimcnv
   50. brlmic
   51. brlmici
   52. lmiclcl
   53. lmicrcl
   54. lmicsym
   55. lmhmpropd
4. Subspace sum; bases for a left module
   1. clbs
   2. df-lbs
   3. islbs
   4. lbsss
   5. lbsel
   6. lbssp
   7. lbsind
   8. lbsind2
   9. lbspss
   10. lsmcl
   11. lsmspsn
   12. lsmelval2
   13. lsmsp
   14. lsmsp2
   15. lsmssspx
   16. lsmpr
   17. lsppreli
   18. lsmelpr
   19. lsppr0
   20. lsppr
   21. lspprel
   22. lspprabs
   23. lspvadd
   24. lspsntri
   25. lspsntrim
   26. lbspropd
   27. pj1lmhm
   28. pj1lmhm2