Axiom ax-hilex 30926

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, ℋ, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hilex	⊢ ℋ ∈ V

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chba 30846	. 2 class ℋ
2		cvv 3462	. 2 class V
3	1, 2	wcel 2099	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30938  hilablo  31087  hhph  31105  hcau  31111  hlimadd  31120  hhcms  31130  issh  31135  shex  31139  hlim0  31162  hhssva  31184  hhsssm  31185  hhssnm  31186  hhshsslem1  31194  hhsscms  31205  ocval  31207  spanval  31260  hsupval  31261  sshjval  31277  sshjval3  31281  pjhfval  31323  pjmfn  31642  pjmf1  31643  hosmval  31662  hommval  31663  hodmval  31664  hfsmval  31665  hfmmval  31666  nmopval  31783  elcnop  31784  ellnop  31785  elunop  31799  elhmop  31800  hmopex  31802  nmfnval  31803  nlfnval  31808  elcnfn  31809  ellnfn  31810  dmadjss  31814  dmadjop  31815  adjeu  31816  adjval  31817  eigvecval  31823  eigvalfval  31824  specval  31825  hhcno  31831  hhcnf  31832  adjeq  31862  brafval  31870  kbfval  31879  adjbdln  32010  rnbra  32034  bra11  32035  leoprf2  32054  ishst  32141