Axiom ax-hilex 31158

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 31078	. 2 class ℋ
2		cvv 3453	. 2 class V
3	1, 2	wcel 2141	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31170  hilablo  31319  hhph  31337  hcau  31343  hlimadd  31352  hhcms  31362  issh  31367  shex  31371  hlim0  31394  hhssva  31416  hhsssm  31417  hhssnm  31418  hhshsslem1  31426  hhsscms  31437  ocval  31439  spanval  31492  hsupval  31493  sshjval  31509  sshjval3  31513  pjhfval  31555  pjmfn  31874  pjmf1  31875  hosmval  31894  hommval  31895  hodmval  31896  hfsmval  31897  hfmmval  31898  nmopval  32015  elcnop  32016  ellnop  32017  elunop  32031  elhmop  32032  hmopex  32034  nmfnval  32035  nlfnval  32040  elcnfn  32041  ellnfn  32042  dmadjss  32046  dmadjop  32047  adjeu  32048  adjval  32049  eigvecval  32055  eigvalfval  32056  specval  32057  hhcno  32063  hhcnf  32064  adjeq  32094  brafval  32102  kbfval  32111  adjbdln  32242  rnbra  32266  bra11  32267  leoprf2  32286  ishst  32373