Axiom ax-hilex 31086

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

This axiom is referenced by:  hvmulex  31098  hilablo  31247  hhph  31265  hcau  31271  hlimadd  31280  hhcms  31290  issh  31295  shex  31299  hlim0  31322  hhssva  31344  hhsssm  31345  hhssnm  31346  hhshsslem1  31354  hhsscms  31365  ocval  31367  spanval  31420  hsupval  31421  sshjval  31437  sshjval3  31441  pjhfval  31483  pjmfn  31802  pjmf1  31803  hosmval  31822  hommval  31823  hodmval  31824  hfsmval  31825  hfmmval  31826  nmopval  31943  elcnop  31944  ellnop  31945  elunop  31959  elhmop  31960  hmopex  31962  nmfnval  31963  nlfnval  31968  elcnfn  31969  ellnfn  31970  dmadjss  31974  dmadjop  31975  adjeu  31976  adjval  31977  eigvecval  31983  eigvalfval  31984  specval  31985  hhcno  31991  hhcnf  31992  adjeq  32022  brafval  32030  kbfval  32039  adjbdln  32170  rnbra  32194  bra11  32195  leoprf2  32214  ishst  32301