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

Axiom ax-hilex 21579
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 21499 . 2  class  ~H
2 cvv 2788 . 2  class  _V
31, 2wcel 1684 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21591  hilablo  21739  hhph  21757  hcau  21763  hlimadd  21772  hhcms  21782  issh  21787  shex  21791  hlim0  21815  hhssva  21836  hhsssm  21837  hhssnm  21838  hhshsslem1  21844  hhsscms  21856  ocval  21859  spanval  21912  hsupval  21913  sshjval  21929  sshjval3  21933  pjhfval  21975  pjmfn  22294  pjmf1  22295  hosmval  22315  hommval  22316  hodmval  22317  hfsmval  22318  hfmmval  22319  nmopval  22436  elcnop  22437  ellnop  22438  elunop  22452  elhmop  22453  hmopex  22455  nmfnval  22456  nlfnval  22461  elcnfn  22462  ellnfn  22463  dmadjss  22467  dmadjop  22468  adjeu  22469  adjval  22470  eigvecval  22476  eigvalfval  22477  specval  22478  hhcno  22484  hhcnf  22485  adjeq  22515  brafval  22523  kbfval  22532  adjbdln  22663  rnbra  22687  bra11  22688  leoprf2  22707  ishst  22794
  Copyright terms: Public domain W3C validator