Axiom ax-hilex 30519

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 30439	. 2 class ℋ
2		cvv 3472	. 2 class V
3	1, 2	wcel 2104	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30531  hilablo  30680  hhph  30698  hcau  30704  hlimadd  30713  hhcms  30723  issh  30728  shex  30732  hlim0  30755  hhssva  30777  hhsssm  30778  hhssnm  30779  hhshsslem1  30787  hhsscms  30798  ocval  30800  spanval  30853  hsupval  30854  sshjval  30870  sshjval3  30874  pjhfval  30916  pjmfn  31235  pjmf1  31236  hosmval  31255  hommval  31256  hodmval  31257  hfsmval  31258  hfmmval  31259  nmopval  31376  elcnop  31377  ellnop  31378  elunop  31392  elhmop  31393  hmopex  31395  nmfnval  31396  nlfnval  31401  elcnfn  31402  ellnfn  31403  dmadjss  31407  dmadjop  31408  adjeu  31409  adjval  31410  eigvecval  31416  eigvalfval  31417  specval  31418  hhcno  31424  hhcnf  31425  adjeq  31455  brafval  31463  kbfval  31472  adjbdln  31603  rnbra  31627  bra11  31628  leoprf2  31647  ishst  31734