Axiom ax-hilex 31480

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 31400	. 2 class ℋ
2		cvv 3450	. 2 class V
3	1, 2	wcel 2145	1 wff ℋ ∈ V

This axiom is used by:  hvmulex  31492  hilablo  31641  hhph  31659  hcau  31665  hlimadd  31674  hhcms  31684  issh  31689  shex  31693  hlim0  31716  hhssva  31738  hhsssm  31739  hhssnm  31740  hhshsslem1  31748  hhsscms  31759  ocval  31761  spanval  31814  hsupval  31815  sshjval  31831  sshjval3  31835  pjhfval  31877  pjmfn  32196  pjmf1  32197  hosmval  32216  hommval  32217  hodmval  32218  hfsmval  32219  hfmmval  32220  nmopval  32337  elcnop  32338  ellnop  32339  elunop  32353  elhmop  32354  hmopex  32356  nmfnval  32357  nlfnval  32362  elcnfn  32363  ellnfn  32364  dmadjss  32368  dmadjop  32369  adjeu  32370  adjval  32371  eigvecval  32377  eigvalfval  32378  specval  32379  hhcno  32385  hhcnf  32386  adjeq  32416  brafval  32424  kbfval  32433  adjbdln  32564  rnbra  32588  bra11  32589  leoprf2  32608  ishst  32695