Axiom ax-hilex 29370

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

This axiom is referenced by:  hvmulex  29382  hilablo  29531  hhph  29549  hcau  29555  hlimadd  29564  hhcms  29574  issh  29579  shex  29583  hlim0  29606  hhssva  29628  hhsssm  29629  hhssnm  29630  hhshsslem1  29638  hhsscms  29649  ocval  29651  spanval  29704  hsupval  29705  sshjval  29721  sshjval3  29725  pjhfval  29767  pjmfn  30086  pjmf1  30087  hosmval  30106  hommval  30107  hodmval  30108  hfsmval  30109  hfmmval  30110  nmopval  30227  elcnop  30228  ellnop  30229  elunop  30243  elhmop  30244  hmopex  30246  nmfnval  30247  nlfnval  30252  elcnfn  30253  ellnfn  30254  dmadjss  30258  dmadjop  30259  adjeu  30260  adjval  30261  eigvecval  30267  eigvalfval  30268  specval  30269  hhcno  30275  hhcnf  30276  adjeq  30306  brafval  30314  kbfval  30323  adjbdln  30454  rnbra  30478  bra11  30479  leoprf2  30498  ishst  30585