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

Axiom ax-hilex 22459
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 22379 . 2  class  ~H
2 cvv 2920 . 2  class  _V
31, 2wcel 1721 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22471  hilablo  22619  hhph  22637  hcau  22643  hlimadd  22652  hhcms  22662  issh  22667  shex  22671  hlim0  22695  hhssva  22716  hhsssm  22717  hhssnm  22718  hhshsslem1  22724  hhsscms  22736  ocval  22739  spanval  22792  hsupval  22793  sshjval  22809  sshjval3  22813  pjhfval  22855  pjmfn  23174  pjmf1  23175  hosmval  23195  hommval  23196  hodmval  23197  hfsmval  23198  hfmmval  23199  nmopval  23316  elcnop  23317  ellnop  23318  elunop  23332  elhmop  23333  hmopex  23335  nmfnval  23336  nlfnval  23341  elcnfn  23342  ellnfn  23343  dmadjss  23347  dmadjop  23348  adjeu  23349  adjval  23350  eigvecval  23356  eigvalfval  23357  specval  23358  hhcno  23364  hhcnf  23365  adjeq  23395  brafval  23403  kbfval  23412  adjbdln  23543  rnbra  23567  bra11  23568  leoprf2  23587  ishst  23674
  Copyright terms: Public domain W3C validator