Axiom ax-hilex 28428

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 28348	. 2 class ℋ
2		cvv 3397	. 2 class V
3	1, 2	wcel 2106	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  28440  hilablo  28589  hhph  28607  hcau  28613  hlimadd  28622  hhcms  28632  issh  28637  shex  28641  hlim0  28664  hhssva  28686  hhsssm  28687  hhssnm  28688  hhshsslem1  28696  hhsscms  28708  ocval  28711  spanval  28764  hsupval  28765  sshjval  28781  sshjval3  28785  pjhfval  28827  pjmfn  29146  pjmf1  29147  hosmval  29166  hommval  29167  hodmval  29168  hfsmval  29169  hfmmval  29170  nmopval  29287  elcnop  29288  ellnop  29289  elunop  29303  elhmop  29304  hmopex  29306  nmfnval  29307  nlfnval  29312  elcnfn  29313  ellnfn  29314  dmadjss  29318  dmadjop  29319  adjeu  29320  adjval  29321  eigvecval  29327  eigvalfval  29328  specval  29329  hhcno  29335  hhcnf  29336  adjeq  29366  brafval  29374  kbfval  29383  adjbdln  29514  rnbra  29538  bra11  29539  leoprf2  29558  ishst  29645