Metamath Proof Explorer

Table of Contents - 19.1. Axiomatization of complex pre-Hilbert spaces

1. Basic Hilbert space definitions
   1. chba
   2. cva
   3. csm
   4. csp
   5. cno
   6. c0v
   7. cmv
   8. ccauold
   9. chli
   10. csh
   11. cch
   12. cort
   13. cph
   14. cspn
   15. chj
   16. chsup
   17. c0h
   18. ccm
   19. cpjh
   20. chos
   21. chot
   22. chod
   23. chfs
   24. chft
   25. ch0o
   26. chio
   27. cnop
   28. ccop
   29. clo
   30. cbo
   31. cuo
   32. cho
   33. cnmf
   34. cnl
   35. ccnfn
   36. clf
   37. cado
   38. cbr
   39. ck
   40. cleo
   41. cei
   42. cel
   43. cspc
   44. cst
   45. chst
   46. ccv
   47. cat
   48. cmd
   49. cdmd
2. Preliminary ZFC lemmas
   1. df-hnorm
   2. df-hba
   3. df-h0v
   4. df-hvsub
   5. df-hlim
   6. df-hcau
   7. h2hva
   8. h2hsm
   9. h2hnm
   10. h2hvs
   11. h2hmetdval
   12. h2hcau
   13. h2hlm
3. Derive the Hilbert space axioms from ZFC set theory
   1. axhilex-zf
   2. axhfvadd-zf
   3. axhvcom-zf
   4. axhvass-zf
   5. axhv0cl-zf
   6. axhvaddid-zf
   7. axhfvmul-zf
   8. axhvmulid-zf
   9. axhvmulass-zf
   10. axhvdistr1-zf
   11. axhvdistr2-zf
   12. axhvmul0-zf
   13. axhfi-zf
   14. axhis1-zf
   15. axhis2-zf
   16. axhis3-zf
   17. axhis4-zf
   18. axhcompl-zf
4. Introduce the vector space axioms for a Hilbert space
   1. ax-hilex
   2. ax-hfvadd
   3. ax-hvcom
   4. ax-hvass
   5. ax-hv0cl
   6. ax-hvaddid
   7. ax-hfvmul
   8. ax-hvmulid
   9. ax-hvmulass
   10. ax-hvdistr1
   11. ax-hvdistr2
   12. ax-hvmul0
5. Vector operations
   1. hvmulex
   2. hvaddcl
   3. hvmulcl
   4. hvmulcli
   5. hvsubf
   6. hvsubval
   7. hvsubcl
   8. hvaddcli
   9. hvcomi
   10. hvsubvali
   11. hvsubcli
   12. ifhvhv0
   13. hvaddid2
   14. hvmul0
   15. hvmul0or
   16. hvsubid
   17. hvnegid
   18. hv2neg
   19. hvaddid2i
   20. hvnegidi
   21. hv2negi
   22. hvm1neg
   23. hvaddsubval
   24. hvadd32
   25. hvadd12
   26. hvadd4
   27. hvsub4
   28. hvaddsub12
   29. hvpncan
   30. hvpncan2
   31. hvaddsubass
   32. hvpncan3
   33. hvmulcom
   34. hvsubass
   35. hvsub32
   36. hvmulassi
   37. hvmulcomi
   38. hvmul2negi
   39. hvsubdistr1
   40. hvsubdistr2
   41. hvdistr1i
   42. hvsubdistr1i
   43. hvassi
   44. hvadd32i
   45. hvsubassi
   46. hvsub32i
   47. hvadd12i
   48. hvadd4i
   49. hvsubsub4i
   50. hvsubsub4
   51. hv2times
   52. hvnegdii
   53. hvsubeq0i
   54. hvsubcan2i
   55. hvaddcani
   56. hvsubaddi
   57. hvnegdi
   58. hvsubeq0
   59. hvaddeq0
   60. hvaddcan
   61. hvaddcan2
   62. hvmulcan
   63. hvmulcan2
   64. hvsubcan
   65. hvsubcan2
   66. hvsub0
   67. hvsubadd
   68. hvaddsub4
6. Inner product postulates for a Hilbert space
   1. ax-hfi
   2. hicl
   3. hicli
   4. ax-his1
   5. ax-his2
   6. ax-his3
   7. ax-his4