Axiom ax-hilex 29262

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 29182	. 2 class ℋ
2		cvv 3422	. 2 class V
3	1, 2	wcel 2108	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  29274  hilablo  29423  hhph  29441  hcau  29447  hlimadd  29456  hhcms  29466  issh  29471  shex  29475  hlim0  29498  hhssva  29520  hhsssm  29521  hhssnm  29522  hhshsslem1  29530  hhsscms  29541  ocval  29543  spanval  29596  hsupval  29597  sshjval  29613  sshjval3  29617  pjhfval  29659  pjmfn  29978  pjmf1  29979  hosmval  29998  hommval  29999  hodmval  30000  hfsmval  30001  hfmmval  30002  nmopval  30119  elcnop  30120  ellnop  30121  elunop  30135  elhmop  30136  hmopex  30138  nmfnval  30139  nlfnval  30144  elcnfn  30145  ellnfn  30146  dmadjss  30150  dmadjop  30151  adjeu  30152  adjval  30153  eigvecval  30159  eigvalfval  30160  specval  30161  hhcno  30167  hhcnf  30168  adjeq  30198  brafval  30206  kbfval  30215  adjbdln  30346  rnbra  30370  bra11  30371  leoprf2  30390  ishst  30477