Theorem axhilex 8934

Description: Derive axiom ax-hilex 8952 from Hilbert space under ZF set theory.

Before introducing the 18 axioms for Hilbert space, we first prove them as the conclusions of theorems axhilex 8934 through axhcompl 8951, using ZFC set theory only. These show that if we are given a known, fixed Hilbert space U = <.<. +h , .h >., normh>. that satisfies their hypotheses, then we can derive the Hilbert space axioms as theorems of ZFC set theory. In practice, in order to use these theorems to convert the Hilbert Space explorer to a ZFC-only subtheory, we would also have to provide definitions for the 3 (otherwise primitive) class constants +h, .h, and .ih before df-hnorm 8920 above. See also the comment in ax-hilex 8952.

Hypotheses

Ref	Expression
axhil.1	|- U = <.<. +h , .h >., normh>.
axhil.2	|- U e. CHil

Assertion

Ref	Expression
axhilex	|- H~ e. V

Proof of Theorem axhilex

Step	Hyp	Ref	Expression
1		df-hba 8921	. 2 |- H~ = (Base` <.<. +h , .h >., normh>.)
2	1	hlex 8684	1 |- H~ e. V

Syntax hints:   = wceq 997   e. wcel 999  Vcvv 1858  <.cop 2463  CHilchl 8673  H~chil 8871   +h cva 8872   .h csm 8873  normhcno 8877

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1003  ax-gen 1004  ax-8 1005  ax-10 1007  ax-11 1008  ax-12 1009  ax-13 1010  ax-14 1011  ax-17 1012  ax-4 1014  ax-5o 1016  ax-6o 1019  ax-9o 1164  ax-10o 1182  ax-16 1252  ax-11o 1260  ax-ext 1504  ax-sep 2758  ax-pow 2798  ax-un 2922

This theorem depends on definitions:  df-bi 154  df-or 231  df-an 232  df-ex 1022  df-sb 1214  df-eu 1424  df-mo 1425  df-clab 1510  df-cleq 1515  df-clel 1518  df-ne 1634  df-v 1859  df-dif 2100  df-un 2101  df-in 2102  df-ss 2104  df-nul 2332  df-pw 2454  df-sn 2464  df-pr 2465  df-uni 2558  df-fv 3255  df-hba 8921

Copyright terms: Public domain