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

Axiom ax-hilex 21581
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 21501 . 2  class  ~H
2 cvv 2790 . 2  class  _V
31, 2wcel 1686 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21593  hilablo  21741  hhph  21759  hcau  21765  hlimadd  21774  hhcms  21784  issh  21789  shex  21793  hlim0  21817  hhssva  21838  hhsssm  21839  hhssnm  21840  hhshsslem1  21846  hhsscms  21858  ocval  21861  spanval  21914  hsupval  21915  sshjval  21931  sshjval3  21935  pjhfval  21977  pjmfn  22296  pjmf1  22297  hosmval  22317  hommval  22318  hodmval  22319  hfsmval  22320  hfmmval  22321  nmopval  22438  elcnop  22439  ellnop  22440  elunop  22454  elhmop  22455  hmopex  22457  nmfnval  22458  nlfnval  22463  elcnfn  22464  ellnfn  22465  dmadjss  22469  dmadjop  22470  adjeu  22471  adjval  22472  eigvecval  22478  eigvalfval  22479  specval  22480  hhcno  22486  hhcnf  22487  adjeq  22517  brafval  22525  kbfval  22534  adjbdln  22665  rnbra  22689  bra11  22690  leoprf2  22709  ishst  22796
  Copyright terms: Public domain W3C validator