Axiom ax-hilex 31085

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

This axiom is referenced by:  hvmulex  31097  hilablo  31246  hhph  31264  hcau  31270  hlimadd  31279  hhcms  31289  issh  31294  shex  31298  hlim0  31321  hhssva  31343  hhsssm  31344  hhssnm  31345  hhshsslem1  31353  hhsscms  31364  ocval  31366  spanval  31419  hsupval  31420  sshjval  31436  sshjval3  31440  pjhfval  31482  pjmfn  31801  pjmf1  31802  hosmval  31821  hommval  31822  hodmval  31823  hfsmval  31824  hfmmval  31825  nmopval  31942  elcnop  31943  ellnop  31944  elunop  31958  elhmop  31959  hmopex  31961  nmfnval  31962  nlfnval  31967  elcnfn  31968  ellnfn  31969  dmadjss  31973  dmadjop  31974  adjeu  31975  adjval  31976  eigvecval  31982  eigvalfval  31983  specval  31984  hhcno  31990  hhcnf  31991  adjeq  32021  brafval  32029  kbfval  32038  adjbdln  32169  rnbra  32193  bra11  32194  leoprf2  32213  ishst  32300