Axiom ax-hilex 31074

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

This axiom is referenced by:  hvmulex  31086  hilablo  31235  hhph  31253  hcau  31259  hlimadd  31268  hhcms  31278  issh  31283  shex  31287  hlim0  31310  hhssva  31332  hhsssm  31333  hhssnm  31334  hhshsslem1  31342  hhsscms  31353  ocval  31355  spanval  31408  hsupval  31409  sshjval  31425  sshjval3  31429  pjhfval  31471  pjmfn  31790  pjmf1  31791  hosmval  31810  hommval  31811  hodmval  31812  hfsmval  31813  hfmmval  31814  nmopval  31931  elcnop  31932  ellnop  31933  elunop  31947  elhmop  31948  hmopex  31950  nmfnval  31951  nlfnval  31956  elcnfn  31957  ellnfn  31958  dmadjss  31962  dmadjop  31963  adjeu  31964  adjval  31965  eigvecval  31971  eigvalfval  31972  specval  31973  hhcno  31979  hhcnf  31980  adjeq  32010  brafval  32018  kbfval  32027  adjbdln  32158  rnbra  32182  bra11  32183  leoprf2  32202  ishst  32289