Theorem hcau

Description: Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in Beran p. 96. (Contributed by NM, 16-Aug-1999) (Revised by Mario Carneiro, 14-May-2014) (New usage is discouraged.)

	Ref	Expression
Assertion	hcau	$$⊢F\in \mathrm{Cauchy}\leftrightarrow \left(F:\mathbb{N}⟶\mathscr{H}\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$

Proof

Step	Hyp	Ref	Expression
1		fveq1	$$⊢f=F\to f\left(y\right)=F\left(y\right)$$
2		fveq1	$$⊢f=F\to f\left(z\right)=F\left(z\right)$$
3	1 2	oveq12d	$$⊢f=F\to f\left(y\right){-}_{ℎ}f\left(z\right)=F\left(y\right){-}_{ℎ}F\left(z\right)$$
4	3	fveq2d	$$⊢f=F\to {norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)={norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)$$
5	4	breq1d	$$⊢f=F\to \left({norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x\leftrightarrow {norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
6	5	rexralbidv	$$⊢f=F\to \left(\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x\leftrightarrow \exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
7	6	ralbidv	$$⊢f=F\to \left(\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x\leftrightarrow \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
8		df-hcau	$$⊢\mathrm{Cauchy}=\left\{f\in \left({\mathscr{H}}^{\mathbb{N}}\right)|\forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(f\left(y\right){-}_{ℎ}f\left(z\right)\right)<x\right\}$$
9	7 8	elrab2	$$⊢F\in \mathrm{Cauchy}\leftrightarrow \left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
10		ax-hilex	$$⊢\mathscr{H}\in \mathrm{V}$$
11		nnex	$$⊢\mathbb{N}\in \mathrm{V}$$
12	10 11	elmap	$$⊢F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\leftrightarrow F:\mathbb{N}⟶\mathscr{H}$$
13	12	anbi1i	$$⊢\left(F\in \left({\mathscr{H}}^{\mathbb{N}}\right)\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)\leftrightarrow \left(F:\mathbb{N}⟶\mathscr{H}\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$
14	9 13	bitri	$$⊢F\in \mathrm{Cauchy}\leftrightarrow \left(F:\mathbb{N}⟶\mathscr{H}\wedge \forall x\in {ℝ}^{+}\exists y\in \mathbb{N}\forall z\in {\mathbb{Z}}_{\ge y}{norm}_{ℎ}\left(F\left(y\right){-}_{ℎ}F\left(z\right)\right)<x\right)$$