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

Axiom ax-hilex 25785
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 25705 . 2  class  ~H
2 cvv 3093 . 2  class  _V
31, 2wcel 1802 1  wff  ~H  e.  _V
Colors of variables: wff setvar class
This axiom is referenced by:  hvmulex  25797  hilablo  25946  hhph  25964  hcau  25970  hlimadd  25979  hhcms  25989  issh  25994  shex  25998  hlim0  26022  hhssva  26044  hhsssm  26045  hhssnm  26046  hhshsslem1  26052  hhsscms  26064  ocval  26067  spanval  26120  hsupval  26121  sshjval  26137  sshjval3  26141  pjhfval  26183  pjmfn  26502  pjmf1  26503  hosmval  26523  hommval  26524  hodmval  26525  hfsmval  26526  hfmmval  26527  nmopval  26644  elcnop  26645  ellnop  26646  elunop  26660  elhmop  26661  hmopex  26663  nmfnval  26664  nlfnval  26669  elcnfn  26670  ellnfn  26671  dmadjss  26675  dmadjop  26676  adjeu  26677  adjval  26678  eigvecval  26684  eigvalfval  26685  specval  26686  hhcno  26692  hhcnf  26693  adjeq  26723  brafval  26731  kbfval  26740  adjbdln  26871  rnbra  26895  bra11  26896  leoprf2  26915  ishst  27002
  Copyright terms: Public domain W3C validator