Axiom ax-hilex 31095

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 31015	. 2 class ℋ
2		cvv 3432	. 2 class V
3	1, 2	wcel 2119	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31107  hilablo  31256  hhph  31274  hcau  31280  hlimadd  31289  hhcms  31299  issh  31304  shex  31308  hlim0  31331  hhssva  31353  hhsssm  31354  hhssnm  31355  hhshsslem1  31363  hhsscms  31374  ocval  31376  spanval  31429  hsupval  31430  sshjval  31446  sshjval3  31450  pjhfval  31492  pjmfn  31811  pjmf1  31812  hosmval  31831  hommval  31832  hodmval  31833  hfsmval  31834  hfmmval  31835  nmopval  31952  elcnop  31953  ellnop  31954  elunop  31968  elhmop  31969  hmopex  31971  nmfnval  31972  nlfnval  31977  elcnfn  31978  ellnfn  31979  dmadjss  31983  dmadjop  31984  adjeu  31985  adjval  31986  eigvecval  31992  eigvalfval  31993  specval  31994  hhcno  32000  hhcnf  32001  adjeq  32031  brafval  32039  kbfval  32048  adjbdln  32179  rnbra  32203  bra11  32204  leoprf2  32223  ishst  32310