Axiom ax-hilex 30240

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 30160	. 2 class ℋ
2		cvv 3475	. 2 class V
3	1, 2	wcel 2107	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30252  hilablo  30401  hhph  30419  hcau  30425  hlimadd  30434  hhcms  30444  issh  30449  shex  30453  hlim0  30476  hhssva  30498  hhsssm  30499  hhssnm  30500  hhshsslem1  30508  hhsscms  30519  ocval  30521  spanval  30574  hsupval  30575  sshjval  30591  sshjval3  30595  pjhfval  30637  pjmfn  30956  pjmf1  30957  hosmval  30976  hommval  30977  hodmval  30978  hfsmval  30979  hfmmval  30980  nmopval  31097  elcnop  31098  ellnop  31099  elunop  31113  elhmop  31114  hmopex  31116  nmfnval  31117  nlfnval  31122  elcnfn  31123  ellnfn  31124  dmadjss  31128  dmadjop  31129  adjeu  31130  adjval  31131  eigvecval  31137  eigvalfval  31138  specval  31139  hhcno  31145  hhcnf  31146  adjeq  31176  brafval  31184  kbfval  31193  adjbdln  31324  rnbra  31348  bra11  31349  leoprf2  31368  ishst  31455