Axiom ax-hilex 31332

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 31252	. 2 class ℋ
2		cvv 3455	. 2 class V
3	1, 2	wcel 2143	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31344  hilablo  31493  hhph  31511  hcau  31517  hlimadd  31526  hhcms  31536  issh  31541  shex  31545  hlim0  31568  hhssva  31590  hhsssm  31591  hhssnm  31592  hhshsslem1  31600  hhsscms  31611  ocval  31613  spanval  31666  hsupval  31667  sshjval  31683  sshjval3  31687  pjhfval  31729  pjmfn  32048  pjmf1  32049  hosmval  32068  hommval  32069  hodmval  32070  hfsmval  32071  hfmmval  32072  nmopval  32189  elcnop  32190  ellnop  32191  elunop  32205  elhmop  32206  hmopex  32208  nmfnval  32209  nlfnval  32214  elcnfn  32215  ellnfn  32216  dmadjss  32220  dmadjop  32221  adjeu  32222  adjval  32223  eigvecval  32229  eigvalfval  32230  specval  32231  hhcno  32237  hhcnf  32238  adjeq  32268  brafval  32276  kbfval  32285  adjbdln  32416  rnbra  32440  bra11  32441  leoprf2  32460  ishst  32547