Axiom ax-hilex 8808

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 8808, ax-hfvadd 8809, ax-hvcom 8810, ax-hvass 8811, ax-hv0cl 8812, ax-hvaddid 8813, ax-hfvmul 8814, ax-hvmulid 8815, ax-hvmulass 8816, ax-hvdistr1 8817, ax-hvdistr2 8818, ax-hvmul0 8819, ax-hfi 8885, ax-his1 8888, ax-his2 8889, ax-his3 8890, ax-his4 8891, and ax-hcompl 9010.

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

If 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 8790, axhfvadd 8791, axhvcom 8792, axhvass 8793, axhv0cl 8794, axhvaddid 8795 , axhfvmul 8796, axhvmulid 8797, axhvmulass 8798, axhvdistr1 8799, axhvdistr2 8800 , axhvmul0 8801, axhfi 8802, axhis1 8803, axhis2 8804, axhis3 8805, axhis4 8806, and axhcompl 8807 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 8790.

Assertion

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

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 8727	. 2 class H~
2		cvv 1807	. 2 class V
3	1, 2	wcel 956	1 wff H~ e. V

This axiom is referenced by:  hvmulex 8820  hilabl 8966  hhph 8984  shex 9016  sh 9017  hhssnm 9070  hhsssh2 9079  ocvalt 9092  pjmvalt 9176  shsumvalt 9215  spanvalt 9237  hsupval2t 9238  sshjvalt 9258  sshjval3t 9264  hosmvalt 9451  hommvalt 9452  hodmvalt 9453  hfsmvalt 9454  hfmmvalt 9455  pjmfn 9600  pjmf1 9601  nmopvalt 9722  elcnopt 9723  ellnopt 9724  elunopt 9739  elhmopt 9740  hmopex 9742  nmfnvalt 9743  nlfnvalt 9748  elcnfnt 9749  ellnfnt 9750  adjvalt 9754  dmadjss 9759  dmadjopt 9760  eigvecvalt 9762  eigvalvalt 9763  specvalt 9764  adjeqt 9798  bravalt 9806  kbvalt 9815  cnlnadjlem4 9941  cnlnadjlem5 9942  adjbdlnt 9954  nmopadjle 9959  rnbra 9978  bra11 9979  leoprf2t 9998

Copyright terms: Public domain