Axiom ax-hilex 27240

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 27160	. 2 class ℋ
2		cvv 3173	. 2 class V
3	1, 2	wcel 1977	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  27252  hilablo  27401  hhph  27419  hcau  27425  hlimadd  27434  hhcms  27444  issh  27449  shex  27453  hlim0  27476  hhssva  27498  hhsssm  27499  hhssnm  27500  hhshsslem1  27508  hhsscms  27520  ocval  27523  spanval  27576  hsupval  27577  sshjval  27593  sshjval3  27597  pjhfval  27639  pjmfn  27958  pjmf1  27959  hosmval  27978  hommval  27979  hodmval  27980  hfsmval  27981  hfmmval  27982  nmopval  28099  elcnop  28100  ellnop  28101  elunop  28115  elhmop  28116  hmopex  28118  nmfnval  28119  nlfnval  28124  elcnfn  28125  ellnfn  28126  dmadjss  28130  dmadjop  28131  adjeu  28132  adjval  28133  eigvecval  28139  eigvalfval  28140  specval  28141  hhcno  28147  hhcnf  28148  adjeq  28178  brafval  28186  kbfval  28195  adjbdln  28326  rnbra  28350  bra11  28351  leoprf2  28370  ishst  28457