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

Axiom ax-hilex 22490
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 22410 . 2  class  ~H
2 cvv 2948 . 2  class  _V
31, 2wcel 1725 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22502  hilablo  22650  hhph  22668  hcau  22674  hlimadd  22683  hhcms  22693  issh  22698  shex  22702  hlim0  22726  hhssva  22747  hhsssm  22748  hhssnm  22749  hhshsslem1  22755  hhsscms  22767  ocval  22770  spanval  22823  hsupval  22824  sshjval  22840  sshjval3  22844  pjhfval  22886  pjmfn  23205  pjmf1  23206  hosmval  23226  hommval  23227  hodmval  23228  hfsmval  23229  hfmmval  23230  nmopval  23347  elcnop  23348  ellnop  23349  elunop  23363  elhmop  23364  hmopex  23366  nmfnval  23367  nlfnval  23372  elcnfn  23373  ellnfn  23374  dmadjss  23378  dmadjop  23379  adjeu  23380  adjval  23381  eigvecval  23387  eigvalfval  23388  specval  23389  hhcno  23395  hhcnf  23396  adjeq  23426  brafval  23434  kbfval  23443  adjbdln  23574  rnbra  23598  bra11  23599  leoprf2  23618  ishst  23705
  Copyright terms: Public domain W3C validator