Axiom ax-hilex 8824

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, ℋ, which contains objects called vectors.

The 18 axioms for a complex Hilbert space consist of ax-hilex 8824, ax-hfvadd 8825, ax-hvcom 8826, ax-hvass 8827, ax-hv0cl 8828, ax-hvaddid 8829, ax-hfvmul 8830, ax-hvmulid 8831, ax-hvmulass 8832, ax-hvdistr1 8833, ax-hvdistr2 8834, ax-hvmul0 8835, ax-hfi 8901, ax-his1 8904, ax-his2 8905, ax-his3 8906, ax-his4 8907, and ax-hcompl 9026.

The axioms specify the properties of 5 primitive symbols, ℋ, +_h, ·_h, 0_h, and ·_ih.

If can prove in ZFC set theory that a class U = ⟨⟨ +_h , ·_h ⟩, norm_h⟩ is a complex Hilbert space, i.e. that U ∈ CHil, then these axioms can be proved as theorems axhilex 8806, axhfvadd 8807, axhvcom 8808, axhvass 8809, axhv0cl 8810, axhvaddid 8811 , axhfvmul 8812, axhvmulid 8813, axhvmulass 8814, axhvdistr1 8815, axhvdistr2 8816 , axhvmul0 8817, axhfi 8818, axhis1 8819, axhis2 8820, axhis3 8821, axhis4 8822, and axhcompl 8823 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 8806.

Assertion

Ref	Expression
ax-hilex	⊢ ℋ ∈ V

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 8743	. 2 class ℋ
2		cvv 1808	. 2 class V
3	1, 2	wcel 957	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex 8836  hilabl 8982  hhph 9000  shex 9032  sh 9033  hhssnm 9086  hhsssh2 9095  ocvalt 9108  pjmvalt 9193  shsumvalt 9232  spanvalt 9254  hsupval2t 9255  sshjvalt 9275  sshjval3t 9281  hosmvalt 9468  hommvalt 9469  hodmvalt 9470  hfsmvalt 9471  hfmmvalt 9472  pjmfn 9617  pjmf1 9618  nmopvalt 9739  elcnopt 9740  ellnopt 9741  elunopt 9756  elhmopt 9757  hmopex 9759  nmfnvalt 9760  nlfnvalt 9765  elcnfnt 9766  ellnfnt 9767  adjvalt 9771  dmadjss 9776  dmadjopt 9777  eigvecvalt 9779  eigvalvalt 9780  specvalt 9781  adjeqt 9816  bravalt 9824  kbvalt 9833  cnlnadjlem4 9959  cnlnadjlem5 9960  adjbdlnt 9972  nmopadjle 9977  rnbra 9996  bra11 9997  leoprf2t 10016

Copyright terms: Public domain