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

Axiom ax-hilex 21409
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 21329 . 2  class  ~H
2 cvv 2727 . 2  class  _V
31, 2wcel 1621 1  wff  ~H  e.  _V
Colors of variables: wff set class
This axiom is referenced by:  hvmulex  21421  hilablo  21569  hhph  21587  hcau  21593  hlimadd  21602  hhcms  21612  issh  21617  shex  21621  hlim0  21645  hhssva  21666  hhsssm  21667  hhssnm  21668  hhshsslem1  21674  hhsscms  21686  ocval  21689  spanval  21742  hsupval  21743  sshjval  21759  sshjval3  21763  pjhfval  21805  hosmval  21997  hommval  21998  hodmval  21999  hfsmval  22000  hfmmval  22001  pjmfn  22142  pjmf1  22143  nmopval  22266  elcnop  22267  ellnop  22268  elunop  22282  elhmop  22283  hmopex  22285  nmfnval  22286  nlfnval  22291  elcnfn  22292  ellnfn  22293  dmadjss  22297  dmadjop  22298  adjeu  22299  adjval  22300  eigvecval  22306  eigvalfval  22307  specval  22308  hhcno  22314  hhcnf  22315  adjeq  22345  brafval  22353  kbfval  22362  adjbdln  22493  rnbra  22517  bra11  22518  leoprf2  22537  ishst  22624
  Copyright terms: Public domain W3C validator