Axiom ax-hilex 27856

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		chil 27776	. 2 class ℋ
2		cvv 3200	. 2 class V
3	1, 2	wcel 1990	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  27868  hilablo  28017  hhph  28035  hcau  28041  hlimadd  28050  hhcms  28060  issh  28065  shex  28069  hlim0  28092  hhssva  28114  hhsssm  28115  hhssnm  28116  hhshsslem1  28124  hhsscms  28136  ocval  28139  spanval  28192  hsupval  28193  sshjval  28209  sshjval3  28213  pjhfval  28255  pjmfn  28574  pjmf1  28575  hosmval  28594  hommval  28595  hodmval  28596  hfsmval  28597  hfmmval  28598  nmopval  28715  elcnop  28716  ellnop  28717  elunop  28731  elhmop  28732  hmopex  28734  nmfnval  28735  nlfnval  28740  elcnfn  28741  ellnfn  28742  dmadjss  28746  dmadjop  28747  adjeu  28748  adjval  28749  eigvecval  28755  eigvalfval  28756  specval  28757  hhcno  28763  hhcnf  28764  adjeq  28794  brafval  28802  kbfval  28811  adjbdln  28942  rnbra  28966  bra11  28967  leoprf2  28986  ishst  29073