Axiom ax-hilex 8864

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 8864, ax-hfvadd 8865, ax-hvcom 8866, ax-hvass 8867, ax-hv0cl 8868, ax-hvaddid 8869, ax-hfvmul 8870, ax-hvmulid 8871, ax-hvmulass 8872, ax-hvdistr1 8873, ax-hvdistr2 8874, ax-hvmul0 8875, ax-hfi 8941, ax-his1 8944, ax-his2 8945, ax-his3 8946, ax-his4 8947, and ax-hcompl 9066.

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 8846, axhfvadd 8847, axhvcom 8848, axhvass 8849, axhv0cl 8850, axhvaddid 8851 , axhfvmul 8852, axhvmulid 8853, axhvmulass 8854, axhvdistr1 8855, axhvdistr2 8856 , axhvmul0 8857, axhfi 8858, axhis1 8859, axhis2 8860, axhis3 8861, axhis4 8862, and axhcompl 8863 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 8846.

Assertion

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

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 8783	. 2 class H~
2		cvv 1814	. 2 class V
3	1, 2	wcel 960	1 wff H~ e. V

This axiom is referenced by:  hvmulex 8876  hilabl 9022  hhph 9040  shex 9072  sh 9073  hhssnm 9126  hhsssh2 9135  ocvalt 9148  pjmvalt 9233  shsumvalt 9272  spanvalt 9294  hsupval2t 9295  sshjvalt 9315  sshjval3t 9321  hosmvalt 9506  hommvalt 9507  hodmvalt 9508  hfsmvalt 9509  hfmmvalt 9510  pjmfn 9655  pjmf1 9656  nmopvalt 9777  elcnopt 9778  ellnopt 9779  elunopt 9794  elhmopt 9795  hmopex 9797  nmfnvalt 9798  nlfnvalt 9803  elcnfnt 9804  ellnfnt 9805  adjvalt 9809  dmadjss 9814  dmadjopt 9815  eigvecvalt 9817  eigvalvalt 9818  specvalt 9819  adjeqt 9854  bravalt 9862  kbvalt 9871  cnlnadjlem4 9998  cnlnadjlem5 9999  adjbdlnt 10011  nmopadjle 10016  rnbra 10035  bra11 10036  leoprf2t 10055

Copyright terms: Public domain