Metamath Proof Explorer

Theorem iscau

Description: Express the property " F is a Cauchy sequence of metric D ". Part of Definition 1.4-3 of Kreyszig p. 28. The condition F C_ ( CC X. X ) allows us to use objects more general than sequences when convenient; see the comment in df-lm . (Contributed by NM, 7-Dec-2006) (Revised by Mario Carneiro, 14-Nov-2013)

Ref Expression
Assertion iscau ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{F}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right)\right)$

Proof

Step Hyp Ref Expression
1 caufval ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \mathrm{Cau}\left({D}\right)=\left\{{f}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)|\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{f}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{f}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right\}$
2 1 eleq2d ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔{F}\in \left\{{f}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)|\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{f}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{f}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right\}\right)$
3 reseq1 ${⊢}{f}={F}\to {{f}↾}_{{ℤ}_{\ge {k}}}={{F}↾}_{{ℤ}_{\ge {k}}}$
4 eqidd ${⊢}{f}={F}\to {ℤ}_{\ge {k}}={ℤ}_{\ge {k}}$
5 fveq1 ${⊢}{f}={F}\to {f}\left({k}\right)={F}\left({k}\right)$
6 5 oveq1d ${⊢}{f}={F}\to {f}\left({k}\right)\mathrm{ball}\left({D}\right){x}={F}\left({k}\right)\mathrm{ball}\left({D}\right){x}$
7 3 4 6 feq123d ${⊢}{f}={F}\to \left(\left({{f}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{f}\left({k}\right)\mathrm{ball}\left({D}\right){x}↔\left({{F}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{F}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right)$
8 7 rexbidv ${⊢}{f}={F}\to \left(\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{f}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{f}\left({k}\right)\mathrm{ball}\left({D}\right){x}↔\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{F}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right)$
9 8 ralbidv ${⊢}{f}={F}\to \left(\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{f}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{f}\left({k}\right)\mathrm{ball}\left({D}\right){x}↔\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{F}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right)$
10 9 elrab ${⊢}{F}\in \left\{{f}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)|\forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{f}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{f}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right\}↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{F}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right)$
11 2 10 syl6bb ${⊢}{D}\in \mathrm{\infty Met}\left({X}\right)\to \left({F}\in \mathrm{Cau}\left({D}\right)↔\left({F}\in \left({X}{↑}_{𝑝𝑚}ℂ\right)\wedge \forall {x}\in {ℝ}^{+}\phantom{\rule{.4em}{0ex}}\exists {k}\in ℤ\phantom{\rule{.4em}{0ex}}\left({{F}↾}_{{ℤ}_{\ge {k}}}\right):{ℤ}_{\ge {k}}⟶{F}\left({k}\right)\mathrm{ball}\left({D}\right){x}\right)\right)$