P. 254 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25301-25400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	iscms 25301	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 25302	The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑀)    &   ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝑀 ∈ CMetSp → 𝐷 ∈ (CMet‘𝑋))
Theorem	bncmet 25303	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 25304	A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝐺 ∈ CMetSp → 𝐺 ∈ MetSp)
Theorem	cmspropd 25305	Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝜑 → 𝐵 = (Base‘𝐾))    &   ⊢ (𝜑 → 𝐵 = (Base‘𝐿))    &   ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵)))    &   ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿))    ⇒   ⊢ (𝜑 → (𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp))
Theorem	cmssmscld 25306	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 25307	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 25308	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 25309	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 25310	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 25311	The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ℂfld ∈ CMetSp
Theorem	cnflduss 25312	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 25313	The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ ℂfld ∈ CUnifSp
Theorem	resscdrg 25314	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 25315	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 25316	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 25317	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 25318	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 25319	Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Ban)
Theorem	hlcph 25320	Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil)
Theorem	hlphl 25321	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 25322	Every subcomplex Hilbert space is a complete metric space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp)
Theorem	hlprlem 25323	Lemma for hlpr 25325. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil → (𝐾 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐾) ∈ DivRing ∧ (ℂfld ↾s 𝐾) ∈ CMetSp))
Theorem	hlress 25324	The scalar field of a subcomplex Hilbert space contains ℝ. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil → ℝ ⊆ 𝐾)
Theorem	hlpr 25325	The scalar field of a subcomplex Hilbert space is either ℝ or ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    ⇒   ⊢ (𝑊 ∈ ℂHil → 𝐾 ∈ {ℝ, ℂ})
Theorem	ishl2 25326	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 25327	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 25328	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 25292. (Contributed by AV, 8-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp) ∧ (𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆)) → 𝑋 ∈ Ban)
Theorem	cmscsscms 25329	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 25330	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 25331	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 31296) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn 25328. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    &   ⊢ 𝐷 = ((dist‘𝑊) ↾ (𝑈 × 𝑈))    ⇒   ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp ∧ 𝑈 ∈ 𝑆) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘(MetOpen‘𝐷))) → 𝑋 ∈ Ban)
Theorem	csschl 25332	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 31296) 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 25333	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 25334	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 25335	The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ (topGen‘ran (,)) = (TopOpen‘ℝfld)
Theorem	recms 25336	The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.)
⊢ ℝfld ∈ CMetSp
Theorem	reust 25337	The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.)
⊢ (UnifSt‘ℝfld) = (metUnif‘((dist‘ℝfld) ↾ (ℝ × ℝ)))
Theorem	recusp 25338	The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.)
⊢ ℝfld ∈ CUnifSp
12.5.8  Euclidean spaces
Syntax	crrx 25339	Extend class notation with generalized real Euclidean spaces.
class ℝ^
Syntax	cehl 25340	Extend class notation with real Euclidean spaces.
class 𝔼hil
Definition	df-rrx 25341	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 25342	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 25373). 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 25343	Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼)))
Theorem	rrxbase 25344*	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 25345	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 25346*	The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) = (·𝑖‘𝐻))
Theorem	rrxnm 25347*	The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻))
Theorem	rrxcph 25348	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 25349*	The distance over generalized Euclidean spaces. Compare with df-rrn 38027. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻))
Theorem	rrxvsca 25350	The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ ∙ = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐽 ∈ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻))    ⇒   ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽)))
Theorem	rrxplusgvscavalb 25351*	The result of the addition combined with scalar multiplication in a generalized Euclidean space is defined by its coordinate-wise operations. (Contributed by AV, 21-Jan-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (Base‘𝐻)    &   ⊢ ∙ = ( ·𝑠 ‘𝐻)    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐴 ∈ ℝ)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑌 ∈ 𝐵)    &   ⊢ (𝜑 → 𝑍 ∈ 𝐵)    &   ⊢ ✚ = (+g‘𝐻)    &   ⊢ (𝜑 → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (𝑍 = ((𝐴 ∙ 𝑋) ✚ (𝐶 ∙ 𝑌)) ↔ ∀𝑖 ∈ 𝐼 (𝑍‘𝑖) = ((𝐴 · (𝑋‘𝑖)) + (𝐶 · (𝑌‘𝑖)))))
Theorem	rrxsca 25352	The field of real numbers is the scalar field of the generalized real Euclidean space. (Contributed by AV, 15-Jan-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → (Scalar‘𝐻) = ℝfld)
Theorem	rrx0 25353	The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 0 = (𝐼 × {0})    ⇒   ⊢ (𝐼 ∈ 𝑉 → (0g‘𝐻) = 0 )
Theorem	rrx0el 25354	The zero ("origin") in a generalized real Euclidean space is an element of its base set. (Contributed by AV, 11-Feb-2023.)
⊢ 0 = (𝐼 × {0})    &   ⊢ 𝑃 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ 𝑉 → 0 ∈ 𝑃)
Theorem	csbren 25355*	Cauchy-Schwarz-Bunjakovsky inequality for R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (Σ𝑘 ∈ 𝐴 (𝐵 · 𝐶)↑2) ≤ (Σ𝑘 ∈ 𝐴 (𝐵↑2) · Σ𝑘 ∈ 𝐴 (𝐶↑2)))
Theorem	trirn 25356*	Triangle inequality in R^n. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 4-Jun-2014.)
⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐵 ∈ ℝ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝐴) → 𝐶 ∈ ℝ)    ⇒   ⊢ (𝜑 → (√‘Σ𝑘 ∈ 𝐴 ((𝐵 + 𝐶)↑2)) ≤ ((√‘Σ𝑘 ∈ 𝐴 (𝐵↑2)) + (√‘Σ𝑘 ∈ 𝐴 (𝐶↑2))))
Theorem	rrxf 25357*	Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → 𝐹:𝐼⟶ℝ)
Theorem	rrxfsupp 25358*	Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 supp 0) ∈ Fin)
Theorem	rrxsuppss 25359*	Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    ⇒   ⊢ (𝜑 → (𝐹 supp 0) ⊆ 𝐼)
Theorem	rrxmvallem 25360*	Support of the function used for building the distance . (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → ((𝑘 ∈ 𝐼 ↦ (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) supp 0) ⊆ ((𝐹 supp 0) ∪ (𝐺 supp 0)))
Theorem	rrxmval 25361*	The value of the Euclidean metric. Compare with rrnmval 38029. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	rrxmfval 25362*	The value of the Euclidean metric. Compare with rrnval 38028. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑓 supp 0) ∪ (𝑔 supp 0))(((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
Theorem	rrxmetlem 25363*	Lemma for rrxmet 25364. (Contributed by Thierry Arnoux, 5-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    &   ⊢ (𝜑 → 𝐼 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐹 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐺 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐴 ⊆ 𝐼)    &   ⊢ (𝜑 → 𝐴 ∈ Fin)    &   ⊢ (𝜑 → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ⊆ 𝐴)    ⇒   ⊢ (𝜑 → Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ 𝐴 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2))
Theorem	rrxmet 25364*	Euclidean space is a metric space. (Contributed by Jeff Madsen, 2-Sep-2009.) (Proof shortened by Mario Carneiro, 5-Jun-2014.) (Revised by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ 𝑉 → 𝐷 ∈ (Met‘𝑋))
Theorem	rrxdstprj1 25365*	The distance between two points in Euclidean space is greater than the distance between the projections onto one coordinate. (Contributed by Jeff Madsen, 2-Sep-2009.) (Revised by Mario Carneiro, 13-Sep-2015.) (Revised by Thierry Arnoux, 7-Jul-2019.)
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0}    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    &   ⊢ 𝑀 = ((abs ∘ − ) ↾ (ℝ × ℝ))    ⇒   ⊢ (((𝐼 ∈ 𝑉 ∧ 𝐴 ∈ 𝐼) ∧ (𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋)) → ((𝐹‘𝐴)𝑀(𝐺‘𝐴)) ≤ (𝐹𝐷𝐺))
Theorem	rrxbasefi 25366	The base of the generalized real Euclidean space, when the dimension of the space is finite. This justifies the use of (ℝ ↑m 𝑋) for the development of the Lebesgue measure theory for n-dimensional real numbers. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ (𝜑 → 𝑋 ∈ Fin)    &   ⊢ 𝐻 = (ℝ^‘𝑋)    &   ⊢ 𝐵 = (Base‘𝐻)    ⇒   ⊢ (𝜑 → 𝐵 = (ℝ ↑m 𝑋))
Theorem	rrxdsfi 25367*	The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐻 = (ℝ^‘𝐼)    &   ⊢ 𝐵 = (ℝ ↑m 𝐼)    ⇒   ⊢ (𝐼 ∈ Fin → (dist‘𝐻) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
Theorem	rrxmetfi 25368	Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.)
⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑m 𝐼)))
Theorem	rrxdsfival 25369*	The value of the Euclidean distance function in a generalized real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.)
⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝐷 = (dist‘(ℝ^‘𝐼))    ⇒   ⊢ ((𝐼 ∈ Fin ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	ehlval 25370	Value of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐸 = (𝔼hil‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐸 = (ℝ^‘(1...𝑁)))
Theorem	ehlbase 25371	The base of the Euclidean space is the set of n-tuples of real numbers. (Contributed by Thierry Arnoux, 16-Jun-2019.)
⊢ 𝐸 = (𝔼hil‘𝑁)    ⇒   ⊢ (𝑁 ∈ ℕ0 → (ℝ ↑m (1...𝑁)) = (Base‘𝐸))
Theorem	ehl0base 25372	The base of the Euclidean space of dimension 0 consists only of one element, the empty set. (Contributed by AV, 12-Feb-2023.)
⊢ 𝐸 = (𝔼hil‘0)    ⇒   ⊢ (Base‘𝐸) = {∅}
Theorem	ehl0 25373	The Euclidean space of dimension 0 consists of the neutral element only. (Contributed by AV, 12-Feb-2023.)
⊢ 𝐸 = (𝔼hil‘0)    &   ⊢ 0 = (0g‘𝐸)    ⇒   ⊢ (Base‘𝐸) = { 0 }
Theorem	ehleudis 25374*	The Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.)
⊢ 𝐼 = (1...𝑁)    &   ⊢ 𝐸 = (𝔼hil‘𝑁)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ (𝑁 ∈ ℕ0 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2))))
Theorem	ehleudisval 25375*	The value of the Euclidean distance function in a real Euclidean space of finite dimension. (Contributed by AV, 15-Jan-2023.)
⊢ 𝐼 = (1...𝑁)    &   ⊢ 𝐸 = (𝔼hil‘𝑁)    &   ⊢ 𝑋 = (ℝ ↑m 𝐼)    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ 𝐼 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)))
Theorem	ehl1eudis 25376*	The Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘1)    &   ⊢ 𝑋 = (ℝ ↑m {1})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (abs‘((𝑓‘1) − (𝑔‘1))))
Theorem	ehl1eudisval 25377	The value of the Euclidean distance function in a real Euclidean space of dimension 1. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘1)    &   ⊢ 𝑋 = (ℝ ↑m {1})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (abs‘((𝐹‘1) − (𝐺‘1))))
Theorem	ehl2eudis 25378*	The Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘2)    &   ⊢ 𝑋 = (ℝ ↑m {1, 2})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘((((𝑓‘1) − (𝑔‘1))↑2) + (((𝑓‘2) − (𝑔‘2))↑2))))
Theorem	ehl2eudisval 25379	The value of the Euclidean distance function in a real Euclidean space of dimension 2. (Contributed by AV, 16-Jan-2023.)
⊢ 𝐸 = (𝔼hil‘2)    &   ⊢ 𝑋 = (ℝ ↑m {1, 2})    &   ⊢ 𝐷 = (dist‘𝐸)    ⇒   ⊢ ((𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘((((𝐹‘1) − (𝐺‘1))↑2) + (((𝐹‘2) − (𝐺‘2))↑2))))
12.5.9  Minimizing Vector Theorem
Theorem	minveclem1 25380*	Lemma for minvec 25392. The set of all distances from points of 𝑌 to 𝐴 are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    ⇒   ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤))
Theorem	minveclem4c 25381*	Lemma for minvec 25392. The infimum of the distances to 𝐴 is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    ⇒   ⊢ (𝜑 → 𝑆 ∈ ℝ)
Theorem	minveclem2 25382*	Lemma for minvec 25392. Any two points 𝐾 and 𝐿 in 𝑌 are close to each other if they are close to the infimum of distance to 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ (𝜑 → 𝐵 ∈ ℝ)    &   ⊢ (𝜑 → 0 ≤ 𝐵)    &   ⊢ (𝜑 → 𝐾 ∈ 𝑌)    &   ⊢ (𝜑 → 𝐿 ∈ 𝑌)    &   ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵))    &   ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵))    ⇒   ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵))
Theorem	minveclem3a 25383*	Lemma for minvec 25392. 𝐷 is a complete metric when restricted to 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → (𝐷 ↾ (𝑌 × 𝑌)) ∈ (CMet‘𝑌))
Theorem	minveclem3b 25384*	Lemma for minvec 25392. The set of vectors within a fixed distance of the infimum forms a filter base. (Contributed by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    ⇒   ⊢ (𝜑 → 𝐹 ∈ (fBas‘𝑌))
Theorem	minveclem3 25385*	Lemma for minvec 25392. The filter formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    ⇒   ⊢ (𝜑 → (𝑌filGen𝐹) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))
Theorem	minveclem4a 25386*	Lemma for minvec 25392. 𝐹 converges to a point 𝑃 in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    ⇒   ⊢ (𝜑 → 𝑃 ∈ ((𝐽 fLim (𝑋filGen𝐹)) ∩ 𝑌))
Theorem	minveclem4b 25387*	Lemma for minvec 25392. The convergent point of the Cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    ⇒   ⊢ (𝜑 → 𝑃 ∈ 𝑋)
Theorem	minveclem4 25388*	Lemma for minvec 25392. The convergent point of the Cauchy sequence 𝐹 attains the minimum distance, and so is closer to 𝐴 than any other point in 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    &   ⊢ 𝐹 = ran (𝑟 ∈ ℝ+ ↦ {𝑦 ∈ 𝑌 ∣ ((𝐴𝐷𝑦)↑2) ≤ ((𝑆↑2) + 𝑟)})    &   ⊢ 𝑃 = ∪ (𝐽 fLim (𝑋filGen𝐹))    &   ⊢ 𝑇 = (((((𝐴𝐷𝑃) + 𝑆) / 2)↑2) − (𝑆↑2))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minveclem5 25389*	Lemma for minvec 25392. Discharge the assumptions in minveclem4 25388. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minveclem6 25390*	Lemma for minvec 25392. Any minimal point is less than 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Revised by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))))
Theorem	minveclem7 25391*	Lemma for minvec 25392. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    &   ⊢ 𝐽 = (TopOpen‘𝑈)    &   ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴 − 𝑦)))    &   ⊢ 𝑆 = inf(𝑅, ℝ, < )    &   ⊢ 𝐷 = ((dist‘𝑈) ↾ (𝑋 × 𝑋))    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
Theorem	minvec 25392*	Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace 𝑊 that minimizes the distance to an arbitrary vector 𝐴 in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (Revised by Mario Carneiro, 15-Oct-2015.) (Proof shortened by AV, 3-Oct-2020.)
⊢ 𝑋 = (Base‘𝑈)    &   ⊢ − = (-g‘𝑈)    &   ⊢ 𝑁 = (norm‘𝑈)    &   ⊢ (𝜑 → 𝑈 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝑌 ∈ (LSubSp‘𝑈))    &   ⊢ (𝜑 → (𝑈 ↾s 𝑌) ∈ CMetSp)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑋)    ⇒   ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦)))
12.5.10  Projection Theorem
Theorem	pjthlem1 25393*	Lemma for pjth 25395. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 17-Oct-2015.) (Proof shortened by AV, 10-Jul-2022.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑈)    &   ⊢ (𝜑 → ∀𝑥 ∈ 𝑈 (𝑁‘𝐴) ≤ (𝑁‘(𝐴 − 𝑥)))    &   ⊢ 𝑇 = ((𝐴 , 𝐵) / ((𝐵 , 𝐵) + 1))    ⇒   ⊢ (𝜑 → (𝐴 , 𝐵) = 0)
Theorem	pjthlem2 25394	Lemma for pjth 25395. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂHil)    &   ⊢ (𝜑 → 𝑈 ∈ 𝐿)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ (𝜑 → 𝑈 ∈ (Clsd‘𝐽))    ⇒   ⊢ (𝜑 → 𝐴 ∈ (𝑈 ⊕ (𝑂‘𝑈)))
Theorem	pjth 25395	Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed uniquely into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ ⊕ = (LSSum‘𝑊)    &   ⊢ 𝑂 = (ocv‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → (𝑈 ⊕ (𝑂‘𝑈)) = 𝑉)
Theorem	pjth2 25396	Projection Theorem with abbreviations: A topologically closed subspace is a projection subspace. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐾 = (proj‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂHil ∧ 𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽)) → 𝑈 ∈ dom 𝐾)
Theorem	cldcss 25397	Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂHil → (𝑈 ∈ 𝐶 ↔ (𝑈 ∈ 𝐿 ∧ 𝑈 ∈ (Clsd‘𝐽))))
Theorem	cldcss2 25398	Corollary of the Projection Theorem: A topologically closed subspace is algebraically closed in Hilbert space. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    &   ⊢ 𝐿 = (LSubSp‘𝑊)    &   ⊢ 𝐶 = (ClSubSp‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂHil → 𝐶 = (𝐿 ∩ (Clsd‘𝐽)))
Theorem	hlhil 25399	Corollary of the Projection Theorem: A subcomplex Hilbert space is a Hilbert space (in the algebraic sense, meaning that all algebraically closed subspaces have a projection decomposition). (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Hil)
PART 13  BASIC REAL AND COMPLEX ANALYSIS
13.1  Continuity
Theorem	addcncf 25400*	The addition of two continuous complex functions is continuous. (Contributed by Glauco Siliprandi, 11-Dec-2019.)
⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝑋–cn→ℂ))    &   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝑋–cn→ℂ))    ⇒   ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 + 𝐵)) ∈ (𝑋–cn→ℂ))