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

Axiom ax-hilex 21504
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 21424 . 2  class  ~H
2 cvv 2740 . 2  class  _V
31, 2wcel 1621 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21516  hilablo  21664  hhph  21682  hcau  21688  hlimadd  21697  hhcms  21707  issh  21712  shex  21716  hlim0  21740  hhssva  21761  hhsssm  21762  hhssnm  21763  hhshsslem1  21769  hhsscms  21781  ocval  21784  spanval  21837  hsupval  21838  sshjval  21854  sshjval3  21858  pjhfval  21900  hosmval  22092  hommval  22093  hodmval  22094  hfsmval  22095  hfmmval  22096  pjmfn  22237  pjmf1  22238  nmopval  22361  elcnop  22362  ellnop  22363  elunop  22377  elhmop  22378  hmopex  22380  nmfnval  22381  nlfnval  22386  elcnfn  22387  ellnfn  22388  dmadjss  22392  dmadjop  22393  adjeu  22394  adjval  22395  eigvecval  22401  eigvalfval  22402  specval  22403  hhcno  22409  hhcnf  22410  adjeq  22440  brafval  22448  kbfval  22457  adjbdln  22588  rnbra  22612  bra11  22613  leoprf2  22632  ishst  22719
  Copyright terms: Public domain W3C validator