Axiom ax-hilex 26651

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 26571	. 2 class ~H
2		cvv 3080	. 2 class _V
3	1, 2	wcel 1872	1 wff ~H e. _V

This axiom is referenced by:  hvmulex  26663  hilablo  26812  hhph  26830  hcau  26836  hlimadd  26845  hhcms  26855  issh  26860  shex  26864  hlim0  26887  hhssva  26909  hhsssm  26910  hhssnm  26911  hhshsslem1  26917  hhsscms  26929  ocval  26932  spanval  26985  hsupval  26986  sshjval  27002  sshjval3  27006  pjhfval  27048  pjmfn  27367  pjmf1  27368  hosmval  27387  hommval  27388  hodmval  27389  hfsmval  27390  hfmmval  27391  nmopval  27508  elcnop  27509  ellnop  27510  elunop  27524  elhmop  27525  hmopex  27527  nmfnval  27528  nlfnval  27533  elcnfn  27534  ellnfn  27535  dmadjss  27539  dmadjop  27540  adjeu  27541  adjval  27542  eigvecval  27548  eigvalfval  27549  specval  27550  hhcno  27556  hhcnf  27557  adjeq  27587  brafval  27595  kbfval  27604  adjbdln  27735  rnbra  27759  bra11  27760  leoprf2  27779  ishst  27866