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 ) |
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 ) |