Axiom ax-hilex 27984

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		chil 27904	. 2 class ℋ
2		cvv 3231	. 2 class V
3	1, 2	wcel 2030	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  27996  hilablo  28145  hhph  28163  hcau  28169  hlimadd  28178  hhcms  28188  issh  28193  shex  28197  hlim0  28220  hhssva  28242  hhsssm  28243  hhssnm  28244  hhshsslem1  28252  hhsscms  28264  ocval  28267  spanval  28320  hsupval  28321  sshjval  28337  sshjval3  28341  pjhfval  28383  pjmfn  28702  pjmf1  28703  hosmval  28722  hommval  28723  hodmval  28724  hfsmval  28725  hfmmval  28726  nmopval  28843  elcnop  28844  ellnop  28845  elunop  28859  elhmop  28860  hmopex  28862  nmfnval  28863  nlfnval  28868  elcnfn  28869  ellnfn  28870  dmadjss  28874  dmadjop  28875  adjeu  28876  adjval  28877  eigvecval  28883  eigvalfval  28884  specval  28885  hhcno  28891  hhcnf  28892  adjeq  28922  brafval  28930  kbfval  28939  adjbdln  29070  rnbra  29094  bra11  29095  leoprf2  29114  ishst  29201