Axiom ax-hilex 26114

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 26034	. 2 class ~H
2		cvv 3106	. 2 class _V
3	1, 2	wcel 1823	1 wff ~H e. _V

This axiom is referenced by:  hvmulex  26126  hilablo  26275  hhph  26293  hcau  26299  hlimadd  26308  hhcms  26318  issh  26323  shex  26327  hlim0  26351  hhssva  26373  hhsssm  26374  hhssnm  26375  hhshsslem1  26381  hhsscms  26393  ocval  26396  spanval  26449  hsupval  26450  sshjval  26466  sshjval3  26470  pjhfval  26512  pjmfn  26831  pjmf1  26832  hosmval  26852  hommval  26853  hodmval  26854  hfsmval  26855  hfmmval  26856  nmopval  26973  elcnop  26974  ellnop  26975  elunop  26989  elhmop  26990  hmopex  26992  nmfnval  26993  nlfnval  26998  elcnfn  26999  ellnfn  27000  dmadjss  27004  dmadjop  27005  adjeu  27006  adjval  27007  eigvecval  27013  eigvalfval  27014  specval  27015  hhcno  27021  hhcnf  27022  adjeq  27052  brafval  27060  kbfval  27069  adjbdln  27200  rnbra  27224  bra11  27225  leoprf2  27244  ishst  27331