Axiom ax-hilex 8869

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 8869, ax-hfvadd 8870, ax-hvcom 8871, ax-hvass 8872, ax-hv0cl 8873, ax-hvaddid 8874, ax-hfvmul 8875, ax-hvmulid 8876, ax-hvmulass 8877, ax-hvdistr1 8878, ax-hvdistr2 8879, ax-hvmul0 8880, ax-hfi 8946, ax-his1 8949, ax-his2 8950, ax-his3 8951, ax-his4 8952, and ax-hcompl 9071.

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

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

Assertion

Ref	Expression
ax-hilex	⊢ ℋ ∈ V

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 8788	. 2 class ℋ
2		cvv 1811	. 2 class V
3	1, 2	wcel 958	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex 8881  hilabl 9027  hhph 9045  shex 9077  sh 9078  hhssnm 9131  hhsssh2 9140  ocvalt 9153  pjmvalt 9238  shsumvalt 9277  spanvalt 9299  hsupval2t 9300  sshjvalt 9320  sshjval3t 9326  hosmvalt 9511  hommvalt 9512  hodmvalt 9513  hfsmvalt 9514  hfmmvalt 9515  pjmfn 9660  pjmf1 9661  nmopvalt 9782  elcnopt 9783  ellnopt 9784  elunopt 9799  elhmopt 9800  hmopex 9802  nmfnvalt 9803  nlfnvalt 9808  elcnfnt 9809  ellnfnt 9810  adjvalt 9814  dmadjss 9819  dmadjopt 9820  eigvecvalt 9822  eigvalvalt 9823  specvalt 9824  adjeqt 9859  bravalt 9867  kbvalt 9876  cnlnadjlem4 10003  cnlnadjlem5 10004  adjbdlnt 10016  nmopadjle 10021  rnbra 10040  bra11 10041  leoprf2t 10060

Copyright terms: Public domain