h2hcau

Description: The Cauchy sequences of Hilbert space. (Contributed by NM, 6-Jun-2008) (Revised by Mario Carneiro, 13-May-2014) (New usage is discouraged.)

	Ref	Expression
Hypotheses	h2hc.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
	h2hc.2	$⊢ U \in NrmCVec$
	h2hc.3	$⊢ ℋ = BaseSet (U)$
	h2hc.4	$⊢ D = IndMet (U)$
Assertion	h2hcau	$⊢ Cauchy = Cau (D) \cap (ℋ^{ℕ})$

Proof

Step	Hyp	Ref	Expression
1		h2hc.1	$⊢ U = ⟨⟨+_{ℎ}, \cdot_{ℎ}⟩, {norm}_{ℎ}⟩$
2		h2hc.2	$⊢ U \in NrmCVec$
3		h2hc.3	$⊢ ℋ = BaseSet (U)$
4		h2hc.4	$⊢ D = IndMet (U)$
5		df-rab	$⊢ \{f \in (ℋ^{ℕ}) \| \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x\} = \{f \| (f \in (ℋ^{ℕ}) \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)\}$
6		df-hcau	$⊢ Cauchy = \{f \in (ℋ^{ℕ}) \| \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x\}$
7		elin	$⊢ f \in (Cau (D) \cap (ℋ^{ℕ})) \leftrightarrow (f \in Cau (D) \land f \in (ℋ^{ℕ}))$
8		ancom	$⊢ (f \in Cau (D) \land f \in (ℋ^{ℕ})) \leftrightarrow (f \in (ℋ^{ℕ}) \land f \in Cau (D))$
9	3	hlex	$⊢ ℋ \in V$
10		nnex	$⊢ ℕ \in V$
11	9 10	elmap	$⊢ f \in (ℋ^{ℕ}) \leftrightarrow f : ℕ ⟶ ℋ$
12		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
13	3 4	imsxmet	$⊢ U \in NrmCVec \to D \in ∞Met (ℋ)$
14	2 13	mp1i	$⊢ f : ℕ ⟶ ℋ \to D \in ∞Met (ℋ)$
15		1zzd	$⊢ f : ℕ ⟶ ℋ \to 1 \in ℤ$
16		eqidd	$⊢ (f : ℕ ⟶ ℋ \land k \in ℕ) \to f (k) = f (k)$
17		eqidd	$⊢ (f : ℕ ⟶ ℋ \land j \in ℕ) \to f (j) = f (j)$
18		id	$⊢ f : ℕ ⟶ ℋ \to f : ℕ ⟶ ℋ$
19	12 14 15 16 17 18	iscauf	$⊢ f : ℕ ⟶ ℋ \to (f \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} f (j) D f (k) < x)$
20		ffvelcdm	$⊢ (f : ℕ ⟶ ℋ \land j \in ℕ) \to f (j) \in ℋ$
21	20	adantr	$⊢ ((f : ℕ ⟶ ℋ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to f (j) \in ℋ$
22		eluznn	$⊢ (j \in ℕ \land k \in ℤ_{\geq j}) \to k \in ℕ$
23		ffvelcdm	$⊢ (f : ℕ ⟶ ℋ \land k \in ℕ) \to f (k) \in ℋ$
24	22 23	sylan2	$⊢ (f : ℕ ⟶ ℋ \land (j \in ℕ \land k \in ℤ_{\geq j})) \to f (k) \in ℋ$
25	24	anassrs	$⊢ ((f : ℕ ⟶ ℋ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to f (k) \in ℋ$
26	1 2 3 4	h2hmetdval	$⊢ (f (j) \in ℋ \land f (k) \in ℋ) \to f (j) D f (k) = {norm}_{ℎ} (f (j) -_{ℎ} f (k))$
27	21 25 26	syl2anc	$⊢ ((f : ℕ ⟶ ℋ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to f (j) D f (k) = {norm}_{ℎ} (f (j) -_{ℎ} f (k))$
28	27	breq1d	$⊢ ((f : ℕ ⟶ ℋ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (f (j) D f (k) < x \leftrightarrow {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
29	28	ralbidva	$⊢ (f : ℕ ⟶ ℋ \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} f (j) D f (k) < x \leftrightarrow \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
30	29	rexbidva	$⊢ f : ℕ ⟶ ℋ \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} f (j) D f (k) < x \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
31	30	ralbidv	$⊢ f : ℕ ⟶ ℋ \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} f (j) D f (k) < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
32	19 31	bitrd	$⊢ f : ℕ ⟶ ℋ \to (f \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
33	11 32	sylbi	$⊢ f \in (ℋ^{ℕ}) \to (f \in Cau (D) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
34	33	pm5.32i	$⊢ (f \in (ℋ^{ℕ}) \land f \in Cau (D)) \leftrightarrow (f \in (ℋ^{ℕ}) \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
35	7 8 34	3bitri	$⊢ f \in (Cau (D) \cap (ℋ^{ℕ})) \leftrightarrow (f \in (ℋ^{ℕ}) \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)$
36	35	eqabi	$⊢ Cau (D) \cap (ℋ^{ℕ}) = \{f \| (f \in (ℋ^{ℕ}) \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} {norm}_{ℎ} (f (j) -_{ℎ} f (k)) < x)\}$
37	5 6 36	3eqtr4i	$⊢ Cauchy = Cau (D) \cap (ℋ^{ℕ})$

Metamath Proof Explorer

Theorem h2hcau

Proof