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	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
	hilcompl.2	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
	hilcompl.3	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
	hilcompl.4	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
	hilcompl.5	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	hilcompl.6	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	hilcompl.7	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
	hilcompl.8	$$⊢F\in \mathrm{Cau}\left(D\right)\to \exists x\in \mathscr{H}F\underset{t}{⇝}\left(J\right)x$$
Assertion	hilcompl	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$

Proof

Step	Hyp	Ref	Expression
1		hilcompl.1	$$⊢\mathscr{H}=\mathrm{BaseSet}\left(U\right)$$
2		hilcompl.2	$$⊢{+}_{ℎ}={+}_v\left(U\right)$$
3		hilcompl.3	$$⊢{\cdot }_{ℎ}={\cdot }_{\mathrm{𝑠OLD}}\left(U\right)$$
4		hilcompl.4	$$⊢{\cdot }_{\mathrm{ih}}={\cdot }_{\mathrm{𝑖OLD}}\left(U\right)$$
5		hilcompl.5	$$⊢D=\mathrm{IndMet}\left(U\right)$$
6		hilcompl.6	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
7		hilcompl.7	$$⊢U\in {CHil}_{\mathrm{OLD}}$$
8		hilcompl.8	$$⊢F\in \mathrm{Cau}\left(D\right)\to \exists x\in \mathscr{H}F\underset{t}{⇝}\left(J\right)x$$
9	7	hlnvi	$$⊢U\in \mathrm{NrmCVec}$$
10	1 2 3 4 9	hilhhi	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
11	10 5 6 8	hhcmpl	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$