Axiom ax-hilex 10293

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 10293, ax-hfvadd 10294, ax-hvcom 10295, ax-hvass 10296, ax-hv0cl 10297, ax-hvaddid 10298, ax-hfvmul 10299, ax-hvmulid 10300, ax-hvmulass 10301, ax-hvdistr1 10302, ax-hvdistr2 10303, ax-hvmul0 10304, ax-hfi 10371, ax-his1 10374, ax-his2 10375, ax-his3 10376, ax-his4 10377, and ax-hcompl 10496.

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 10275, axhfvadd 10276, axhvcom 10277, axhvass 10278, axhv0cl 10279, axhvaddid 10280, axhfvmul 10281, axhvmulid 10282, axhvmulass 10283, axhvdistr1 10284, axhvdistr2 10285, axhvmul0 10286, axhfi 10287, axhis1 10288, axhis2 10289, axhis3 10290, axhis4 10291, and axhcompl 10292 respectively. In that case, the theorems of the Hilbert Space Explorer will become theorems of ZFC set theory. See also the comments in axhilex 10275.

Assertion

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

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 10212	. 2 class ~H
2		cvv 2125	. 2 class _V
3	1, 2	wcel 1138	1 wff ~H e. _V

This axiom is referenced by:  hvmulex 10305  hilabl 10452  hhph 10470  shex 10502  sh 10503  hhssnm 10556  hhsssh2 10565  ocval 10578  pjmval 10663  shsumval 10702  spanval 10724  hsupval2 10725  sshjval 10745  sshjval3 10751  hosmval 10936  hommval 10937  hodmval 10938  hfsmval 10939  hfmmval 10940  pjmfn 11087  pjmf1 11088  nmopval 11211  elcnop 11212  ellnop 11213  elunop 11228  elhmop 11229  hmopex 11231  nmfnval 11232  nlfnval 11237  elcnfn 11238  ellnfn 11239  adjval 11243  dmadjss 11248  dmadjop 11249  eigvecval 11251  eigvalval 11252  specval 11253  adjeq 11288  braval 11296  kbval 11305  cnlnadjlem4 11432  cnlnadjlem5 11433  adjbdln 11445  nmopadjlei 11450  rnbra 11470  bra11 11471  leoprf2 11490

Copyright terms: Public domain