Axiom ax-hilex 29369

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 29289	. 2 class ℋ
2		cvv 3429	. 2 class V
3	1, 2	wcel 2106	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  29381  hilablo  29530  hhph  29548  hcau  29554  hlimadd  29563  hhcms  29573  issh  29578  shex  29582  hlim0  29605  hhssva  29627  hhsssm  29628  hhssnm  29629  hhshsslem1  29637  hhsscms  29648  ocval  29650  spanval  29703  hsupval  29704  sshjval  29720  sshjval3  29724  pjhfval  29766  pjmfn  30085  pjmf1  30086  hosmval  30105  hommval  30106  hodmval  30107  hfsmval  30108  hfmmval  30109  nmopval  30226  elcnop  30227  ellnop  30228  elunop  30242  elhmop  30243  hmopex  30245  nmfnval  30246  nlfnval  30251  elcnfn  30252  ellnfn  30253  dmadjss  30257  dmadjop  30258  adjeu  30259  adjval  30260  eigvecval  30266  eigvalfval  30267  specval  30268  hhcno  30274  hhcnf  30275  adjeq  30305  brafval  30313  kbfval  30322  adjbdln  30453  rnbra  30477  bra11  30478  leoprf2  30497  ishst  30584