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

Axiom ax-hilex 22507
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,  ~H, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)
Assertion
Ref Expression
ax-hilex  |-  ~H  e.  _V

Detailed syntax breakdown of Axiom ax-hilex
StepHypRef Expression
1 chil 22427 . 2  class  ~H
2 cvv 2958 . 2  class  _V
31, 2wcel 1726 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  22519  hilablo  22667  hhph  22685  hcau  22691  hlimadd  22700  hhcms  22710  issh  22715  shex  22719  hlim0  22743  hhssva  22764  hhsssm  22765  hhssnm  22766  hhshsslem1  22772  hhsscms  22784  ocval  22787  spanval  22840  hsupval  22841  sshjval  22857  sshjval3  22861  pjhfval  22903  pjmfn  23222  pjmf1  23223  hosmval  23243  hommval  23244  hodmval  23245  hfsmval  23246  hfmmval  23247  nmopval  23364  elcnop  23365  ellnop  23366  elunop  23380  elhmop  23381  hmopex  23383  nmfnval  23384  nlfnval  23389  elcnfn  23390  ellnfn  23391  dmadjss  23395  dmadjop  23396  adjeu  23397  adjval  23398  eigvecval  23404  eigvalfval  23405  specval  23406  hhcno  23412  hhcnf  23413  adjeq  23443  brafval  23451  kbfval  23460  adjbdln  23591  rnbra  23615  bra11  23616  leoprf2  23635  ishst  23722
  Copyright terms: Public domain W3C validator