Axiom ax-hilex 30928

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

This axiom is referenced by:  hvmulex  30940  hilablo  31089  hhph  31107  hcau  31113  hlimadd  31122  hhcms  31132  issh  31137  shex  31141  hlim0  31164  hhssva  31186  hhsssm  31187  hhssnm  31188  hhshsslem1  31196  hhsscms  31207  ocval  31209  spanval  31262  hsupval  31263  sshjval  31279  sshjval3  31283  pjhfval  31325  pjmfn  31644  pjmf1  31645  hosmval  31664  hommval  31665  hodmval  31666  hfsmval  31667  hfmmval  31668  nmopval  31785  elcnop  31786  ellnop  31787  elunop  31801  elhmop  31802  hmopex  31804  nmfnval  31805  nlfnval  31810  elcnfn  31811  ellnfn  31812  dmadjss  31816  dmadjop  31817  adjeu  31818  adjval  31819  eigvecval  31825  eigvalfval  31826  specval  31827  hhcno  31833  hhcnf  31834  adjeq  31864  brafval  31872  kbfval  31881  adjbdln  32012  rnbra  32036  bra11  32037  leoprf2  32056  ishst  32143