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 27032
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 26952 . 2 class
2 cvv 3077 . 2 class V
31, 2wcel 1938 1 wff ℋ ∈ V
Colors of variables: wff setvar class
This axiom is referenced by:  hvmulex  27044  hilablo  27193  hhph  27211  hcau  27217  hlimadd  27226  hhcms  27236  issh  27241  shex  27245  hlim0  27268  hhssva  27290  hhsssm  27291  hhssnm  27292  hhshsslem1  27300  hhsscms  27312  ocval  27315  spanval  27368  hsupval  27369  sshjval  27385  sshjval3  27389  pjhfval  27431  pjmfn  27750  pjmf1  27751  hosmval  27770  hommval  27771  hodmval  27772  hfsmval  27773  hfmmval  27774  nmopval  27891  elcnop  27892  ellnop  27893  elunop  27907  elhmop  27908  hmopex  27910  nmfnval  27911  nlfnval  27916  elcnfn  27917  ellnfn  27918  dmadjss  27922  dmadjop  27923  adjeu  27924  adjval  27925  eigvecval  27931  eigvalfval  27932  specval  27933  hhcno  27939  hhcnf  27940  adjeq  27970  brafval  27978  kbfval  27987  adjbdln  28118  rnbra  28142  bra11  28143  leoprf2  28162  ishst  28249
  Copyright terms: Public domain W3C validator