Axiom ax-hilex 30935

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 30855	. 2 class ℋ
2		cvv 3450	. 2 class V
3	1, 2	wcel 2109	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30947  hilablo  31096  hhph  31114  hcau  31120  hlimadd  31129  hhcms  31139  issh  31144  shex  31148  hlim0  31171  hhssva  31193  hhsssm  31194  hhssnm  31195  hhshsslem1  31203  hhsscms  31214  ocval  31216  spanval  31269  hsupval  31270  sshjval  31286  sshjval3  31290  pjhfval  31332  pjmfn  31651  pjmf1  31652  hosmval  31671  hommval  31672  hodmval  31673  hfsmval  31674  hfmmval  31675  nmopval  31792  elcnop  31793  ellnop  31794  elunop  31808  elhmop  31809  hmopex  31811  nmfnval  31812  nlfnval  31817  elcnfn  31818  ellnfn  31819  dmadjss  31823  dmadjop  31824  adjeu  31825  adjval  31826  eigvecval  31832  eigvalfval  31833  specval  31834  hhcno  31840  hhcnf  31841  adjeq  31871  brafval  31879  kbfval  31888  adjbdln  32019  rnbra  32043  bra11  32044  leoprf2  32063  ishst  32150