Axiom ax-hilex 28776

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 28696	. 2 class ℋ
2		cvv 3494	. 2 class V
3	1, 2	wcel 2114	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  28788  hilablo  28937  hhph  28955  hcau  28961  hlimadd  28970  hhcms  28980  issh  28985  shex  28989  hlim0  29012  hhssva  29034  hhsssm  29035  hhssnm  29036  hhshsslem1  29044  hhsscms  29055  ocval  29057  spanval  29110  hsupval  29111  sshjval  29127  sshjval3  29131  pjhfval  29173  pjmfn  29492  pjmf1  29493  hosmval  29512  hommval  29513  hodmval  29514  hfsmval  29515  hfmmval  29516  nmopval  29633  elcnop  29634  ellnop  29635  elunop  29649  elhmop  29650  hmopex  29652  nmfnval  29653  nlfnval  29658  elcnfn  29659  ellnfn  29660  dmadjss  29664  dmadjop  29665  adjeu  29666  adjval  29667  eigvecval  29673  eigvalfval  29674  specval  29675  hhcno  29681  hhcnf  29682  adjeq  29712  brafval  29720  kbfval  29729  adjbdln  29860  rnbra  29884  bra11  29885  leoprf2  29904  ishst  29991