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 27840
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 27760 . 2 class
2 cvv 3198 . 2 class V
31, 2wcel 1989 1 wff ℋ ∈ V
Colors of variables: wff setvar class
This axiom is referenced by:  hvmulex  27852  hilablo  28001  hhph  28019  hcau  28025  hlimadd  28034  hhcms  28044  issh  28049  shex  28053  hlim0  28076  hhssva  28098  hhsssm  28099  hhssnm  28100  hhshsslem1  28108  hhsscms  28120  ocval  28123  spanval  28176  hsupval  28177  sshjval  28193  sshjval3  28197  pjhfval  28239  pjmfn  28558  pjmf1  28559  hosmval  28578  hommval  28579  hodmval  28580  hfsmval  28581  hfmmval  28582  nmopval  28699  elcnop  28700  ellnop  28701  elunop  28715  elhmop  28716  hmopex  28718  nmfnval  28719  nlfnval  28724  elcnfn  28725  ellnfn  28726  dmadjss  28730  dmadjop  28731  adjeu  28732  adjval  28733  eigvecval  28739  eigvalfval  28740  specval  28741  hhcno  28747  hhcnf  28748  adjeq  28778  brafval  28786  kbfval  28795  adjbdln  28926  rnbra  28950  bra11  28951  leoprf2  28970  ishst  29057
  Copyright terms: Public domain W3C validator