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. lmodbn0
   12. lmodacl
   13. lmodmcl
   14. lmodsn0
   15. lmodvacl
   16. lmodass
   17. lmodlcan
   18. lmodvscl
   19. scaffval
   20. scafval
   21. scafeq
   22. scaffn
   23. lmodscaf
   24. lmodvsdi
   25. lmodvsdir
   26. lmodvsass
   27. lmod0cl
   28. lmod1cl
   29. lmodvs1
   30. lmod0vcl
   31. lmod0vlid
   32. lmod0vrid
   33. lmod0vid
   34. lmod0vs
   35. lmodvs0
   36. lmodvsmmulgdi
   37. lmodfopnelem1
   38. lmodfopnelem2
   39. lmodfopne
   40. lcomf
   41. lcomfsupp
   42. lmodvnegcl
   43. lmodvnegid
   44. lmodvneg1
   45. lmodvsneg
   46. lmodvsubcl
   47. lmodcom
   48. lmodabl
   49. lmodcmn
   50. lmodnegadd
   51. lmod4
   52. lmodvsubadd
   53. lmodvaddsub4
   54. lmodvpncan
   55. lmodvnpcan
   56. lmodvsubval2
   57. lmodsubvs
   58. lmodsubdi
   59. lmodsubdir
   60. lmodsubeq0
   61. lmodsubid
   62. lmodvsghm
   63. lmodprop2d
   64. lmodpropd
   65. gsumvsmul
   66. mptscmfsupp0
   67. mptscmfsuppd
   68. rmodislmodlem
   69. 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. lssvsubcl
   14. lssvancl1
   15. lssvancl2
   16. lss0cl
   17. lsssn0
   18. lss0ss
   19. lssle0
   20. lssne0
   21. lssvneln0
   22. lssneln0
   23. lssssr
   24. lssvacl
   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. lspsnel3
   62. lspprss
   63. lspsnid
   64. lspsnel6
   65. lspsnel5
   66. lspsnel5a
   67. lspprid1
   68. lspprid2
   69. lspprvacl
   70. lssats2
   71. lspsneli
   72. lspsn
   73. lspsnel
   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. lss0v
   87. lsspropd
   88. 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