Metamath Proof Explorer

Table of Contents - 19.6. Operators on Hilbert spaces

1. Operator sum, difference, and scalar multiplication
   1. df-hosum
   2. df-homul
   3. df-hodif
   4. df-hfsum
   5. df-hfmul
   6. hosmval
   7. hommval
   8. hodmval
   9. hfsmval
   10. hfmmval
   11. hosval
   12. homval
   13. hodval
   14. hfsval
   15. hfmval
   16. hoscl
   17. homcl
   18. hodcl
2. Zero and identity operators
   1. df-h0op
   2. df-iop
   3. ho0val
   4. ho0f
   5. df0op2
   6. dfiop2
   7. hoif
   8. hoival
   9. hoico1
   10. hoico2
3. Operations on Hilbert space operators
   1. hoaddcl
   2. homulcl
   3. hoeq
   4. hoeqi
   5. hoscli
   6. hodcli
   7. hocoi
   8. hococli
   9. hocofi
   10. hocofni
   11. hoaddcli
   12. hosubcli
   13. hoaddfni
   14. hosubfni
   15. hoaddcomi
   16. hosubcl
   17. hoaddcom
   18. hodsi
   19. hoaddassi
   20. hoadd12i
   21. hoadd32i
   22. hocadddiri
   23. hocsubdiri
   24. ho2coi
   25. hoaddass
   26. hoadd32
   27. hoadd4
   28. hocsubdir
   29. hoaddid1i
   30. hodidi
   31. ho0coi
   32. hoid1i
   33. hoid1ri
   34. hoaddid1
   35. hodid
   36. hon0
   37. hodseqi
   38. ho0subi
   39. honegsubi
   40. ho0sub
   41. hosubid1
   42. honegsub
   43. homulid2
   44. homco1
   45. homulass
   46. hoadddi
   47. hoadddir
   48. homul12
   49. honegneg
   50. hosubneg
   51. hosubdi
   52. honegdi
   53. honegsubdi
   54. honegsubdi2
   55. hosubsub2
   56. hosub4
   57. hosubadd4
   58. hoaddsubass
   59. hoaddsub
   60. hosubsub
   61. hosubsub4
   62. ho2times
   63. hoaddsubassi
   64. hoaddsubi
   65. hosd1i
   66. hosd2i
   67. hopncani
   68. honpcani
   69. hosubeq0i
   70. honpncani
   71. ho01i
   72. ho02i
   73. hoeq1
   74. hoeq2
   75. adjmo
   76. adjsym
   77. eigrei
   78. eigre
   79. eigposi
   80. eigorthi
   81. eigorth
4. Linear, continuous, bounded, Hermitian, unitary operators and norms
   1. df-nmop
   2. df-cnop
   3. df-lnop
   4. df-bdop
   5. df-unop
   6. df-hmop
5. Theorems about operators and functionals
   1. nmopval
   2. elcnop
   3. ellnop
   4. lnopf
   5. elbdop
   6. bdopln
   7. bdopf
   8. nmopsetretALT
   9. nmopsetretHIL
   10. nmopsetn0
   11. nmopxr
   12. nmoprepnf
   13. nmopgtmnf
   14. nmopreltpnf
   15. nmopre
   16. elbdop2
   17. elunop
   18. elhmop
   19. hmopf
   20. hmopex
   21. nmfnval
   22. nmfnsetre
   23. nmfnsetn0
   24. nmfnxr
   25. nmfnrepnf
   26. nlfnval
   27. elcnfn
   28. ellnfn
   29. lnfnf
   30. dfadj2
   31. funadj
   32. dmadjss
   33. dmadjop
   34. adjeu
   35. adjval
   36. adjval2
   37. cnvadj
   38. funcnvadj
   39. adj1o
   40. dmadjrn
   41. eigvecval
   42. eigvalfval
   43. specval
   44. speccl
   45. hhlnoi
   46. hhnmoi
   47. hhbloi
   48. hh0oi
   49. hhcno
   50. hhcnf
   51. dmadjrnb
   52. nmoplb
   53. nmopub
   54. nmopub2tALT
   55. nmopub2tHIL
   56. nmopge0
   57. nmopgt0
   58. cnopc
   59. lnopl
   60. unop
   61. unopf1o
   62. unopnorm
   63. cnvunop
   64. unopadj
   65. unoplin
   66. counop
   67. hmop
   68. hmopre
   69. nmfnlb
   70. nmfnleub
   71. nmfnleub2
   72. nmfnge0
   73. elnlfn
   74. elnlfn2
   75. cnfnc
   76. lnfnl
   77. adjcl
   78. adj1
   79. adj2
   80. adjeq
   81. adjadj
   82. adjvalval
   83. unopadj2
   84. hmopadj
   85. hmdmadj
   86. hmopadj2
   87. hmoplin
   88. brafval
   89. braval
   90. braadd
   91. bramul
   92. brafn
   93. bralnfn
   94. bracl
   95. bra0
   96. brafnmul
   97. kbfval
   98. kbop
   99. kbval
   100. kbmul
   101. kbpj
   102. eleigvec
   103. eleigvec2
   104. eleigveccl
   105. eigvalval
   106. eigvalcl
   107. eigvec1
   108. eighmre
   109. eighmorth
   110. nmopnegi
   111. lnop0
   112. lnopmul
   113. lnopli
   114. lnopfi
   115. lnop0i
   116. lnopaddi
   117. lnopmuli
   118. lnopaddmuli
   119. lnopsubi
   120. lnopsubmuli
   121. lnopmulsubi
   122. homco2
   123. idunop
   124. 0cnop
   125. 0cnfn
   126. idcnop
   127. idhmop
   128. 0hmop
   129. 0lnop
   130. 0lnfn
   131. nmop0
   132. nmfn0
   133. hmopbdoptHIL
   134. hoddii
   135. hoddi
   136. nmop0h
   137. idlnop
   138. 0bdop
   139. adj0
   140. nmlnop0iALT
   141. nmlnop0iHIL
   142. nmlnopgt0i
   143. nmlnop0
   144. nmlnopne0
   145. lnopmi
   146. lnophsi
   147. lnophdi
   148. lnopcoi
   149. lnopco0i
   150. lnopeq0lem1
   151. lnopeq0lem2
   152. lnopeq0i
   153. lnopeqi
   154. lnopeq
   155. lnopunilem1
   156. lnopunilem2
   157. lnopunii
   158. elunop2
   159. nmopun
   160. unopbd
   161. lnophmlem1
   162. lnophmlem2
   163. lnophmi
   164. lnophm
   165. hmops
   166. hmopm
   167. hmopd
   168. hmopco
   169. nmbdoplbi
   170. nmbdoplb
   171. nmcexi
   172. nmcopexi
   173. nmcoplbi
   174. nmcopex
   175. nmcoplb
   176. nmophmi
   177. bdophmi
   178. lnconi
   179. lnopconi
   180. lnopcon
   181. lnopcnbd
   182. lncnopbd
   183. lncnbd
   184. lnopcnre
   185. lnfnli
   186. lnfnfi
   187. lnfn0i
   188. lnfnaddi
   189. lnfnmuli
   190. lnfnaddmuli
   191. lnfnsubi
   192. lnfn0
   193. lnfnmul
   194. nmbdfnlbi
   195. nmbdfnlb
   196. nmcfnexi
   197. nmcfnlbi
   198. nmcfnex
   199. nmcfnlb
   200. lnfnconi
   201. lnfncon
   202. lnfncnbd
   203. imaelshi
   204. rnelshi
   205. nlelshi
   206. nlelchi
6. Adjoints (cont.)
   1. cnlnadjlem1
   2. cnlnadjlem2
   3. cnlnadjlem3
   4. cnlnadjlem4
   5. cnlnadjlem5
   6. cnlnadjlem6
   7. cnlnadjlem7
   8. cnlnadjlem8
   9. cnlnadjlem9
   10. cnlnadji
   11. cnlnadjeui
   12. cnlnadjeu
   13. cnlnadj
   14. cnlnssadj
   15. bdopssadj
   16. bdopadj
   17. adjbdln
   18. adjbdlnb
   19. adjbd1o
   20. adjlnop
   21. adjsslnop
   22. nmopadjlei
   23. nmopadjlem
   24. nmopadji
   25. adjeq0
   26. adjmul
   27. adjadd
   28. nmoptrii
   29. nmopcoi
   30. bdophsi
   31. bdophdi
   32. bdopcoi
   33. nmoptri2i
   34. adjcoi
   35. nmopcoadji
   36. nmopcoadj2i
   37. nmopcoadj0i
7. Quantum computation error bound theorem
   1. unierri
8. Dirac bra-ket notation (cont.)
   1. branmfn
   2. brabn
   3. rnbra
   4. bra11
   5. bracnln
   6. cnvbraval
   7. cnvbracl
   8. cnvbrabra
   9. bracnvbra
   10. bracnlnval
   11. cnvbramul
   12. kbass1
   13. kbass2
   14. kbass3
   15. kbass4
   16. kbass5
   17. kbass6
9. Projectors as operators
   1. pjhmopi
   2. pjlnopi
   3. pjnmopi
   4. pjbdlni
   5. pjhmop
   6. hmopidmchi
   7. hmopidmpji
   8. hmopidmch
   9. hmopidmpj
   10. pjsdii
   11. pjddii
   12. pjsdi2i
   13. pjcoi
   14. pjcocli
   15. pjcohcli
   16. pjadjcoi
   17. pjcofni
   18. pjss1coi
   19. pjss2coi
   20. pjssmi
   21. pjssge0i
   22. pjdifnormi
   23. pjnormssi
   24. pjorthcoi
   25. pjscji
   26. pjssumi
   27. pjssposi
   28. pjordi
   29. pjssdif2i
   30. pjssdif1i
   31. pjimai
   32. pjidmcoi
   33. pjoccoi
   34. pjtoi
   35. pjoci
   36. pjidmco
   37. dfpjop
   38. pjhmopidm
   39. elpjidm
   40. elpjhmop
   41. 0leopj
   42. pjadj2
   43. pjadj3
   44. elpjch
   45. elpjrn
   46. pjinvari
   47. pjin1i
   48. pjin2i
   49. pjin3i
   50. pjclem1
   51. pjclem2
   52. pjclem3
   53. pjclem4a
   54. pjclem4
   55. pjci
   56. pjcmul1i
   57. pjcmul2i
   58. pjcohocli
   59. pjadj2coi
   60. pj2cocli
   61. pj3lem1
   62. pj3si
   63. pj3i
   64. pj3cor1i
   65. pjs14i