Axiom ax-hilex 30981

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 30901	. 2 class ℋ
2		cvv 3437	. 2 class V
3	1, 2	wcel 2113	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30993  hilablo  31142  hhph  31160  hcau  31166  hlimadd  31175  hhcms  31185  issh  31190  shex  31194  hlim0  31217  hhssva  31239  hhsssm  31240  hhssnm  31241  hhshsslem1  31249  hhsscms  31260  ocval  31262  spanval  31315  hsupval  31316  sshjval  31332  sshjval3  31336  pjhfval  31378  pjmfn  31697  pjmf1  31698  hosmval  31717  hommval  31718  hodmval  31719  hfsmval  31720  hfmmval  31721  nmopval  31838  elcnop  31839  ellnop  31840  elunop  31854  elhmop  31855  hmopex  31857  nmfnval  31858  nlfnval  31863  elcnfn  31864  ellnfn  31865  dmadjss  31869  dmadjop  31870  adjeu  31871  adjval  31872  eigvecval  31878  eigvalfval  31879  specval  31880  hhcno  31886  hhcnf  31887  adjeq  31917  brafval  31925  kbfval  31934  adjbdln  32065  rnbra  32089  bra11  32090  leoprf2  32109  ishst  32196