Axiom ax-hilex 31072

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

This axiom is referenced by:  hvmulex  31084  hilablo  31233  hhph  31251  hcau  31257  hlimadd  31266  hhcms  31276  issh  31281  shex  31285  hlim0  31308  hhssva  31330  hhsssm  31331  hhssnm  31332  hhshsslem1  31340  hhsscms  31351  ocval  31353  spanval  31406  hsupval  31407  sshjval  31423  sshjval3  31427  pjhfval  31469  pjmfn  31788  pjmf1  31789  hosmval  31808  hommval  31809  hodmval  31810  hfsmval  31811  hfmmval  31812  nmopval  31929  elcnop  31930  ellnop  31931  elunop  31945  elhmop  31946  hmopex  31948  nmfnval  31949  nlfnval  31954  elcnfn  31955  ellnfn  31956  dmadjss  31960  dmadjop  31961  adjeu  31962  adjval  31963  eigvecval  31969  eigvalfval  31970  specval  31971  hhcno  31977  hhcnf  31978  adjeq  32008  brafval  32016  kbfval  32025  adjbdln  32156  rnbra  32180  bra11  32181  leoprf2  32200  ishst  32287