Axiom ax-hilex 28782

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 28702	. 2 class ℋ
2		cvv 3441	. 2 class V
3	1, 2	wcel 2111	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  28794  hilablo  28943  hhph  28961  hcau  28967  hlimadd  28976  hhcms  28986  issh  28991  shex  28995  hlim0  29018  hhssva  29040  hhsssm  29041  hhssnm  29042  hhshsslem1  29050  hhsscms  29061  ocval  29063  spanval  29116  hsupval  29117  sshjval  29133  sshjval3  29137  pjhfval  29179  pjmfn  29498  pjmf1  29499  hosmval  29518  hommval  29519  hodmval  29520  hfsmval  29521  hfmmval  29522  nmopval  29639  elcnop  29640  ellnop  29641  elunop  29655  elhmop  29656  hmopex  29658  nmfnval  29659  nlfnval  29664  elcnfn  29665  ellnfn  29666  dmadjss  29670  dmadjop  29671  adjeu  29672  adjval  29673  eigvecval  29679  eigvalfval  29680  specval  29681  hhcno  29687  hhcnf  29688  adjeq  29718  brafval  29726  kbfval  29735  adjbdln  29866  rnbra  29890  bra11  29891  leoprf2  29910  ishst  29997