Axiom ax-hilex 22455

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 22375	. 2 class ~H
2		cvv 2916	. 2 class _V
3	1, 2	wcel 1721	1 wff ~H e. _V

This axiom is referenced by:  hvmulex  22467  hilablo  22615  hhph  22633  hcau  22639  hlimadd  22648  hhcms  22658  issh  22663  shex  22667  hlim0  22691  hhssva  22712  hhsssm  22713  hhssnm  22714  hhshsslem1  22720  hhsscms  22732  ocval  22735  spanval  22788  hsupval  22789  sshjval  22805  sshjval3  22809  pjhfval  22851  pjmfn  23170  pjmf1  23171  hosmval  23191  hommval  23192  hodmval  23193  hfsmval  23194  hfmmval  23195  nmopval  23312  elcnop  23313  ellnop  23314  elunop  23328  elhmop  23329  hmopex  23331  nmfnval  23332  nlfnval  23337  elcnfn  23338  ellnfn  23339  dmadjss  23343  dmadjop  23344  adjeu  23345  adjval  23346  eigvecval  23352  eigvalfval  23353  specval  23354  hhcno  23360  hhcnf  23361  adjeq  23391  brafval  23399  kbfval  23408  adjbdln  23539  rnbra  23563  bra11  23564  leoprf2  23583  ishst  23670