Axiom ax-hilex 31027

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 30947	. 2 class ℋ
2		cvv 3477	. 2 class V
3	1, 2	wcel 2105	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31039  hilablo  31188  hhph  31206  hcau  31212  hlimadd  31221  hhcms  31231  issh  31236  shex  31240  hlim0  31263  hhssva  31285  hhsssm  31286  hhssnm  31287  hhshsslem1  31295  hhsscms  31306  ocval  31308  spanval  31361  hsupval  31362  sshjval  31378  sshjval3  31382  pjhfval  31424  pjmfn  31743  pjmf1  31744  hosmval  31763  hommval  31764  hodmval  31765  hfsmval  31766  hfmmval  31767  nmopval  31884  elcnop  31885  ellnop  31886  elunop  31900  elhmop  31901  hmopex  31903  nmfnval  31904  nlfnval  31909  elcnfn  31910  ellnfn  31911  dmadjss  31915  dmadjop  31916  adjeu  31917  adjval  31918  eigvecval  31924  eigvalfval  31925  specval  31926  hhcno  31932  hhcnf  31933  adjeq  31963  brafval  31971  kbfval  31980  adjbdln  32111  rnbra  32135  bra11  32136  leoprf2  32155  ishst  32242