Metamath Proof Explorer


Theorem hilcompl

Description: Lemma used for derivation of the completeness axiom ax-hcompl from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex ; the 6th would be satisfied by eqid ; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl . (Contributed by NM, 13-Sep-2007) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

Ref Expression
Hypotheses hilcompl.1
|- ~H = ( BaseSet ` U )
hilcompl.2
|- +h = ( +v ` U )
hilcompl.3
|- .h = ( .sOLD ` U )
hilcompl.4
|- .ih = ( .iOLD ` U )
hilcompl.5
|- D = ( IndMet ` U )
hilcompl.6
|- J = ( MetOpen ` D )
hilcompl.7
|- U e. CHilOLD
hilcompl.8
|- ( F e. ( Cau ` D ) -> E. x e. ~H F ( ~~>t ` J ) x )
Assertion hilcompl
|- ( F e. Cauchy -> E. x e. ~H F ~~>v x )

Proof

Step Hyp Ref Expression
1 hilcompl.1
 |-  ~H = ( BaseSet ` U )
2 hilcompl.2
 |-  +h = ( +v ` U )
3 hilcompl.3
 |-  .h = ( .sOLD ` U )
4 hilcompl.4
 |-  .ih = ( .iOLD ` U )
5 hilcompl.5
 |-  D = ( IndMet ` U )
6 hilcompl.6
 |-  J = ( MetOpen ` D )
7 hilcompl.7
 |-  U e. CHilOLD
8 hilcompl.8
 |-  ( F e. ( Cau ` D ) -> E. x e. ~H F ( ~~>t ` J ) x )
9 7 hlnvi
 |-  U e. NrmCVec
10 1 2 3 4 9 hilhhi
 |-  U = <. <. +h , .h >. , normh >.
11 10 5 6 8 hhcmpl
 |-  ( F e. Cauchy -> E. x e. ~H F ~~>v x )