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 28195
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 chil 28115 . 2 class
2 cvv 3351 . 2 class V
31, 2wcel 2145 1 wff ℋ ∈ V
Colors of variables: wff setvar class
This axiom is referenced by:  hvmulex  28207  hilablo  28356  hhph  28374  hcau  28380  hlimadd  28389  hhcms  28399  issh  28404  shex  28408  hlim0  28431  hhssva  28453  hhsssm  28454  hhssnm  28455  hhshsslem1  28463  hhsscms  28475  ocval  28478  spanval  28531  hsupval  28532  sshjval  28548  sshjval3  28552  pjhfval  28594  pjmfn  28913  pjmf1  28914  hosmval  28933  hommval  28934  hodmval  28935  hfsmval  28936  hfmmval  28937  nmopval  29054  elcnop  29055  ellnop  29056  elunop  29070  elhmop  29071  hmopex  29073  nmfnval  29074  nlfnval  29079  elcnfn  29080  ellnfn  29081  dmadjss  29085  dmadjop  29086  adjeu  29087  adjval  29088  eigvecval  29094  eigvalfval  29095  specval  29096  hhcno  29102  hhcnf  29103  adjeq  29133  brafval  29141  kbfval  29150  adjbdln  29281  rnbra  29305  bra11  29306  leoprf2  29325  ishst  29412
  Copyright terms: Public domain W3C validator