Axiom ax-hilex 26487

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 26407	. 2 class ~H
2		cvv 3087	. 2 class _V
3	1, 2	wcel 1870	1 wff ~H e. _V

This axiom is referenced by:  hvmulex  26499  hilablo  26648  hhph  26666  hcau  26672  hlimadd  26681  hhcms  26691  issh  26696  shex  26700  hlim0  26723  hhssva  26745  hhsssm  26746  hhssnm  26747  hhshsslem1  26753  hhsscms  26765  ocval  26768  spanval  26821  hsupval  26822  sshjval  26838  sshjval3  26842  pjhfval  26884  pjmfn  27203  pjmf1  27204  hosmval  27223  hommval  27224  hodmval  27225  hfsmval  27226  hfmmval  27227  nmopval  27344  elcnop  27345  ellnop  27346  elunop  27360  elhmop  27361  hmopex  27363  nmfnval  27364  nlfnval  27369  elcnfn  27370  ellnfn  27371  dmadjss  27375  dmadjop  27376  adjeu  27377  adjval  27378  eigvecval  27384  eigvalfval  27385  specval  27386  hhcno  27392  hhcnf  27393  adjeq  27423  brafval  27431  kbfval  27440  adjbdln  27571  rnbra  27595  bra11  27596  leoprf2  27615  ishst  27702