Axiom ax-hilex 8790

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 8790, ax-hfvadd 8791, ax-hvcom 8792, ax-hvass 8793, ax-hv0cl 8794, ax-hvaddid 8795, ax-hfvmul 8796, ax-hvmulid 8797, ax-hvmulass 8798, ax-hvdistr1 8799, ax-hvdistr2 8800, ax-hvmul0 8801, ax-hfi 8867, ax-his1 8870, ax-his2 8871, ax-his3 8872, ax-his4 8873, and ax-hcompl 8992.

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 (future), axhfvadd (future), axhvcom (future), axhvass (future), axhv0cl (future), axhvaddid (future) , axhfvmul (future), axhvmulid (future), axhvmulass (future), axhvdistr1 (future), axhvdistr2 (future) , axhvmul0 (future), axhfi (future), axhis1 (future), axhis2 (future), axhis3 (future), axhis4 (future), and axhcompl (future) respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex (future).

Assertion

Ref	Expression
ax-hilex	⊢ ℋ ∈ V

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 8727	. 2 class ℋ
2		cvv 1802	. 2 class V
3	1, 2	wcel 955	1 wff ℋ ∈ V

This axiom is referenced by:  hvmulex 8802  hilabl 8948  hhph 8966  shex 8998  sh 8999  hhssnm 9052  ocvalt 9069  pjmvalt 9153  shsumvalt 9192  spanvalt 9214  hsupval2t 9215  sshjvalt 9235  sshjval3t 9241  hosmvalt 9428  hommvalt 9429  hodmvalt 9430  hfsmvalt 9431  hfmmvalt 9432  pjmfn 9577  pjmf1 9578  nmopvalt 9699  elcnopt 9700  ellnopt 9701  elunopt 9716  elhmopt 9717  hmopex 9719  nmfnvalt 9720  nlfnvalt 9725  elcnfnt 9726  ellnfnt 9727  adjvalt 9731  dmadjss 9736  dmadjopt 9737  eigvecvalt 9739  eigvalvalt 9740  specvalt 9741  adjeqt 9775  bravalt 9783  kbvalt 9792  cnlnadjlem4 9918  cnlnadjlem5 9919  adjbdlnt 9931  nmopadjle 9936  rnbra 9953  bra11 9954  leoprf2t 9972

Copyright terms: Public domain