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

Step	Hyp	Ref	Expression
1		chil 25705	. 2 class ~H
2		cvv 3093	. 2 class _V
3	1, 2	wcel 1802	1 wff ~H e. _V

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