Axiom ax-hilex 28770

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 28690	. 2 class ℋ
2		cvv 3494	. 2 class V
3	1, 2	wcel 2110	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  28782  hilablo  28931  hhph  28949  hcau  28955  hlimadd  28964  hhcms  28974  issh  28979  shex  28983  hlim0  29006  hhssva  29028  hhsssm  29029  hhssnm  29030  hhshsslem1  29038  hhsscms  29049  ocval  29051  spanval  29104  hsupval  29105  sshjval  29121  sshjval3  29125  pjhfval  29167  pjmfn  29486  pjmf1  29487  hosmval  29506  hommval  29507  hodmval  29508  hfsmval  29509  hfmmval  29510  nmopval  29627  elcnop  29628  ellnop  29629  elunop  29643  elhmop  29644  hmopex  29646  nmfnval  29647  nlfnval  29652  elcnfn  29653  ellnfn  29654  dmadjss  29658  dmadjop  29659  adjeu  29660  adjval  29661  eigvecval  29667  eigvalfval  29668  specval  29669  hhcno  29675  hhcnf  29676  adjeq  29706  brafval  29714  kbfval  29723  adjbdln  29854  rnbra  29878  bra11  29879  leoprf2  29898  ishst  29985