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

Axiom ax-hilex 21595
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 21515 . 2  class  ~H
2 cvv 2801 . 2  class  _V
31, 2wcel 1696 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21607  hilablo  21755  hhph  21773  hcau  21779  hlimadd  21788  hhcms  21798  issh  21803  shex  21807  hlim0  21831  hhssva  21852  hhsssm  21853  hhssnm  21854  hhshsslem1  21860  hhsscms  21872  ocval  21875  spanval  21928  hsupval  21929  sshjval  21945  sshjval3  21949  pjhfval  21991  pjmfn  22310  pjmf1  22311  hosmval  22331  hommval  22332  hodmval  22333  hfsmval  22334  hfmmval  22335  nmopval  22452  elcnop  22453  ellnop  22454  elunop  22468  elhmop  22469  hmopex  22471  nmfnval  22472  nlfnval  22477  elcnfn  22478  ellnfn  22479  dmadjss  22483  dmadjop  22484  adjeu  22485  adjval  22486  eigvecval  22492  eigvalfval  22493  specval  22494  hhcno  22500  hhcnf  22501  adjeq  22531  brafval  22539  kbfval  22548  adjbdln  22679  rnbra  22703  bra11  22704  leoprf2  22723  ishst  22810
  Copyright terms: Public domain W3C validator