Axiom ax-hilex 31288

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 31208	. 2 class ℋ
2		cvv 3463	. 2 class V
3	1, 2	wcel 2149	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  31300  hilablo  31449  hhph  31467  hcau  31473  hlimadd  31482  hhcms  31492  issh  31497  shex  31501  hlim0  31524  hhssva  31546  hhsssm  31547  hhssnm  31548  hhshsslem1  31556  hhsscms  31567  ocval  31569  spanval  31622  hsupval  31623  sshjval  31639  sshjval3  31643  pjhfval  31685  pjmfn  32004  pjmf1  32005  hosmval  32024  hommval  32025  hodmval  32026  hfsmval  32027  hfmmval  32028  nmopval  32145  elcnop  32146  ellnop  32147  elunop  32161  elhmop  32162  hmopex  32164  nmfnval  32165  nlfnval  32170  elcnfn  32171  ellnfn  32172  dmadjss  32176  dmadjop  32177  adjeu  32178  adjval  32179  eigvecval  32185  eigvalfval  32186  specval  32187  hhcno  32193  hhcnf  32194  adjeq  32224  brafval  32232  kbfval  32241  adjbdln  32372  rnbra  32396  bra11  32397  leoprf2  32416  ishst  32503