Axiom ax-hilex 31380

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 31300	. 2 class ℋ
2		cvv 3457	. 2 class V
3	1, 2	wcel 2146	1 wff ℋ ∈ V

This axiom is used by:  hvmulex  31392  hilablo  31541  hhph  31559  hcau  31565  hlimadd  31574  hhcms  31584  issh  31589  shex  31593  hlim0  31616  hhssva  31638  hhsssm  31639  hhssnm  31640  hhshsslem1  31648  hhsscms  31659  ocval  31661  spanval  31714  hsupval  31715  sshjval  31731  sshjval3  31735  pjhfval  31777  pjmfn  32096  pjmf1  32097  hosmval  32116  hommval  32117  hodmval  32118  hfsmval  32119  hfmmval  32120  nmopval  32237  elcnop  32238  ellnop  32239  elunop  32253  elhmop  32254  hmopex  32256  nmfnval  32257  nlfnval  32262  elcnfn  32263  ellnfn  32264  dmadjss  32268  dmadjop  32269  adjeu  32270  adjval  32271  eigvecval  32277  eigvalfval  32278  specval  32279  hhcno  32285  hhcnf  32286  adjeq  32316  brafval  32324  kbfval  32333  adjbdln  32464  rnbra  32488  bra11  32489  leoprf2  32508  ishst  32595