Axiom ax-hilex 31031

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

This axiom is referenced by:  hvmulex  31043  hilablo  31192  hhph  31210  hcau  31216  hlimadd  31225  hhcms  31235  issh  31240  shex  31244  hlim0  31267  hhssva  31289  hhsssm  31290  hhssnm  31291  hhshsslem1  31299  hhsscms  31310  ocval  31312  spanval  31365  hsupval  31366  sshjval  31382  sshjval3  31386  pjhfval  31428  pjmfn  31747  pjmf1  31748  hosmval  31767  hommval  31768  hodmval  31769  hfsmval  31770  hfmmval  31771  nmopval  31888  elcnop  31889  ellnop  31890  elunop  31904  elhmop  31905  hmopex  31907  nmfnval  31908  nlfnval  31913  elcnfn  31914  ellnfn  31915  dmadjss  31919  dmadjop  31920  adjeu  31921  adjval  31922  eigvecval  31928  eigvalfval  31929  specval  31930  hhcno  31936  hhcnf  31937  adjeq  31967  brafval  31975  kbfval  31984  adjbdln  32115  rnbra  32139  bra11  32140  leoprf2  32159  ishst  32246