Axiom ax-hilex 31607

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 31527	. 2 class ℋ
2		cvv 3450	. 2 class V
3	1, 2	wcel 2144	1 wff ℋ ∈ V

This axiom is used by:  hvmulex  31619  hilablo  31768  hhph  31786  hcau  31792  hlimadd  31801  hhcms  31811  issh  31816  shex  31820  hlim0  31843  hhssva  31865  hhsssm  31866  hhssnm  31867  hhshsslem1  31875  hhsscms  31886  ocval  31888  spanval  31941  hsupval  31942  sshjval  31958  sshjval3  31962  pjhfval  32004  pjmfn  32323  pjmf1  32324  hosmval  32343  hommval  32344  hodmval  32345  hfsmval  32346  hfmmval  32347  nmopval  32464  elcnop  32465  ellnop  32466  elunop  32480  elhmop  32481  hmopex  32483  nmfnval  32484  nlfnval  32489  elcnfn  32490  ellnfn  32491  dmadjss  32495  dmadjop  32496  adjeu  32497  adjval  32498  eigvecval  32504  eigvalfval  32505  specval  32506  hhcno  32512  hhcnf  32513  adjeq  32543  brafval  32551  kbfval  32560  adjbdln  32691  rnbra  32715  bra11  32716  leoprf2  32735  ishst  32822