P. 253 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25201-25300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscmet2 25201	A metric 𝐷 is complete iff all Cauchy sequences converge to a point in the space. The proof uses countable choice. Part of Definition 1.4-3 of [Kreyszig] p. 28. (Contributed by NM, 7-Sep-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘𝐽)))
Theorem	cfilresi 25202	A Cauchy filter on a metric subspace extends to a Cauchy filter in the larger space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))) → (𝑋filGen𝐹) ∈ (CauFil‘𝐷))
Theorem	cfilres 25203	Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ↾t 𝑌) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	caussi 25204	Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ⊆ (Cau‘𝐷))
Theorem	causs 25205	Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	equivcfil 25206*	If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), all the 𝐷-Cauchy filters are also 𝐶-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → (CauFil‘𝐷) ⊆ (CauFil‘𝐶))
Theorem	equivcau 25207*	If the metric 𝐷 is "strongly finer" than 𝐶 (meaning that there is a positive real constant 𝑅 such that 𝐶(𝑥, 𝑦) ≤ 𝑅 · 𝐷(𝑥, 𝑦)), all the 𝐷-Cauchy sequences are also 𝐶-Cauchy. (Using this theorem twice in each direction states that if two metrics are strongly equivalent, then they have the same Cauchy sequences.) (Contributed by Mario Carneiro, 14-Sep-2015.)
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    ⇒   ⊢ (𝜑 → (Cau‘𝐷) ⊆ (Cau‘𝐶))
Theorem	lmle 25208*	If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. (Contributed by NM, 23-Dec-2007.) (Proof shortened by Mario Carneiro, 1-May-2014.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑄 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝑄𝐷(𝐹‘𝑘)) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (𝑄𝐷𝑃) ≤ 𝑅)
Theorem	nglmle 25209*	If the norm of each member of a converging sequence is less than or equal to a given amount, so is the norm of the convergence value. (Contributed by NM, 25-Dec-2007.) (Revised by AV, 16-Oct-2021.)
⊢ 𝑋 = (Base‘𝐺)    &   ⊢ 𝐷 = ((dist‘𝐺) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ (𝜑 → 𝐺 ∈ NrmGrp)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ*)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑁‘(𝐹‘𝑘)) ≤ 𝑅)    ⇒   ⊢ (𝜑 → (𝑁‘𝑃) ≤ 𝑅)
Theorem	lmclim 25210	Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 9-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑍 ⊆ dom 𝐹) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (ℂ ↑pm ℂ) ∧ 𝐹 ⇝ 𝑃)))
Theorem	lmclimf 25211	Relate a limit on the metric space of complex numbers to our complex number limit notation. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (TopOpen‘ℂfld)    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶ℂ) → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ 𝐹 ⇝ 𝑃))
Theorem	metelcls 25212*	A point belongs to the closure of a subset iff there is a sequence in the subset converging to it. Theorem 1.4-6(a) of [Kreyszig] p. 30. This proof uses countable choice ax-cc 10395. The statement can be generalized to first-countable spaces, not just metrizable spaces. (Contributed by NM, 8-Nov-2007.) (Proof shortened by Mario Carneiro, 1-May-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑆 ⊆ 𝑋)    ⇒   ⊢ (𝜑 → (𝑃 ∈ ((cls‘𝐽)‘𝑆) ↔ ∃𝑓(𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑃)))
Theorem	metcld 25213*	A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30. (Contributed by NM, 11-Nov-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ∀𝑥∀𝑓((𝑓:ℕ⟶𝑆 ∧ 𝑓(⇝𝑡‘𝐽)𝑥) → 𝑥 ∈ 𝑆)))
Theorem	metcld2 25214	A subset of a metric space is closed iff every convergent sequence on it converges to a point in the subset. Theorem 1.4-6(b) of [Kreyszig] p. 30. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑆 ⊆ 𝑋) → (𝑆 ∈ (Clsd‘𝐽) ↔ ((⇝𝑡‘𝐽) “ (𝑆 ↑m ℕ)) ⊆ 𝑆))
Theorem	caubl 25215*	Sufficient condition to ensure a sequence of nested balls is Cauchy. (Contributed by Mario Carneiro, 18-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))    &   ⊢ (𝜑 → ∀𝑟 ∈ ℝ+ ∃𝑛 ∈ ℕ (2nd ‘(𝐹‘𝑛)) < 𝑟)    ⇒   ⊢ (𝜑 → (1st ∘ 𝐹) ∈ (Cau‘𝐷))
Theorem	caublcls 25216*	The convergent point of a sequence of nested balls is in the closures of any of the balls (i.e. it is in the intersection of the closures). Indeed, it is the only point in the intersection because a metric space is Hausdorff, but we don't prove this here. (Contributed by Mario Carneiro, 21-Jan-2014.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝐹‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝐹‘𝑛)))    &   ⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝜑 ∧ (1st ∘ 𝐹)(⇝𝑡‘𝐽)𝑃 ∧ 𝐴 ∈ ℕ) → 𝑃 ∈ ((cls‘𝐽)‘((ball‘𝐷)‘(𝐹‘𝐴))))
Theorem	metcnp4 25217*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous at point 𝑃. Theorem 14-4.3 of [Gleason] p. 240. (Contributed by NM, 17-May-2007.) (Revised by Mario Carneiro, 4-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 ∈ ((𝐽 CnP 𝐾)‘𝑃) ↔ (𝐹:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ 𝑓(⇝𝑡‘𝐽)𝑃) → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑃)))))
Theorem	metcn4 25218*	Two ways to say a mapping from metric 𝐶 to metric 𝐷 is continuous. Theorem 10.3 of [Munkres] p. 128. (Contributed by NM, 13-Jun-2007.) (Revised by Mario Carneiro, 4-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐶)    &   ⊢ 𝐾 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐶 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑌))    &   ⊢ (𝜑 → 𝐹:𝑋⟶𝑌)    ⇒   ⊢ (𝜑 → (𝐹 ∈ (𝐽 Cn 𝐾) ↔ ∀𝑓(𝑓:ℕ⟶𝑋 → ∀𝑥(𝑓(⇝𝑡‘𝐽)𝑥 → (𝐹 ∘ 𝑓)(⇝𝑡‘𝐾)(𝐹‘𝑥)))))
Theorem	iscmet3i 25219*	Properties that determine a complete metric space. (Contributed by NM, 15-Apr-2007.) (Revised by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ 𝐷 ∈ (Met‘𝑋)    &   ⊢ ((𝑓 ∈ (Cau‘𝐷) ∧ 𝑓:ℕ⟶𝑋) → 𝑓 ∈ dom (⇝𝑡‘𝐽))    ⇒   ⊢ 𝐷 ∈ (CMet‘𝑋)
Theorem	lmcau 25220	Every convergent sequence in a metric space is a Cauchy sequence. Theorem 1.4-5 of [Kreyszig] p. 28. (Contributed by NM, 29-Jan-2008.) (Proof shortened by Mario Carneiro, 5-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (∞Met‘𝑋) → dom (⇝𝑡‘𝐽) ⊆ (Cau‘𝐷))
Theorem	flimcfil 25221	Every convergent filter in a metric space is a Cauchy filter. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐴 ∈ (𝐽 fLim 𝐹)) → 𝐹 ∈ (CauFil‘𝐷))
Theorem	metsscmetcld 25222	A complete subspace of a metric space is closed in the parent space. Formerly part of proof for cmetss 25223. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 9-Oct-2022.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (Met‘𝑋) ∧ (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌)) → 𝑌 ∈ (Clsd‘𝐽))
Theorem	cmetss 25223	A subspace of a complete metric space is complete iff it is closed in the parent space. Theorem 1.4-7 of [Kreyszig] p. 30. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 9-Oct-2022.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (𝐷 ∈ (CMet‘𝑋) → ((𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌) ↔ 𝑌 ∈ (Clsd‘𝐽)))
Theorem	equivcmet 25224*	If two metrics are strongly equivalent, one is complete iff the other is. Unlike equivcau 25207, metss2 24407, this theorem does not have a one-directional form - it is possible for a metric 𝐶 that is strongly finer than the complete metric 𝐷 to be incomplete and vice versa. Consider 𝐷 = the metric on ℝ induced by the usual homeomorphism from (0, 1) against the usual metric 𝐶 on ℝ and against the discrete metric 𝐸 on ℝ. Then both 𝐶 and 𝐸 are complete but 𝐷 is not, and 𝐶 is strongly finer than 𝐷, which is strongly finer than 𝐸. (Contributed by Mario Carneiro, 15-Sep-2015.)
⊢ (𝜑 → 𝐶 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝑆 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐶𝑦) ≤ (𝑅 · (𝑥𝐷𝑦)))    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑋)) → (𝑥𝐷𝑦) ≤ (𝑆 · (𝑥𝐶𝑦)))    ⇒   ⊢ (𝜑 → (𝐶 ∈ (CMet‘𝑋) ↔ 𝐷 ∈ (CMet‘𝑋)))
Theorem	relcmpcmet 25225*	If 𝐷 is a metric space such that all the balls of some fixed size are relatively compact, then 𝐷 is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑋) → (𝐽 ↾t ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑅))) ∈ Comp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
Theorem	cmpcmet 25226	A compact metric space is complete. One half of heibor 37822. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐽 ∈ Comp)    ⇒   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))
Theorem	cfilucfil3 25227	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋)) → ((𝐶 ∈ (Fil‘𝑋) ∧ 𝐶 ∈ (CauFilu‘(metUnif‘𝐷))) ↔ 𝐶 ∈ (CauFil‘𝐷)))
Theorem	cfilucfil4 25228	Given a metric 𝐷 and a uniform structure generated by that metric, Cauchy filter bases on that uniform structure are exactly the Cauchy filters for the metric. (Contributed by Thierry Arnoux, 15-Dec-2017.) (Revised by Thierry Arnoux, 11-Feb-2018.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (∞Met‘𝑋) ∧ 𝐶 ∈ (Fil‘𝑋)) → (𝐶 ∈ (CauFilu‘(metUnif‘𝐷)) ↔ 𝐶 ∈ (CauFil‘𝐷)))
Theorem	cncmet 25229	The set of complex numbers is a complete metric space under the absolute value metric. (Contributed by NM, 20-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐷 = (abs ∘ − )    ⇒   ⊢ 𝐷 ∈ (CMet‘ℂ)
Theorem	recmet 25230	The real numbers are a complete metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 12-Sep-2015.)
⊢ ((abs ∘ − ) ↾ (ℝ × ℝ)) ∈ (CMet‘ℝ)
12.5.6  Baire's Category Theorem
Theorem	bcthlem1 25231*	Lemma for bcth 25236. Substitutions for the function 𝐹. (Contributed by Mario Carneiro, 9-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    ⇒   ⊢ ((𝜑 ∧ (𝐴 ∈ ℕ ∧ 𝐵 ∈ (𝑋 × ℝ+))) → (𝐶 ∈ (𝐴𝐹𝐵) ↔ (𝐶 ∈ (𝑋 × ℝ+) ∧ (2nd ‘𝐶) < (1 / 𝐴) ∧ ((cls‘𝐽)‘((ball‘𝐷)‘𝐶)) ⊆ (((ball‘𝐷)‘𝐵) ∖ (𝑀‘𝐴)))))
Theorem	bcthlem2 25232*	Lemma for bcth 25236. The balls in the sequence form an inclusion chain. (Contributed by Mario Carneiro, 7-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))    ⇒   ⊢ (𝜑 → ∀𝑛 ∈ ℕ ((ball‘𝐷)‘(𝑔‘(𝑛 + 1))) ⊆ ((ball‘𝐷)‘(𝑔‘𝑛)))
Theorem	bcthlem3 25233*	Lemma for bcth 25236. The limit point of the centers in the sequence is in the intersection of every ball in the sequence. (Contributed by Mario Carneiro, 7-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))    ⇒   ⊢ ((𝜑 ∧ (1st ∘ 𝑔)(⇝𝑡‘𝐽)𝑥 ∧ 𝐴 ∈ ℕ) → 𝑥 ∈ ((ball‘𝐷)‘(𝑔‘𝐴)))
Theorem	bcthlem4 25234*	Lemma for bcth 25236. Given any open ball (𝐶(ball‘𝐷)𝑅) as starting point (and in particular, a ball in int(∪ ran 𝑀)), the limit point 𝑥 of the centers of the induced sequence of balls 𝑔 is outside ∪ ran 𝑀. Note that a set 𝐴 has empty interior iff every nonempty open set 𝑈 contains points outside 𝐴, i.e. (𝑈 ∖ 𝐴) ≠ ∅. (Contributed by Mario Carneiro, 7-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑋)    &   ⊢ (𝜑 → 𝑔:ℕ⟶(𝑋 × ℝ+))    &   ⊢ (𝜑 → (𝑔‘1) = ⟨𝐶, 𝑅⟩)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ (𝑔‘(𝑘 + 1)) ∈ (𝑘𝐹(𝑔‘𝑘)))    ⇒   ⊢ (𝜑 → ((𝐶(ball‘𝐷)𝑅) ∖ ∪ ran 𝑀) ≠ ∅)
Theorem	bcthlem5 25235*	Lemma for bcth 25236. The proof makes essential use of the Axiom of Dependent Choice axdc4uz 13956, which in the form used here accepts a "selection" function 𝐹 from each element of 𝐾 to a nonempty subset of 𝐾, and the result function 𝑔 maps 𝑔(𝑛 + 1) to an element of 𝐹(𝑛, 𝑔(𝑛)). The trick here is thus in the choice of 𝐹 and 𝐾: we let 𝐾 be the set of all tagged nonempty open sets (tagged here meaning that we have a point and an open set, in an ordered pair), and 𝐹(𝑘, ⟨𝑥, 𝑧⟩) gives the set of all balls of size less than 1 / 𝑘, tagged by their centers, whose closures fit within the given open set 𝑧 and miss 𝑀(𝑘). Since 𝑀(𝑘) is closed, 𝑧 ∖ 𝑀(𝑘) is open and also nonempty, since 𝑧 is nonempty and 𝑀(𝑘) has empty interior. Then there is some ball contained in it, and hence our function 𝐹 is valid (it never maps to the empty set). Now starting at a point in the interior of ∪ ran 𝑀, DC gives us the function 𝑔 all whose elements are constrained by 𝐹 acting on the previous value. (This is all proven in this lemma.) Now 𝑔 is a sequence of tagged open balls, forming an inclusion chain (see bcthlem2 25232) and whose sizes tend to zero, since they are bounded above by 1 / 𝑘. Thus, the centers of these balls form a Cauchy sequence, and converge to a point 𝑥 (see bcthlem4 25234). Since the inclusion chain also ensures the closure of each ball is in the previous ball, the point 𝑥 must be in all these balls (see bcthlem3 25233) and hence misses each 𝑀(𝑘), contradicting the fact that 𝑥 is in the interior of ∪ ran 𝑀 (which was the starting point). (Contributed by Mario Carneiro, 6-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ 𝐹 = (𝑘 ∈ ℕ, 𝑧 ∈ (𝑋 × ℝ+) ↦ {⟨𝑥, 𝑟⟩ ∣ ((𝑥 ∈ 𝑋 ∧ 𝑟 ∈ ℝ+) ∧ (𝑟 < (1 / 𝑘) ∧ ((cls‘𝐽)‘(𝑥(ball‘𝐷)𝑟)) ⊆ (((ball‘𝐷)‘𝑧) ∖ (𝑀‘𝑘))))})    &   ⊢ (𝜑 → 𝑀:ℕ⟶(Clsd‘𝐽))    &   ⊢ (𝜑 → ∀𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) = ∅)    ⇒   ⊢ (𝜑 → ((int‘𝐽)‘∪ ran 𝑀) = ∅)
Theorem	bcth 25236*	Baire's Category Theorem. If a nonempty metric space is complete, it is nonmeager in itself. In other words, no open set in the metric space can be the countable union of rare closed subsets (where rare means having a closure with empty interior), so some subset 𝑀‘𝑘 must have a nonempty interior. Theorem 4.7-2 of [Kreyszig] p. 247. (The terminology "meager" and "nonmeager" is used by Kreyszig to replace Baire's "of the first category" and "of the second category." The latter terms are going out of favor to avoid confusion with category theory.) See bcthlem5 25235 for an overview of the proof. (Contributed by NM, 28-Oct-2007.) (Proof shortened by Mario Carneiro, 6-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶(Clsd‘𝐽) ∧ ((int‘𝐽)‘∪ ran 𝑀) ≠ ∅) → ∃𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)
Theorem	bcth2 25237*	Baire's Category Theorem, version 2: If countably many closed sets cover 𝑋, then one of them has an interior. (Contributed by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ (((𝐷 ∈ (CMet‘𝑋) ∧ 𝑋 ≠ ∅) ∧ (𝑀:ℕ⟶(Clsd‘𝐽) ∧ ∪ ran 𝑀 = 𝑋)) → ∃𝑘 ∈ ℕ ((int‘𝐽)‘(𝑀‘𝑘)) ≠ ∅)
Theorem	bcth3 25238*	Baire's Category Theorem, version 3: The intersection of countably many dense open sets is dense. (Contributed by Mario Carneiro, 10-Jan-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝑀:ℕ⟶𝐽 ∧ ∀𝑘 ∈ ℕ ((cls‘𝐽)‘(𝑀‘𝑘)) = 𝑋) → ((cls‘𝐽)‘∩ ran 𝑀) = 𝑋)
12.5.7  Banach spaces and subcomplex Hilbert spaces
Syntax	ccms 25239	Extend class notation with the class of complete metric spaces.
class CMetSp
Syntax	cbn 25240	Extend class notation with the class of Banach spaces.
class Ban
Syntax	chl 25241	Extend class notation with the class of subcomplex Hilbert spaces.
class ℂHil
Definition	df-cms 25242*	Define the class of complete metric spaces. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ CMetSp = {𝑤 ∈ MetSp ∣ [(Base‘𝑤) / 𝑏]((dist‘𝑤) ↾ (𝑏 × 𝑏)) ∈ (CMet‘𝑏)}
Definition	df-bn 25243	Define the class of all Banach spaces. A Banach space is a normed vector space such that both the vector space and the scalar field are complete under their respective norm-induced metrics. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ Ban = {𝑤 ∈ (NrmVec ∩ CMetSp) ∣ (Scalar‘𝑤) ∈ CMetSp}
Definition	df-hl 25244	Define the class of all subcomplex Hilbert spaces. A subcomplex Hilbert space is a Banach space which is also an inner product space over a subfield of the field of complex numbers closed under square roots of nonnegative reals. (Contributed by Steve Rodriguez, 28-Apr-2007.)
⊢ ℂHil = (Ban ∩ ℂPreHil)
Theorem	isbn 25245	A Banach space is a normed vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ Ban ↔ (𝑊 ∈ NrmVec ∧ 𝑊 ∈ CMetSp ∧ 𝐹 ∈ CMetSp))
Theorem	bnsca 25246	The scalar field of a Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ (𝑊 ∈ Ban → 𝐹 ∈ CMetSp)
Theorem	bnnvc 25247	A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmVec)
Theorem	bnnlm 25248	A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmMod)
Theorem	bnngp 25249	A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmGrp)
Theorem	bnlmod 25250	A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod)
Theorem	bncms 25251	A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp)
Theorem	iscms 25252	A complete metric space is a metric space with a complete metric. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ CMetSp ↔ (𝑀 ∈ MetSp ∧ 𝐷 ∈ (CMet‘𝑋)))
Theorem	cmscmet 25253	The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ CMetSp → 𝐷 ∈ (CMet‘𝑋))
Theorem	bncmet 25254	The induced metric on Banach space is complete. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ Ban → 𝐷 ∈ (CMet‘𝑋))
Theorem	cmsms 25255	A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝐺 ∈ CMetSp → 𝐺 ∈ MetSp)
Theorem	cmspropd 25256	Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp))
Theorem	cmssmscld 25257	The restriction of a metric space is closed if it is complete. (Contributed by AV, 9-Oct-2022.)
⊢ 𝐾 = (𝑀 ↾s 𝐴)    &   ⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐽 = (TopOpen‘𝑀)    ⇒   ⊢ ((𝑀 ∈ MetSp ∧ 𝐴 ⊆ 𝑋 ∧ 𝐾 ∈ CMetSp) → 𝐴 ∈ (Clsd‘𝐽))
Theorem	cmsss 25258	The restriction of a complete metric space is complete iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐾 = (𝑀 ↾s 𝐴)    &   ⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐽 = (TopOpen‘𝑀)    ⇒   ⊢ ((𝑀 ∈ CMetSp ∧ 𝐴 ⊆ 𝑋) → (𝐾 ∈ CMetSp ↔ 𝐴 ∈ (Clsd‘𝐽)))
Theorem	lssbn 25259	A subspace of a Banach space is a Banach space iff it is closed. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ Ban ∧ 𝑈 ∈ 𝑆) → (𝑋 ∈ Ban ↔ 𝑈 ∈ (Clsd‘𝐽)))
Theorem	cmetcusp1 25260	If the uniform set of a complete metric space is the uniform structure generated by its metric, then it is a complete uniform space. (Contributed by Thierry Arnoux, 15-Dec-2017.)
⊢ 𝑋 = (Base‘𝐹)    &   ⊢ 𝐷 = ((dist‘𝐹) ↾ (𝑋 × 𝑋))    &   ⊢ 𝑈 = (UnifSt‘𝐹)    ⇒   ⊢ ((𝑋 ≠ ∅ ∧ 𝐹 ∈ CMetSp ∧ 𝑈 = (metUnif‘𝐷)) → 𝐹 ∈ CUnifSp)
Theorem	cmetcusp 25261	The uniform space generated by a complete metric is a complete uniform space. (Contributed by Thierry Arnoux, 5-Dec-2017.)
⊢ ((𝑋 ≠ ∅ ∧ 𝐷 ∈ (CMet‘𝑋)) → (toUnifSp‘(metUnif‘𝐷)) ∈ CUnifSp)
Theorem	cncms 25262	The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ℂfld ∈ CMetSp
Theorem	cnflduss 25263	The uniform structure of the complex numbers. (Contributed by Thierry Arnoux, 17-Dec-2017.) (Revised by Thierry Arnoux, 11-Mar-2018.)
⊢ 𝑈 = (UnifSt‘ℂfld)    ⇒   ⊢ 𝑈 = (metUnif‘(abs ∘ − ))
Theorem	cnfldcusp 25264	The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ ℂfld ∈ CUnifSp
Theorem	resscdrg 25265	The real numbers are a subset of any complete subfield in the complex numbers. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (ℂfld ↾s 𝐾)    ⇒   ⊢ ((𝐾 ∈ (SubRing‘ℂfld) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp) → ℝ ⊆ 𝐾)
Theorem	cncdrg 25266	The only complete subfields of the complex numbers are ℝ and ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (ℂfld ↾s 𝐾)    ⇒   ⊢ ((𝐾 ∈ (SubRing‘ℂfld) ∧ 𝐹 ∈ DivRing ∧ 𝐹 ∈ CMetSp) → 𝐾 ∈ {ℝ, ℂ})
Theorem	srabn 25267	The subring algebra over a complete normed ring is a Banach space iff the subring is a closed division ring. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐴 = ((subringAlg ‘𝑊)‘𝑆)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ NrmRing ∧ 𝑊 ∈ CMetSp ∧ 𝑆 ∈ (SubRing‘𝑊)) → (𝐴 ∈ Ban ↔ (𝑆 ∈ (Clsd‘𝐽) ∧ (𝑊 ↾s 𝑆) ∈ DivRing)))
Theorem	rlmbn 25268	The ring module over a complete normed division ring is a Banach space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝑅 ∈ NrmRing ∧ 𝑅 ∈ DivRing ∧ 𝑅 ∈ CMetSp) → (ringLMod‘𝑅) ∈ Ban)
Theorem	ishl 25269	The predicate "is a subcomplex Hilbert space". A Hilbert space is a Banach space which is also an inner product space, i.e. whose norm satisfies the parallelogram law. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ ℂHil ↔ (𝑊 ∈ Ban ∧ 𝑊 ∈ ℂPreHil))
Theorem	hlbn 25270	Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Ban)
Theorem	hlcph 25271	Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
Theorem	hlphl 25272	Every subcomplex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ PreHil)
Theorem	hlcms 25273	Every subcomplex Hilbert space is a complete metric space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp)
Theorem	hlprlem 25274	Lemma for hlpr 25276. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil → (𝐾 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐾) ∈ DivRing ∧ (ℂfld ↾s 𝐾) ∈ CMetSp))
Theorem	hlress 25275	The scalar field of a subcomplex Hilbert space contains ℝ. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil → ℝ ⊆ 𝐾)
Theorem	hlpr 25276	The scalar field of a subcomplex Hilbert space is either ℝ or ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil → 𝐾 ∈ {ℝ, ℂ})
Theorem	ishl2 25277	A Hilbert space is a complete subcomplex pre-Hilbert space over ℝ or ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil ↔ (𝑊 ∈ CMetSp ∧ 𝑊 ∈ ℂPreHil ∧ 𝐾 ∈ {ℝ, ℂ}))
Theorem	cphssphl 25278	A Banach subspace of a subcomplex pre-Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 11-Apr-2008.) (Revised by AV, 25-Sep-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ 𝑋 ∈ Ban) → 𝑋 ∈ ℂHil)
Theorem	cmslssbn 25279	A complete linear subspace of a normed vector space is a Banach space. We furthermore have to assume that the field of scalars is complete since this is a requirement in the current definition of Banach spaces df-bn 25243. (Contributed by AV, 8-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp) ∧ (𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆)) → 𝑋 ∈ Ban)
Theorem	cmscsscms 25280	A closed subspace of a complete metric space which is also a subcomplex pre-Hilbert space is a complete metric space. Remark: the assumption that the Banach space must be a (subcomplex) pre-Hilbert space is required because the definition of ClSubSp is based on an inner product. If ClSubSp was generalized to arbitrary topological spaces (or at least topological modules), this assumption could be omitted. (Contributed by AV, 8-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (ClSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ CMetSp ∧ 𝑊 ∈ ℂPreHil) ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ CMetSp)
Theorem	bncssbn 25281	A closed subspace of a Banach space which is also a subcomplex pre-Hilbert space is a Banach space. Remark: the assumption that the Banach space must be a (subcomplex) pre-Hilbert space is required because the definition of ClSubSp is based on an inner product. If ClSubSp was generalized for arbitrary topological spaces, this assuption could be omitted. (Contributed by AV, 8-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (ClSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ Ban ∧ 𝑊 ∈ ℂPreHil) ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ Ban)
Theorem	cssbn 25282	A complete subspace of a normed vector space with a complete scalar field is a Banach space. Remark: In contrast to ClSubSp, a complete subspace is defined by "a linear subspace in which all Cauchy sequences converge to a point in the subspace". This is closer to the original, but deprecated definition Cℋ (df-ch 31157) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn 25279. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐷 = ((dist‘𝑊) ↾ (𝑈 × 𝑈))    ⇒   ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp ∧ 𝑈 ∈ 𝑆) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘(MetOpen‘𝐷))) → 𝑋 ∈ Ban)
Theorem	csschl 25283	A complete subspace of a complex pre-Hilbert space is a complex Hilbert space. Remarks: (a) In contrast to ClSubSp, a complete subspace is defined by "a linear subspace in which all Cauchy sequences converge to a point in the subspace". This is closer to the original, but deprecated definition Cℋ (df-ch 31157) of closed subspaces of a Hilbert space. (b) This theorem does not hold for arbitrary subcomplex (pre-)Hilbert spaces, because the scalar field as restriction of the field of the complex numbers need not be closed. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐷 = ((dist‘𝑊) ↾ (𝑈 × 𝑈))    &   ⊢ (Scalar‘𝑊) = ℂfld    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆 ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘(MetOpen‘𝐷))) → (𝑋 ∈ ℂHil ∧ (Scalar‘𝑋) = ℂfld))
Theorem	cmslsschl 25284	A complete linear subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by AV, 8-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂHil)
Theorem	chlcsschl 25285	A closed subspace of a subcomplex Hilbert space is a subcomplex Hilbert space. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 8-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (ClSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂHil)
12.5.7.1  The complete ordered field of the real numbers
Theorem	retopn 25286	The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (topGen‘ran (,)) = (TopOpen‘ℝfld)
Theorem	recms 25287	The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝfld ∈ CMetSp
Theorem	reust 25288	The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (UnifSt‘ℝfld) = (metUnif‘((dist‘ℝfld) ↾ (ℝ × ℝ)))
Theorem	recusp 25289	The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ ℝfld ∈ CUnifSp
12.5.8  Euclidean spaces
Syntax	crrx 25290	Extend class notation with generalized real Euclidean spaces.
class ℝ^
Syntax	cehl 25291	Extend class notation with real Euclidean spaces.
class 𝔼hil
Definition	df-rrx 25292	Define the function associating with a set the free real vector space on that set, equipped with the natural inner product and norm. This is the direct sum of copies of the field of real numbers indexed by that set. We call it here a "generalized real Euclidean space", but note that it need not be complete (for instance if the given set is infinite countable). (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ ℝ^ = (𝑖 ∈ V ↦ (toℂPreHil‘(ℝfld freeLMod 𝑖)))
Definition	df-ehl 25293	Define a function generating the real Euclidean spaces of finite dimension. The case 𝑛 = 0 corresponds to a space of dimension 0, that is, limited to a neutral element (see ehl0 25324). Members of this family of spaces are Hilbert spaces, as shown in - ehlhl . (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝔼hil = (𝑛 ∈ ℕ0 ↦ (ℝ^‘(1...𝑛)))
Theorem	rrxval 25294	Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼)))
Theorem	rrxbase 25295*	The base of the generalized real Euclidean space is the set of functions with finite support. (Contributed by Thierry Arnoux, 16-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐵 = {𝑓 ∈ (ℝ ↑m 𝐼) ∣ 𝑓 finSupp 0})
Theorem	rrxprds 25296	Expand the definition of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘((ℝfldXs(𝐼 × {((subringAlg ‘ℝfld)‘ℝ)})) ↾s 𝐵)))
Theorem	rrxip 25297*	The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) = (·𝑖‘𝐻))
Theorem	rrxnm 25298*	The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻))
Theorem	rrxcph 25299	Generalized Euclidean real spaces are subcomplex pre-Hilbert spaces. (Contributed by Thierry Arnoux, 23-Jun-2019.) (Proof shortened by AV, 22-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 ∈ ℂPreHil)
Theorem	rrxds 25300*	The distance over generalized Euclidean spaces. Compare with df-rrn 37827. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻))