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

Axiom ax-hilex 21575
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 21495 . 2  class  ~H
2 cvv 2789 . 2  class  _V
31, 2wcel 1685 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21587  hilablo  21735  hhph  21753  hcau  21759  hlimadd  21768  hhcms  21778  issh  21783  shex  21787  hlim0  21811  hhssva  21832  hhsssm  21833  hhssnm  21834  hhshsslem1  21840  hhsscms  21852  ocval  21855  spanval  21908  hsupval  21909  sshjval  21925  sshjval3  21929  pjhfval  21971  pjmfn  22290  pjmf1  22291  hosmval  22311  hommval  22312  hodmval  22313  hfsmval  22314  hfmmval  22315  nmopval  22432  elcnop  22433  ellnop  22434  elunop  22448  elhmop  22449  hmopex  22451  nmfnval  22452  nlfnval  22457  elcnfn  22458  ellnfn  22459  dmadjss  22463  dmadjop  22464  adjeu  22465  adjval  22466  eigvecval  22472  eigvalfval  22473  specval  22474  hhcno  22480  hhcnf  22481  adjeq  22511  brafval  22519  kbfval  22528  adjbdln  22659  rnbra  22683  bra11  22684  leoprf2  22703  ishst  22790
  Copyright terms: Public domain W3C validator