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

Axiom ax-hilex 21540
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 21460 . 2  class  ~H
2 cvv 2763 . 2  class  _V
31, 2wcel 1621 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21552  hilablo  21700  hhph  21718  hcau  21724  hlimadd  21733  hhcms  21743  issh  21748  shex  21752  hlim0  21776  hhssva  21797  hhsssm  21798  hhssnm  21799  hhshsslem1  21805  hhsscms  21817  ocval  21820  spanval  21873  hsupval  21874  sshjval  21890  sshjval3  21894  pjhfval  21936  pjmfn  22255  pjmf1  22256  hosmval  22276  hommval  22277  hodmval  22278  hfsmval  22279  hfmmval  22280  nmopval  22397  elcnop  22398  ellnop  22399  elunop  22413  elhmop  22414  hmopex  22416  nmfnval  22417  nlfnval  22422  elcnfn  22423  ellnfn  22424  dmadjss  22428  dmadjop  22429  adjeu  22430  adjval  22431  eigvecval  22437  eigvalfval  22438  specval  22439  hhcno  22445  hhcnf  22446  adjeq  22476  brafval  22484  kbfval  22493  adjbdln  22624  rnbra  22648  bra11  22649  leoprf2  22668  ishst  22755
  Copyright terms: Public domain W3C validator