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 28780
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 28700 . 2 class
2 cvv 3469 . 2 class V
31, 2wcel 2114 1 wff ℋ ∈ V
Colors of variables: wff setvar class
This axiom is referenced by:  hvmulex  28792  hilablo  28941  hhph  28959  hcau  28965  hlimadd  28974  hhcms  28984  issh  28989  shex  28993  hlim0  29016  hhssva  29038  hhsssm  29039  hhssnm  29040  hhshsslem1  29048  hhsscms  29059  ocval  29061  spanval  29114  hsupval  29115  sshjval  29131  sshjval3  29135  pjhfval  29177  pjmfn  29496  pjmf1  29497  hosmval  29516  hommval  29517  hodmval  29518  hfsmval  29519  hfmmval  29520  nmopval  29637  elcnop  29638  ellnop  29639  elunop  29653  elhmop  29654  hmopex  29656  nmfnval  29657  nlfnval  29662  elcnfn  29663  ellnfn  29664  dmadjss  29668  dmadjop  29669  adjeu  29670  adjval  29671  eigvecval  29677  eigvalfval  29678  specval  29679  hhcno  29685  hhcnf  29686  adjeq  29716  brafval  29724  kbfval  29733  adjbdln  29864  rnbra  29888  bra11  29889  leoprf2  29908  ishst  29995
  Copyright terms: Public domain W3C validator