Metamath Proof Explorer

Table of Contents - 12.5. Metric subcomplex vector spaces

1. Subcomplex modules
   1. cclm
   2. df-clm
   3. isclm
   4. clmsca
   5. clmsubrg
   6. clmlmod
   7. clmgrp
   8. clmabl
   9. clmring
   10. clmfgrp
   11. clm0
   12. clm1
   13. clmadd
   14. clmmul
   15. clmcj
   16. isclmi
   17. clmzss
   18. clmsscn
   19. clmsub
   20. clmneg
   21. clmneg1
   22. clmabs
   23. clmacl
   24. clmmcl
   25. clmsubcl
   26. lmhmclm
   27. clmvscl
   28. clmvsass
   29. clmvscom
   30. clmvsdir
   31. clmvsdi
   32. clmvs1
   33. clmvs2
   34. clm0vs
   35. clmopfne
   36. isclmp
   37. isclmi0
   38. clmvneg1
   39. clmvsneg
   40. clmmulg
   41. clmsubdir
   42. clmpm1dir
   43. clmnegneg
   44. clmnegsubdi2
   45. clmsub4
   46. clmvsrinv
   47. clmvslinv
   48. clmvsubval
   49. clmvsubval2
   50. clmvz
   51. zlmclm
   52. clmzlmvsca
   53. nmoleub2lem
   54. nmoleub2lem3
   55. nmoleub2lem2
   56. nmoleub2a
   57. nmoleub2b
   58. nmoleub3
   59. nmhmcn
   60. cmodscexp
   61. cmodscmulexp
2. Subcomplex vector spaces
   1. ccvs
   2. df-cvs
   3. cvslvec
   4. cvsclm
   5. iscvs
   6. iscvsp
   7. iscvsi
   8. cvsi
   9. cvsunit
   10. cvsdiv
   11. cvsdivcl
   12. cvsmuleqdivd
   13. cvsdiveqd
   14. cnlmodlem1
   15. cnlmodlem2
   16. cnlmodlem3
   17. cnlmod4
   18. cnlmod
   19. cnstrcvs
   20. cnrbas
   21. cnrlmod
   22. cnrlvec
   23. cncvs
   24. recvs
   25. qcvs
   26. zclmncvs
3. Normed subcomplex vector spaces
   1. isncvsngp
   2. isncvsngpd
   3. ncvsi
   4. ncvsprp
   5. ncvsge0
   6. ncvsm1
   7. ncvsdif
   8. ncvspi
   9. ncvs1
   10. cnrnvc
   11. cnncvs
   12. cnnm
   13. ncvspds
   14. cnindmet
   15. cnncvsaddassdemo
   16. cnncvsmulassdemo
   17. cnncvsabsnegdemo
4. Subcomplex pre-Hilbert space
   1. ccph
   2. ctcph
   3. df-cph
   4. df-tcph
   5. iscph
   6. cphphl
   7. cphnlm
   8. cphngp
   9. cphlmod
   10. cphlvec
   11. cphnvc
   12. cphsubrglem
   13. cphreccllem
   14. cphsca
   15. cphsubrg
   16. cphreccl
   17. cphdivcl
   18. cphcjcl
   19. cphsqrtcl
   20. cphabscl
   21. cphsqrtcl2
   22. cphsqrtcl3
   23. cphqss
   24. cphclm
   25. cphnmvs
   26. cphipcl
   27. cphnmfval
   28. cphnm
   29. nmsq
   30. cphnmf
   31. cphnmcl
   32. reipcl
   33. ipge0
   34. cphipcj
   35. cphipipcj
   36. cphorthcom
   37. cphip0l
   38. cphip0r
   39. cphipeq0
   40. cphdir
   41. cphdi
   42. cph2di
   43. cphsubdir
   44. cphsubdi
   45. cph2subdi
   46. cphass
   47. cphassr
   48. cph2ass
   49. cphassi
   50. cphassir
   51. tcphex
   52. tcphval
   53. tcphbas
   54. tchplusg
   55. tcphsub
   56. tcphmulr
   57. tcphsca
   58. tcphvsca
   59. tcphip
   60. tcphtopn
   61. tcphphl
   62. tchnmfval
   63. tcphnmval
   64. cphtcphnm
   65. tcphds
   66. phclm
   67. tcphcphlem3
   68. ipcau2
   69. tcphcphlem1
   70. tcphcphlem2
   71. tcphcph
   72. ipcau
   73. nmparlem
   74. nmpar
   75. cphipval2
   76. 4cphipval2
   77. cphipval
   78. ipcnlem2
   79. ipcnlem1
   80. ipcn
   81. cnmpt1ip
   82. cnmpt2ip
   83. csscld
   84. clsocv
   85. cphsscph
5. Neighborhoods and closure
6. Convergence and completeness
   1. ccfil
   2. ccau
   3. ccmet
   4. df-cfil
   5. df-cau
   6. df-cmet
   7. lmmbr
   8. lmmbr2
   9. lmmbr3
   10. lmmcvg
   11. lmmbrf
   12. lmnn
   13. cfilfval
   14. iscfil
   15. iscfil2
   16. cfilfil
   17. cfili
   18. cfil3i
   19. cfilss
   20. fgcfil
   21. fmcfil
   22. iscfil3
   23. cfilfcls
   24. caufval
   25. iscau
   26. iscau2
   27. iscau3
   28. iscau4
   29. iscauf
   30. caun0
   31. caufpm
   32. caucfil
   33. iscmet
   34. cmetcvg
   35. cmetmet
   36. cmetmeti
   37. cmetcaulem
   38. cmetcau
   39. iscmet3lem3
   40. iscmet3lem1
   41. iscmet3lem2
   42. iscmet3
   43. iscmet2
   44. cfilresi
   45. cfilres
   46. caussi
   47. causs
   48. equivcfil
   49. equivcau
   50. lmle
   51. nglmle
   52. lmclim
   53. lmclimf
   54. metelcls
   55. metcld
   56. metcld2
   57. caubl
   58. caublcls
   59. metcnp4
   60. metcn4
   61. iscmet3i
   62. lmcau
   63. flimcfil
   64. metsscmetcld
   65. cmetss
   66. equivcmet
   67. relcmpcmet
   68. cmpcmet
   69. cfilucfil3
   70. cfilucfil4
   71. cncmet
   72. recmet
7. Baire's Category Theorem
   1. bcthlem1
   2. bcthlem2
   3. bcthlem3
   4. bcthlem4
   5. bcthlem5
   6. bcth
   7. bcth2
   8. bcth3
8. Banach spaces and subcomplex Hilbert spaces
   1. ccms
   2. cbn
   3. chl
   4. df-cms
   5. df-bn
   6. df-hl
   7. isbn
   8. bnsca
   9. bnnvc
   10. bnnlm
   11. bnngp
   12. bnlmod
   13. bncms
   14. iscms
   15. cmscmet
   16. bncmet
   17. cmsms
   18. cmspropd
   19. cmssmscld
   20. cmsss
   21. lssbn
   22. cmetcusp1
   23. cmetcusp
   24. cncms
   25. cnflduss
   26. cnfldcusp
   27. resscdrg
   28. cncdrg
   29. srabn
   30. rlmbn
   31. ishl
   32. hlbn
   33. hlcph
   34. hlphl
   35. hlcms
   36. hlprlem
   37. hlress
   38. hlpr
   39. ishl2
   40. cphssphl
   41. cmslssbn
   42. cmscsscms
   43. bncssbn
   44. cssbn
   45. csschl
   46. cmslsschl
   47. chlcsschl
   48. The complete ordered field of the real numbers
9. Euclidean spaces
   1. crrx
   2. cehl
   3. df-rrx
   4. df-ehl
   5. rrxval
   6. rrxbase
   7. rrxprds
   8. rrxip
   9. rrxnm
   10. rrxcph
   11. rrxds
   12. rrxvsca
   13. rrxplusgvscavalb
   14. rrxsca
   15. rrx0
   16. rrx0el
   17. csbren
   18. trirn
   19. rrxf
   20. rrxfsupp
   21. rrxsuppss
   22. rrxmvallem
   23. rrxmval
   24. rrxmfval
   25. rrxmetlem
   26. rrxmet
   27. rrxdstprj1
   28. rrxbasefi
   29. rrxdsfi
   30. rrxmetfi
   31. rrxdsfival
   32. ehlval
   33. ehlbase
   34. ehl0base
   35. ehl0
   36. ehleudis
   37. ehleudisval
   38. ehl1eudis
   39. ehl1eudisval
   40. ehl2eudis
   41. ehl2eudisval
10. Minimizing Vector Theorem
    1. minveclem1
    2. minveclem4c
    3. minveclem2
    4. minveclem3a
    5. minveclem3b
    6. minveclem3
    7. minveclem4a
    8. minveclem4b
    9. minveclem4
    10. minveclem5
    11. minveclem6
    12. minveclem7
    13. minvec
11. Projection Theorem
    1. pjthlem1
    2. pjthlem2
    3. pjth
    4. pjth2
    5. cldcss
    6. cldcss2
    7. hlhil