Axiom ax-hilex 26708

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, ~H, which contains objects called vectors. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.)

Assertion

Ref	Expression
ax-hilex	|- ~H e. _V

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 26628	. 2 class ~H
2		cvv 3057	. 2 class _V
3	1, 2	wcel 1898	1 wff ~H e. _V

This axiom is referenced by:  hvmulex  26720  hilablo  26869  hhph  26887  hcau  26893  hlimadd  26902  hhcms  26912  issh  26917  shex  26921  hlim0  26944  hhssva  26966  hhsssm  26967  hhssnm  26968  hhshsslem1  26974  hhsscms  26986  ocval  26989  spanval  27042  hsupval  27043  sshjval  27059  sshjval3  27063  pjhfval  27105  pjmfn  27424  pjmf1  27425  hosmval  27444  hommval  27445  hodmval  27446  hfsmval  27447  hfmmval  27448  nmopval  27565  elcnop  27566  ellnop  27567  elunop  27581  elhmop  27582  hmopex  27584  nmfnval  27585  nlfnval  27590  elcnfn  27591  ellnfn  27592  dmadjss  27596  dmadjop  27597  adjeu  27598  adjval  27599  eigvecval  27605  eigvalfval  27606  specval  27607  hhcno  27613  hhcnf  27614  adjeq  27644  brafval  27652  kbfval  27661  adjbdln  27792  rnbra  27816  bra11  27817  leoprf2  27836  ishst  27923