Axiom ax-hilex 30977

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 30897	. 2 class ℋ
2		cvv 3436	. 2 class V
3	1, 2	wcel 2111	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30989  hilablo  31138  hhph  31156  hcau  31162  hlimadd  31171  hhcms  31181  issh  31186  shex  31190  hlim0  31213  hhssva  31235  hhsssm  31236  hhssnm  31237  hhshsslem1  31245  hhsscms  31256  ocval  31258  spanval  31311  hsupval  31312  sshjval  31328  sshjval3  31332  pjhfval  31374  pjmfn  31693  pjmf1  31694  hosmval  31713  hommval  31714  hodmval  31715  hfsmval  31716  hfmmval  31717  nmopval  31834  elcnop  31835  ellnop  31836  elunop  31850  elhmop  31851  hmopex  31853  nmfnval  31854  nlfnval  31859  elcnfn  31860  ellnfn  31861  dmadjss  31865  dmadjop  31866  adjeu  31867  adjval  31868  eigvecval  31874  eigvalfval  31875  specval  31876  hhcno  31882  hhcnf  31883  adjeq  31913  brafval  31921  kbfval  31930  adjbdln  32061  rnbra  32085  bra11  32086  leoprf2  32105  ishst  32192