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

Axiom ax-hilex 22504
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 22424 . 2  class  ~H
2 cvv 2958 . 2  class  _V
31, 2wcel 1726 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22516  hilablo  22664  hhph  22682  hcau  22688  hlimadd  22697  hhcms  22707  issh  22712  shex  22716  hlim0  22740  hhssva  22761  hhsssm  22762  hhssnm  22763  hhshsslem1  22769  hhsscms  22781  ocval  22784  spanval  22837  hsupval  22838  sshjval  22854  sshjval3  22858  pjhfval  22900  pjmfn  23219  pjmf1  23220  hosmval  23240  hommval  23241  hodmval  23242  hfsmval  23243  hfmmval  23244  nmopval  23361  elcnop  23362  ellnop  23363  elunop  23377  elhmop  23378  hmopex  23380  nmfnval  23381  nlfnval  23386  elcnfn  23387  ellnfn  23388  dmadjss  23392  dmadjop  23393  adjeu  23394  adjval  23395  eigvecval  23401  eigvalfval  23402  specval  23403  hhcno  23409  hhcnf  23410  adjeq  23440  brafval  23448  kbfval  23457  adjbdln  23588  rnbra  23612  bra11  23613  leoprf2  23632  ishst  23719
  Copyright terms: Public domain W3C validator