Axiom ax-hilex 31594

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 31514	. 2 class ℋ
2		cvv 3451	. 2 class V
3	1, 2	wcel 2145	1 wff ℋ ∈ V

This axiom is used by:  hvmulex  31606  hilablo  31755  hhph  31773  hcau  31779  hlimadd  31788  hhcms  31798  issh  31803  shex  31807  hlim0  31830  hhssva  31852  hhsssm  31853  hhssnm  31854  hhshsslem1  31862  hhsscms  31873  ocval  31875  spanval  31928  hsupval  31929  sshjval  31945  sshjval3  31949  pjhfval  31991  pjmfn  32310  pjmf1  32311  hosmval  32330  hommval  32331  hodmval  32332  hfsmval  32333  hfmmval  32334  nmopval  32451  elcnop  32452  ellnop  32453  elunop  32467  elhmop  32468  hmopex  32470  nmfnval  32471  nlfnval  32476  elcnfn  32477  ellnfn  32478  dmadjss  32482  dmadjop  32483  adjeu  32484  adjval  32485  eigvecval  32491  eigvalfval  32492  specval  32493  hhcno  32499  hhcnf  32500  adjeq  32530  brafval  32538  kbfval  32547  adjbdln  32678  rnbra  32702  bra11  32703  leoprf2  32722  ishst  32809