HomeHome Hilbert Space Explorer < Previous   Next >
Related theorems
Unicode version

Axiom ax-hilex 4983
Description: This is our primary postulate for 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 whose properties are postulated in this axiom (which asserts that it is a set) and the axioms ax-hvaddcl 4984, ax-hvcom 4985, ax-hvass 4986, ax-hvzercl 4987, ax-hvaddid 4988, ax-hvmulcl 4989, ax-hvmulid 4991, ax-hvmulass 4992, ax-hvdistr1 4993, ax-hvdistr2 4994, ax-hvmulzer 4995, ax-hicl 5043, ax-his1 5045, ax-his2 5046, ax-his3 5047, ax-his4 5048, and ax-hcompl 5113. .
Assertion
Ref Expression
ax-hilex |- H~ e. V

Detailed syntax breakdown of Axiom ax-hilex
StepHypRef Expression
1 chil 4958 . 2 class H~
2 cvv 1348 . 2 class V
31, 2wcel 1092 1 wff H~ e. V
Colors of variables: wff set class
This axiom is referenced by:  shex 5115  sh 5116  ocvalt 5161  pjmvalt 5245  shsumvalt 5279  spanvalt 5300  hsupval2t 5301  sshjvalt 5321  sshjval3t 5327  hosmvalt 5487  hodmvalt 5488
metamath.org