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 :

ax-hil $a CHil $.

where we define the Hilbert space primitives in terms of :

df-hilbase $a Base $.

df-hiladd $a $.

df-hilmul $a $.

df-hil0 $a $.

df-hilip $a $.

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 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 $.

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.