Axiom ax-hilex 31018

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 30938	. 2 class ℋ
2		cvv 3480	. 2 class V
3	1, 2	wcel 2108	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31030  hilablo  31179  hhph  31197  hcau  31203  hlimadd  31212  hhcms  31222  issh  31227  shex  31231  hlim0  31254  hhssva  31276  hhsssm  31277  hhssnm  31278  hhshsslem1  31286  hhsscms  31297  ocval  31299  spanval  31352  hsupval  31353  sshjval  31369  sshjval3  31373  pjhfval  31415  pjmfn  31734  pjmf1  31735  hosmval  31754  hommval  31755  hodmval  31756  hfsmval  31757  hfmmval  31758  nmopval  31875  elcnop  31876  ellnop  31877  elunop  31891  elhmop  31892  hmopex  31894  nmfnval  31895  nlfnval  31900  elcnfn  31901  ellnfn  31902  dmadjss  31906  dmadjop  31907  adjeu  31908  adjval  31909  eigvecval  31915  eigvalfval  31916  specval  31917  hhcno  31923  hhcnf  31924  adjeq  31954  brafval  31962  kbfval  31971  adjbdln  32102  rnbra  32126  bra11  32127  leoprf2  32146  ishst  32233