Axiom ax-hilex 30837

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 30757	. 2 class ℋ
2		cvv 3473	. 2 class V
3	1, 2	wcel 2098	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30849  hilablo  30998  hhph  31016  hcau  31022  hlimadd  31031  hhcms  31041  issh  31046  shex  31050  hlim0  31073  hhssva  31095  hhsssm  31096  hhssnm  31097  hhshsslem1  31105  hhsscms  31116  ocval  31118  spanval  31171  hsupval  31172  sshjval  31188  sshjval3  31192  pjhfval  31234  pjmfn  31553  pjmf1  31554  hosmval  31573  hommval  31574  hodmval  31575  hfsmval  31576  hfmmval  31577  nmopval  31694  elcnop  31695  ellnop  31696  elunop  31710  elhmop  31711  hmopex  31713  nmfnval  31714  nlfnval  31719  elcnfn  31720  ellnfn  31721  dmadjss  31725  dmadjop  31726  adjeu  31727  adjval  31728  eigvecval  31734  eigvalfval  31735  specval  31736  hhcno  31742  hhcnf  31743  adjeq  31773  brafval  31781  kbfval  31790  adjbdln  31921  rnbra  31945  bra11  31946  leoprf2  31965  ishst  32052