Axiom ax-hilex 31658

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 31578	. 2 class ℋ
2		cvv 3454	. 2 class V
3	1, 2	wcel 2147	1 wff ℋ ∈ V

This axiom is used by:  hvmulex  31670  hilablo  31819  hhph  31837  hcau  31843  hlimadd  31852  hhcms  31862  issh  31867  shex  31871  hlim0  31894  hhssva  31916  hhsssm  31917  hhssnm  31918  hhshsslem1  31926  hhsscms  31937  ocval  31939  spanval  31992  hsupval  31993  sshjval  32009  sshjval3  32013  pjhfval  32055  pjmfn  32374  pjmf1  32375  hosmval  32394  hommval  32395  hodmval  32396  hfsmval  32397  hfmmval  32398  nmopval  32515  elcnop  32516  ellnop  32517  elunop  32531  elhmop  32532  hmopex  32534  nmfnval  32535  nlfnval  32540  elcnfn  32541  ellnfn  32542  dmadjss  32546  dmadjop  32547  adjeu  32548  adjval  32549  eigvecval  32555  eigvalfval  32556  specval  32557  hhcno  32563  hhcnf  32564  adjeq  32594  brafval  32602  kbfval  32611  adjbdln  32742  rnbra  32766  bra11  32767  leoprf2  32786  ishst  32873