Axiom ax-hilex 9017

Description: This is our first axiom for 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 whose properties are postulated in this axiom (which asserts that it is a set) and the axioms ax-hfvadd 9018, ax-hvcom 9019, ax-hvass 9020, ax-hv0cl 9021, ax-hvaddid 9022, ax-hfvmul 9023, ax-hvmulid 9024, ax-hvmulass 9025, ax-hvdistr1 9026, ax-hvdistr2 9027, ax-hvmul0 9028, ax-hfi 9095, ax-his1 9098, ax-his2 9099, ax-his3 9100, ax-his4 9101, and ax-hcompl 9222.

Earlier, we also developed Hilbert space directly under ZFC starting with df-hl 8456. However, when we are dealing with a fixed Hilbert space, the use of separate axioms makes the theorems somewhat less clumsy to state and prove. Compare, for example, hlcom 8466 and ax-hvcom 9019.

We could also specify the following alternate axiomatization for the Hilbert Space Explorer, consisting of a single axiom containing a new class constant H.:

ax-hil $a |- H. e. CHil $.

where we define the Hilbert space primitives in terms of H.:

df-hilbase $a |- H~ = (Base` H.) $.

df-hiladd $a |- +h = (+v` H.) $.

df-hilmul $a |- .h = (.s` H.) $.

df-hil0 $a |- 0h = (0v` H.) $.

df-hilip $a |- .ih = (.i` H.) $.

The existing axioms ax-hilex 9017 through ax-hcompl 9222 will then follow as theorems from hlex 8464, hladdf 8465, hlcom 8466, hlass 8467, hl0cl 8468, hladdid 8469, hlmulf 8470, hlmulid 8471, hlmulass 8472, hldi 8473, hldir 8474, hlmul0 8475, hlipf 8476, hlipcj 8477, hlipdir 8478, hlipass 8479, hlipgt0 8480, and hlcompl 8481 respectively. (Note that theorem hilcompl 9221 will transform hlcompl 8481 into ax-hcompl 9222.)

To eliminate the sole axiom ax-hil, we can add a definition equating H. to any class previously proved (under ZFC) to be a Hilbert space. Then ax-hil will follow as a theorem, making all theorems in the Hilbert Space Explorer become pure ZFC theorems. For example, we know that complex numbers form a Hilbert space by cnhl 8482. If we add the definition

df-hil $a |- H. = <.<. + , x. >., abs>. $.

then ax-hil will follow as a theorem by cnhl 8482, so that every theorem in the Hilbert Space Explorer will become a theorem of ZFC only, with no additional axioms.

Assertion

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

Detailed syntax breakdown of Axiom ax-hilex

Step	Hyp	Ref	Expression
1		chil 8968	. 2 class H~
2		cvv 1786	. 2 class V
3	1, 2	wcel 1105	1 wff H~ e. V

This axiom is referenced by:  hvmulex 9029  hilabl 9176  hhsm 9185  hhnm 9187  hhph 9194  hillim 9216  hilcau 9217  shex 9228  sh 9229  hhssnm 9282  ocvalt 9283  pjmvalt 9367  shsumvalt 9406  spanvalt 9428  hsupval2t 9429  sshjvalt 9449  sshjval3t 9455  hosmvalt 9642  hommvalt 9643  hodmvalt 9644  hfsmvalt 9645  hfmmvalt 9646  pjmfn 9791  pjmf1 9792  nmopvalt 9913  elcnopt 9914  ellnopt 9915  elunopt 9930  elhmopt 9931  hmopex 9933  nmfnvalt 9934  nlfnvalt 9939  elcnfnt 9940  ellnfnt 9941  adjvalt 9945  dmadjss 9950  dmadjopt 9951  eigvecvalt 9953  eigvalvalt 9954  specvalt 9955  adjeqt 9989  bravalt 9997  kbvalt 10006  cnlnadjlem4 10132  cnlnadjlem5 10133  adjbdlnt 10145  nmopadjle 10150  rnbra 10167  bra11 10168  leoprf2t 10186

Copyright terms: Public domain