Theorem hhcmpl

Description: Lemma used for derivation of the completeness axiom ax-hcompl from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008) (New usage is discouraged.)

	Ref	Expression
Hypotheses	hhlm.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
	hhlm.2	$$⊢D=\mathrm{IndMet}\left(U\right)$$
	hhlm.3	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
	hhcmpl.c	$$⊢F\in \mathrm{Cau}\left(D\right)\to \exists x\in \mathscr{H}F\underset{t}{⇝}\left(J\right)x$$
Assertion	hhcmpl	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$

Proof

Step	Hyp	Ref	Expression
1		hhlm.1	$$⊢U=⟨⟨{+}_{ℎ},{\cdot }_{ℎ}⟩,{norm}_{ℎ}⟩$$
2		hhlm.2	$$⊢D=\mathrm{IndMet}\left(U\right)$$
3		hhlm.3	$$⊢J=\mathrm{MetOpen}\left(D\right)$$
4		hhcmpl.c	$$⊢F\in \mathrm{Cau}\left(D\right)\to \exists x\in \mathscr{H}F\underset{t}{⇝}\left(J\right)x$$
5	4	anim1ci	$$⊢\left(F\in \mathrm{Cau}\left(D\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge \exists x\in \mathscr{H}F\underset{t}{⇝}\left(J\right)x\right)$$
6		elin	$$⊢F\in \left(\mathrm{Cau}\left(D\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\leftrightarrow \left(F\in \mathrm{Cau}\left(D\right)\wedge F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\right)$$
7		r19.42v	$$⊢\exists x\in \mathscr{H}\left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(J\right)x\right)\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge \exists x\in \mathscr{H}F\underset{t}{⇝}\left(J\right)x\right)$$
8	5 6 7	3imtr4i	$$⊢F\in \left(\mathrm{Cau}\left(D\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)\right)\to \exists x\in \mathscr{H}\left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(J\right)x\right)$$
9	1 2	hhcau	$$⊢\mathrm{Cauchy}=\mathrm{Cau}\left(D\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)$$
10	9	eleq2i	$$⊢F\in \mathrm{Cauchy}\leftrightarrow F\in \left(\mathrm{Cau}\left(D\right)\cap \left({\mathscr{H}}^{\mathbb{N}}\right)\right)$$
11	1 2 3	hhlm	$$⊢\underset{v}{⇝}={\underset{t}{⇝}\left(J\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}$$
12	11	breqi	$$⊢F\underset{v}{⇝}x\leftrightarrow F\left({\underset{t}{⇝}\left(J\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)x$$
13		vex	$$⊢x\in \mathrm{V}$$
14	13	brresi	$$⊢F\left({\underset{t}{⇝}\left(J\right)\upharpoonright }_{\left({\mathscr{H}}^{\mathbb{N}}\right)}\right)x\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(J\right)x\right)$$
15	12 14	bitri	$$⊢F\underset{v}{⇝}x\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(J\right)x\right)$$
16	15	rexbii	$$⊢\exists x\in \mathscr{H}F\underset{v}{⇝}x\leftrightarrow \exists x\in \mathscr{H}\left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge F\underset{t}{⇝}\left(J\right)x\right)$$
17	8 10 16	3imtr4i	$$⊢F\in \mathrm{Cauchy}\to \exists x\in \mathscr{H}F\underset{v}{⇝}x$$