Axiom ax-hilex 30761

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 30681	. 2 class ℋ
2		cvv 3468	. 2 class V
3	1, 2	wcel 2098	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30773  hilablo  30922  hhph  30940  hcau  30946  hlimadd  30955  hhcms  30965  issh  30970  shex  30974  hlim0  30997  hhssva  31019  hhsssm  31020  hhssnm  31021  hhshsslem1  31029  hhsscms  31040  ocval  31042  spanval  31095  hsupval  31096  sshjval  31112  sshjval3  31116  pjhfval  31158  pjmfn  31477  pjmf1  31478  hosmval  31497  hommval  31498  hodmval  31499  hfsmval  31500  hfmmval  31501  nmopval  31618  elcnop  31619  ellnop  31620  elunop  31634  elhmop  31635  hmopex  31637  nmfnval  31638  nlfnval  31643  elcnfn  31644  ellnfn  31645  dmadjss  31649  dmadjop  31650  adjeu  31651  adjval  31652  eigvecval  31658  eigvalfval  31659  specval  31660  hhcno  31666  hhcnf  31667  adjeq  31697  brafval  31705  kbfval  31714  adjbdln  31845  rnbra  31869  bra11  31870  leoprf2  31889  ishst  31976