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

Axiom ax-hilex 28704
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, , which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hilex ℋ ∈ V

Detailed syntax breakdown of Axiom ax-hilex
StepHypRef Expression
1 chba 28624 . 2 class
2 cvv 3495 . 2 class V
31, 2wcel 2105 1 wff ℋ ∈ V
Colors of variables: wff setvar class
This axiom is referenced by:  hvmulex  28716  hilablo  28865  hhph  28883  hcau  28889  hlimadd  28898  hhcms  28908  issh  28913  shex  28917  hlim0  28940  hhssva  28962  hhsssm  28963  hhssnm  28964  hhshsslem1  28972  hhsscms  28983  ocval  28985  spanval  29038  hsupval  29039  sshjval  29055  sshjval3  29059  pjhfval  29101  pjmfn  29420  pjmf1  29421  hosmval  29440  hommval  29441  hodmval  29442  hfsmval  29443  hfmmval  29444  nmopval  29561  elcnop  29562  ellnop  29563  elunop  29577  elhmop  29578  hmopex  29580  nmfnval  29581  nlfnval  29586  elcnfn  29587  ellnfn  29588  dmadjss  29592  dmadjop  29593  adjeu  29594  adjval  29595  eigvecval  29601  eigvalfval  29602  specval  29603  hhcno  29609  hhcnf  29610  adjeq  29640  brafval  29648  kbfval  29657  adjbdln  29788  rnbra  29812  bra11  29813  leoprf2  29832  ishst  29919
  Copyright terms: Public domain W3C validator