Metamath Proof Explorer


Axiom ax-hilex

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.)

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

Detailed syntax breakdown

Step Hyp Ref Expression
0 chba
 |-  ~H
1 cvv
 |-  _V
2 0 1 wcel
 |-  ~H e. _V