Axiom ax-hilex 31070

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 30990	. 2 class ℋ
2		cvv 3429	. 2 class V
3	1, 2	wcel 2114	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31082  hilablo  31231  hhph  31249  hcau  31255  hlimadd  31264  hhcms  31274  issh  31279  shex  31283  hlim0  31306  hhssva  31328  hhsssm  31329  hhssnm  31330  hhshsslem1  31338  hhsscms  31349  ocval  31351  spanval  31404  hsupval  31405  sshjval  31421  sshjval3  31425  pjhfval  31467  pjmfn  31786  pjmf1  31787  hosmval  31806  hommval  31807  hodmval  31808  hfsmval  31809  hfmmval  31810  nmopval  31927  elcnop  31928  ellnop  31929  elunop  31943  elhmop  31944  hmopex  31946  nmfnval  31947  nlfnval  31952  elcnfn  31953  ellnfn  31954  dmadjss  31958  dmadjop  31959  adjeu  31960  adjval  31961  eigvecval  31967  eigvalfval  31968  specval  31969  hhcno  31975  hhcnf  31976  adjeq  32006  brafval  32014  kbfval  32023  adjbdln  32154  rnbra  32178  bra11  32179  leoprf2  32198  ishst  32285