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 )