Axiom ax-hilex 30961

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 30881	. 2 class ℋ
2		cvv 3438	. 2 class V
3	1, 2	wcel 2109	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex  30973  hilablo  31122  hhph  31140  hcau  31146  hlimadd  31155  hhcms  31165  issh  31170  shex  31174  hlim0  31197  hhssva  31219  hhsssm  31220  hhssnm  31221  hhshsslem1  31229  hhsscms  31240  ocval  31242  spanval  31295  hsupval  31296  sshjval  31312  sshjval3  31316  pjhfval  31358  pjmfn  31677  pjmf1  31678  hosmval  31697  hommval  31698  hodmval  31699  hfsmval  31700  hfmmval  31701  nmopval  31818  elcnop  31819  ellnop  31820  elunop  31834  elhmop  31835  hmopex  31837  nmfnval  31838  nlfnval  31843  elcnfn  31844  ellnfn  31845  dmadjss  31849  dmadjop  31850  adjeu  31851  adjval  31852  eigvecval  31858  eigvalfval  31859  specval  31860  hhcno  31866  hhcnf  31867  adjeq  31897  brafval  31905  kbfval  31914  adjbdln  32045  rnbra  32069  bra11  32070  leoprf2  32089  ishst  32176