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

Axiom ax-hilex 22455
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 22375 . 2  class  ~H
2 cvv 2916 . 2  class  _V
31, 2wcel 1721 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22467  hilablo  22615  hhph  22633  hcau  22639  hlimadd  22648  hhcms  22658  issh  22663  shex  22667  hlim0  22691  hhssva  22712  hhsssm  22713  hhssnm  22714  hhshsslem1  22720  hhsscms  22732  ocval  22735  spanval  22788  hsupval  22789  sshjval  22805  sshjval3  22809  pjhfval  22851  pjmfn  23170  pjmf1  23171  hosmval  23191  hommval  23192  hodmval  23193  hfsmval  23194  hfmmval  23195  nmopval  23312  elcnop  23313  ellnop  23314  elunop  23328  elhmop  23329  hmopex  23331  nmfnval  23332  nlfnval  23337  elcnfn  23338  ellnfn  23339  dmadjss  23343  dmadjop  23344  adjeu  23345  adjval  23346  eigvecval  23352  eigvalfval  23353  specval  23354  hhcno  23360  hhcnf  23361  adjeq  23391  brafval  23399  kbfval  23408  adjbdln  23539  rnbra  23563  bra11  23564  leoprf2  23583  ishst  23670
  Copyright terms: Public domain W3C validator