Axiom ax-hilex 25592

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 25512	. 2 class ~H
2		cvv 3113	. 2 class _V
3	1, 2	wcel 1767	1 wff ~H e. _V

This axiom is referenced by:  hvmulex  25604  hilablo  25753  hhph  25771  hcau  25777  hlimadd  25786  hhcms  25796  issh  25801  shex  25805  hlim0  25829  hhssva  25851  hhsssm  25852  hhssnm  25853  hhshsslem1  25859  hhsscms  25871  ocval  25874  spanval  25927  hsupval  25928  sshjval  25944  sshjval3  25948  pjhfval  25990  pjmfn  26309  pjmf1  26310  hosmval  26330  hommval  26331  hodmval  26332  hfsmval  26333  hfmmval  26334  nmopval  26451  elcnop  26452  ellnop  26453  elunop  26467  elhmop  26468  hmopex  26470  nmfnval  26471  nlfnval  26476  elcnfn  26477  ellnfn  26478  dmadjss  26482  dmadjop  26483  adjeu  26484  adjval  26485  eigvecval  26491  eigvalfval  26492  specval  26493  hhcno  26499  hhcnf  26500  adjeq  26530  brafval  26538  kbfval  26547  adjbdln  26678  rnbra  26702  bra11  26703  leoprf2  26722  ishst  26809