HSE Home Hilbert Space Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  HSE Home  >  Th. List  >  ax-hilex Unicode version

Axiom ax-hilex 22013
Description: This is our first axiom for a complex Hilbert space, which is the foundation for quantum mechanics and quantum field theory. We assume that there exists a primitive class,  ~H, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hilex  |-  ~H  e.  _V

Detailed syntax breakdown of Axiom ax-hilex
StepHypRef Expression
1 chil 21933 . 2  class  ~H
2 cvv 2873 . 2  class  _V
31, 2wcel 1715 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22025  hilablo  22173  hhph  22191  hcau  22197  hlimadd  22206  hhcms  22216  issh  22221  shex  22225  hlim0  22249  hhssva  22270  hhsssm  22271  hhssnm  22272  hhshsslem1  22278  hhsscms  22290  ocval  22293  spanval  22346  hsupval  22347  sshjval  22363  sshjval3  22367  pjhfval  22409  pjmfn  22728  pjmf1  22729  hosmval  22749  hommval  22750  hodmval  22751  hfsmval  22752  hfmmval  22753  nmopval  22870  elcnop  22871  ellnop  22872  elunop  22886  elhmop  22887  hmopex  22889  nmfnval  22890  nlfnval  22895  elcnfn  22896  ellnfn  22897  dmadjss  22901  dmadjop  22902  adjeu  22903  adjval  22904  eigvecval  22910  eigvalfval  22911  specval  22912  hhcno  22918  hhcnf  22919  adjeq  22949  brafval  22957  kbfval  22966  adjbdln  23097  rnbra  23121  bra11  23122  leoprf2  23141  ishst  23228
  Copyright terms: Public domain W3C validator