Axiom ax-hilex 28432

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 28352	. 2 class ℋ
2		cvv 3398	. 2 class V
3	1, 2	wcel 2107	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  28444  hilablo  28593  hhph  28611  hcau  28617  hlimadd  28626  hhcms  28636  issh  28641  shex  28645  hlim0  28668  hhssva  28690  hhsssm  28691  hhssnm  28692  hhshsslem1  28700  hhsscms  28712  ocval  28715  spanval  28768  hsupval  28769  sshjval  28785  sshjval3  28789  pjhfval  28831  pjmfn  29150  pjmf1  29151  hosmval  29170  hommval  29171  hodmval  29172  hfsmval  29173  hfmmval  29174  nmopval  29291  elcnop  29292  ellnop  29293  elunop  29307  elhmop  29308  hmopex  29310  nmfnval  29311  nlfnval  29316  elcnfn  29317  ellnfn  29318  dmadjss  29322  dmadjop  29323  adjeu  29324  adjval  29325  eigvecval  29331  eigvalfval  29332  specval  29333  hhcno  29339  hhcnf  29340  adjeq  29370  brafval  29378  kbfval  29387  adjbdln  29518  rnbra  29542  bra11  29543  leoprf2  29562  ishst  29649