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 = BaseSet U
hilcompl.2 + = + v U
hilcompl.3 = 𝑠OLD U
hilcompl.4 ih = 𝑖OLD U
hilcompl.5 D = IndMet U
hilcompl.6 J = MetOpen D
hilcompl.7 U CHil OLD
hilcompl.8 F Cau D x F t J x
Assertion hilcompl F Cauchy x F v x

Proof

Step Hyp Ref Expression
1 hilcompl.1 = BaseSet U
2 hilcompl.2 + = + v U
3 hilcompl.3 = 𝑠OLD U
4 hilcompl.4 ih = 𝑖OLD U
5 hilcompl.5 D = IndMet U
6 hilcompl.6 J = MetOpen D
7 hilcompl.7 U CHil OLD
8 hilcompl.8 F Cau D x F t J x
9 7 hlnvi U NrmCVec
10 1 2 3 4 9 hilhhi U = + norm
11 10 5 6 8 hhcmpl F Cauchy x F v x