Metamath Proof Explorer

Table of Contents - 19.5. Properties of Hilbert subspaces

1. Orthomodular law
   1. omlsilem
   2. omlsii
   3. omlsi
   4. ococi
   5. ococ
   6. dfch2
   7. ococin
   8. hsupval2
   9. chsupval2
   10. sshjval2
   11. chsupid
   12. chsupsn
   13. shlub
   14. shlubi
2. Projectors (cont.)
   1. pjhtheu2
   2. pjcli
   3. pjhcli
   4. pjpjpre
   5. axpjpj
   6. pjclii
   7. pjhclii
   8. pjpj0i
   9. pjpji
   10. pjpjhth
   11. pjpjhthi
   12. pjop
   13. pjpo
   14. pjopi
   15. pjpoi
   16. pjoc1i
   17. pjchi
   18. pjoccl
   19. pjoc1
   20. pjomli
   21. pjoml
   22. pjococi
   23. pjoc2i
   24. pjoc2
3. Hilbert lattice operations
   1. sh0le
   2. ch0le
   3. shle0
   4. chle0
   5. chnlen0
   6. ch0pss
   7. orthin
   8. ssjo
   9. shne0i
   10. shs0i
   11. shs00i
   12. ch0lei
   13. chle0i
   14. chne0i
   15. chocini
   16. chj0i
   17. chm1i
   18. chjcli
   19. chsleji
   20. chseli
   21. chincli
   22. chsscon3i
   23. chsscon1i
   24. chsscon2i
   25. chcon2i
   26. chcon1i
   27. chcon3i
   28. chunssji
   29. chjcomi
   30. chub1i
   31. chub2i
   32. chlubi
   33. chlubii
   34. chlej1i
   35. chlej2i
   36. chlej12i
   37. chlejb1i
   38. chdmm1i
   39. chdmm2i
   40. chdmm3i
   41. chdmm4i
   42. chdmj1i
   43. chdmj2i
   44. chdmj3i
   45. chdmj4i
   46. chnlei
   47. chjassi
   48. chj00i
   49. chjoi
   50. chj1i
   51. chm0i
   52. chm0
   53. shjshsi
   54. shjshseli
   55. chne0
   56. chocin
   57. chssoc
   58. chj0
   59. chslej
   60. chincl
   61. chsscon3
   62. chsscon1
   63. chsscon2
   64. chpsscon3
   65. chpsscon1
   66. chpsscon2
   67. chjcom
   68. chub1
   69. chub2
   70. chlub
   71. chlej1
   72. chlej2
   73. chlejb1
   74. chlejb2
   75. chnle
   76. chjo
   77. chabs1
   78. chabs2
   79. chabs1i
   80. chabs2i
   81. chjidm
   82. chjidmi
   83. chj12i
   84. chj4i
   85. chjjdiri
   86. chdmm1
   87. chdmm2
   88. chdmm3
   89. chdmm4
   90. chdmj1
   91. chdmj2
   92. chdmj3
   93. chdmj4
   94. chjass
   95. chj12
   96. chj4
   97. ledii
   98. lediri
   99. lejdii
   100. lejdiri
   101. ledi
4. Span (cont.) and one-dimensional subspaces
   1. spansn0
   2. span0
   3. elspani
   4. spanuni
   5. spanun
   6. sshhococi
   7. hne0
   8. chsup0
   9. h1deoi
   10. h1dei
   11. h1did
   12. h1dn0
   13. h1de2i
   14. h1de2bi
   15. h1de2ctlem
   16. h1de2ci
   17. spansni
   18. elspansni
   19. spansn
   20. spansnch
   21. spansnsh
   22. spansnchi
   23. spansnid
   24. spansnmul
   25. elspansncl
   26. elspansn
   27. elspansn2
   28. spansncol
   29. spansneleqi
   30. spansneleq
   31. spansnss
   32. elspansn3
   33. elspansn4
   34. elspansn5
   35. spansnss2
   36. normcan
   37. pjspansn
   38. spansnpji
   39. spanunsni
   40. spanpr
   41. h1datomi
   42. h1datom
5. Commutes relation for Hilbert lattice elements
   1. df-cm
   2. cmbr
   3. pjoml2i
   4. pjoml3i
   5. pjoml4i
   6. pjoml5i
   7. pjoml6i
   8. cmbri
   9. cmcmlem
   10. cmcmi
   11. cmcm2i
   12. cmcm3i
   13. cmcm4i
   14. cmbr2i
   15. cmcmii
   16. cmcm2ii
   17. cmcm3ii
   18. cmbr3i
   19. cmbr4i
   20. lecmi
   21. lecmii
   22. cmj1i
   23. cmj2i
   24. cmm1i
   25. cmm2i
   26. cmbr3
   27. cm0
   28. cmidi
   29. pjoml2
   30. pjoml3
   31. pjoml5
   32. cmcm
   33. cmcm3
   34. cmcm2
   35. lecm
6. Foulis-Holland theorem
   1. fh1
   2. fh2
   3. cm2j
   4. fh1i
   5. fh2i
   6. fh3i
   7. fh4i
   8. cm2ji
   9. cm2mi
7. Quantum Logic Explorer axioms
   1. qlax1i
   2. qlax2i
   3. qlax3i
   4. qlax4i
   5. qlax5i
   6. qlaxr1i
   7. qlaxr2i
   8. qlaxr4i
   9. qlaxr5i
   10. qlaxr3i
8. Orthogonal subspaces
   1. chscllem1
   2. chscllem2
   3. chscllem3
   4. chscllem4
   5. chscl
   6. osumi
   7. osumcori
   8. osumcor2i
   9. osum
   10. spansnji
   11. spansnj
   12. spansnscl
   13. sumspansn
   14. spansnm0i
   15. nonbooli
   16. spansncvi
   17. spansncv
9. Orthoarguesian laws 5OA and 3OA
   1. 5oalem1
   2. 5oalem2
   3. 5oalem3
   4. 5oalem4
   5. 5oalem5
   6. 5oalem6
   7. 5oalem7
   8. 5oai
   9. 3oalem1
   10. 3oalem2
   11. 3oalem3
   12. 3oalem4
   13. 3oalem5
   14. 3oalem6
   15. 3oai
10. Projectors (cont.)
    1. pjorthi
    2. pjch1
    3. pjo
    4. pjcompi
    5. pjidmi
    6. pjadjii
    7. pjaddii
    8. pjinormii
    9. pjmulii
    10. pjsubii
    11. pjsslem
    12. pjss2i
    13. pjssmii
    14. pjssge0ii
    15. pjdifnormii
    16. pjcji
    17. pjadji
    18. pjaddi
    19. pjinormi
    20. pjsubi
    21. pjmuli
    22. pjige0i
    23. pjige0
    24. pjcjt2
    25. pj0i
    26. pjch
    27. pjid
    28. pjvec
    29. pjocvec
    30. pjocini
    31. pjini
    32. pjjsi
    33. pjfni
    34. pjrni
    35. pjfoi
    36. pjfi
    37. pjvi
    38. pjhfo
    39. pjrn
    40. pjhf
    41. pjfn
    42. pjsumi
    43. pj11i
    44. pjdsi
    45. pjds3i
    46. pj11
    47. pjmfn
    48. pjmf1
    49. pjoi0
    50. pjoi0i
    51. pjopythi
    52. pjopyth
    53. pjnormi
    54. pjpythi
    55. pjneli
    56. pjnorm
    57. pjpyth
    58. pjnel
    59. pjnorm2
11. Mayet's equation E_3
    1. mayete3i
    2. mayetes3i