Metamath Proof Explorer

Table of Contents - 19.4. Subspaces and projections

1. Subspaces
   1. df-sh
   2. issh
   3. issh2
   4. shss
   5. shel
   6. shex
   7. shssii
   8. sheli
   9. shelii
   10. sh0
   11. shaddcl
   12. shmulcl
   13. issh3
   14. shsubcl
2. Closed subspaces
   1. df-ch
   2. isch
   3. isch2
   4. chsh
   5. chsssh
   6. chex
   7. chshii
   8. ch0
   9. chss
   10. chel
   11. chssii
   12. cheli
   13. chelii
   14. chlimi
   15. hlim0
   16. hlimcaui
   17. hlimf
   18. hlimuni
   19. hlimreui
   20. hlimeui
   21. isch3
   22. chcompl
   23. helch
   24. ifchhv
   25. helsh
   26. shsspwh
   27. chsspwh
   28. hsn0elch
   29. norm1
   30. norm1exi
   31. norm1hex
3. Orthocomplements
   1. df-oc
   2. df-ch0
   3. elch0
   4. h0elch
   5. h0elsh
   6. hhssva
   7. hhsssm
   8. hhssnm
   9. issubgoilem
   10. hhssabloilem
   11. hhssabloi
   12. hhssablo
   13. hhssnv
   14. hhssnvt
   15. hhsst
   16. hhshsslem1
   17. hhshsslem2
   18. hhsssh
   19. hhsssh2
   20. hhssba
   21. hhssvs
   22. hhssvsf
   23. hhssims
   24. hhssims2
   25. hhssmet
   26. hhssmetdval
   27. hhsscms
   28. hhssbnOLD
   29. ocval
   30. ocel
   31. shocel
   32. ocsh
   33. shocsh
   34. ocss
   35. shocss
   36. occon
   37. occon2
   38. occon2i
   39. oc0
   40. ocorth
   41. shocorth
   42. ococss
   43. shococss
   44. shorth
   45. ocin
   46. occon3
   47. ocnel
   48. chocvali
   49. shuni
   50. chocunii
   51. pjhthmo
   52. occllem
   53. occl
   54. shoccl
   55. choccl
   56. choccli
4. Subspace sum, span, lattice join, lattice supremum
   1. df-shs
   2. df-span
   3. df-chj
   4. df-chsup
   5. shsval
   6. shsss
   7. shsel
   8. shsel3
   9. shseli
   10. shscli
   11. shscl
   12. shscom
   13. shsva
   14. shsel1
   15. shsel2
   16. shsvs
   17. shsub1
   18. shsub2
   19. choc0
   20. choc1
   21. chocnul
   22. shintcli
   23. shintcl
   24. chintcli
   25. chintcl
   26. spanval
   27. hsupval
   28. chsupval
   29. spancl
   30. elspancl
   31. shsupcl
   32. hsupcl
   33. chsupcl
   34. hsupss
   35. chsupss
   36. hsupunss
   37. chsupunss
   38. spanss2
   39. shsupunss
   40. spanid
   41. spanss
   42. spanssoc
   43. sshjval
   44. shjval
   45. chjval
   46. chjvali
   47. sshjval3
   48. sshjcl
   49. shjcl
   50. chjcl
   51. shjcom
   52. shless
   53. shlej1
   54. shlej2
   55. shincli
   56. shscomi
   57. shsvai
   58. shsel1i
   59. shsel2i
   60. shsvsi
   61. shunssi
   62. shunssji
   63. shsleji
   64. shjcomi
   65. shsub1i
   66. shsub2i
   67. shub1i
   68. shjcli
   69. shjshcli
   70. shlessi
   71. shlej1i
   72. shlej2i
   73. shslej
   74. shincl
   75. shub1
   76. shub2
   77. shsidmi
   78. shslubi
   79. shlesb1i
   80. shsval2i
   81. shsval3i
   82. shmodsi
   83. shmodi
5. Projection theorem
   1. pjhthlem1
   2. pjhthlem2
   3. pjhth
   4. pjhtheu
6. Projectors
   1. df-pjh
   2. pjhfval
   3. pjhval
   4. pjpreeq
   5. pjeq
   6. axpjcl
   7. pjhcl