Axiom ax-hilex 28195

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

This axiom is referenced by:  hvmulex  28207  hilablo  28356  hhph  28374  hcau  28380  hlimadd  28389  hhcms  28399  issh  28404  shex  28408  hlim0  28431  hhssva  28453  hhsssm  28454  hhssnm  28455  hhshsslem1  28463  hhsscms  28475  ocval  28478  spanval  28531  hsupval  28532  sshjval  28548  sshjval3  28552  pjhfval  28594  pjmfn  28913  pjmf1  28914  hosmval  28933  hommval  28934  hodmval  28935  hfsmval  28936  hfmmval  28937  nmopval  29054  elcnop  29055  ellnop  29056  elunop  29070  elhmop  29071  hmopex  29073  nmfnval  29074  nlfnval  29079  elcnfn  29080  ellnfn  29081  dmadjss  29085  dmadjop  29086  adjeu  29087  adjval  29088  eigvecval  29094  eigvalfval  29095  specval  29096  hhcno  29102  hhcnf  29103  adjeq  29133  brafval  29141  kbfval  29150  adjbdln  29281  rnbra  29305  bra11  29306  leoprf2  29325  ishst  29412