Axiom ax-hilex 30934

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

This axiom is referenced by:  hvmulex  30946  hilablo  31095  hhph  31113  hcau  31119  hlimadd  31128  hhcms  31138  issh  31143  shex  31147  hlim0  31170  hhssva  31192  hhsssm  31193  hhssnm  31194  hhshsslem1  31202  hhsscms  31213  ocval  31215  spanval  31268  hsupval  31269  sshjval  31285  sshjval3  31289  pjhfval  31331  pjmfn  31650  pjmf1  31651  hosmval  31670  hommval  31671  hodmval  31672  hfsmval  31673  hfmmval  31674  nmopval  31791  elcnop  31792  ellnop  31793  elunop  31807  elhmop  31808  hmopex  31810  nmfnval  31811  nlfnval  31816  elcnfn  31817  ellnfn  31818  dmadjss  31822  dmadjop  31823  adjeu  31824  adjval  31825  eigvecval  31831  eigvalfval  31832  specval  31833  hhcno  31839  hhcnf  31840  adjeq  31870  brafval  31878  kbfval  31887  adjbdln  32018  rnbra  32042  bra11  32043  leoprf2  32062  ishst  32149