Axiom ax-hilex 9144

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.

The 18 axioms for a complex Hilbert space consist of ax-hilex 9144, ax-hfvadd 9145, ax-hvcom 9146, ax-hvass 9147, ax-hv0cl 9148, ax-hvaddid 9149, ax-hfvmul 9150, ax-hvmulid 9151, ax-hvmulass 9152, ax-hvdistr1 9153, ax-hvdistr2 9154, ax-hvmul0 9155, ax-hfi 9222, ax-his1 9225, ax-his2 9226, ax-his3 9227, ax-his4 9228, and ax-hcompl 9347.

The axioms specify the properties of 5 primitive symbols, H~, +h, .h, 0h, and .ih.

If we can prove in ZFC set theory that a class U = <.<. +h , .h >., normh>. is a complex Hilbert space, i.e. that U e. CHil, then these axioms can be proved as theorems axhilex 9126, axhfvadd 9127, axhvcom 9128, axhvass 9129, axhv0cl 9130, axhvaddid 9131 , axhfvmul 9132, axhvmulid 9133, axhvmulass 9134, axhvdistr1 9135, axhvdistr2 9136 , axhvmul0 9137, axhfi 9138, axhis1 9139, axhis2 9140, axhis3 9141, axhis4 9142, and axhcompl 9143 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 9126.

Assertion

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

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 9063	. 2 class H~
2		cvv 1857	. 2 class V
3	1, 2	wcel 994	1 wff H~ e. V

This axiom is referenced by:  hvmulex 9156  hilabl 9303  hhph 9321  shex 9353  sh 9354  hhssnm 9407  hhsssh2 9416  ocval 9429  pjmval 9514  shsumval 9553  spanval 9575  hsupval2 9576  sshjval 9596  sshjval3 9602  hosmval 9787  hommval 9788  hodmval 9789  hfsmval 9790  hfmmval 9791  pjmfn 9938  pjmf1 9939  nmopval 10062  elcnop 10063  ellnop 10064  elunop 10079  elhmop 10080  hmopex 10082  nmfnval 10083  nlfnval 10088  elcnfn 10089  ellnfn 10090  adjval 10094  dmadjss 10099  dmadjop 10100  eigvecval 10102  eigvalval 10103  specval 10104  adjeq 10139  braval 10147  kbval 10156  cnlnadjlem4 10282  cnlnadjlem5 10283  adjbdln 10295  nmopadjlei 10300  rnbra 10320  bra11 10321  leoprf2 10340

Copyright terms: Public domain