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

Axiom ax-hilex 22343
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 22263 . 2  class  ~H
2 cvv 2892 . 2  class  _V
31, 2wcel 1717 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22355  hilablo  22503  hhph  22521  hcau  22527  hlimadd  22536  hhcms  22546  issh  22551  shex  22555  hlim0  22579  hhssva  22600  hhsssm  22601  hhssnm  22602  hhshsslem1  22608  hhsscms  22620  ocval  22623  spanval  22676  hsupval  22677  sshjval  22693  sshjval3  22697  pjhfval  22739  pjmfn  23058  pjmf1  23059  hosmval  23079  hommval  23080  hodmval  23081  hfsmval  23082  hfmmval  23083  nmopval  23200  elcnop  23201  ellnop  23202  elunop  23216  elhmop  23217  hmopex  23219  nmfnval  23220  nlfnval  23225  elcnfn  23226  ellnfn  23227  dmadjss  23231  dmadjop  23232  adjeu  23233  adjval  23234  eigvecval  23240  eigvalfval  23241  specval  23242  hhcno  23248  hhcnf  23249  adjeq  23279  brafval  23287  kbfval  23296  adjbdln  23427  rnbra  23451  bra11  23452  leoprf2  23471  ishst  23558
  Copyright terms: Public domain W3C validator