![]() |
Metamath
Proof Explorer Theorem List (p. 248 of 473) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-hl 24701 | 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 24702 | 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 24703 | 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 24704 | A Banach space is a normed vector space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmVec) | ||
Theorem | bnnlm 24705 | A Banach space is a normed module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmMod) | ||
Theorem | bnngp 24706 | A Banach space is a normed group. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ NrmGrp) | ||
Theorem | bnlmod 24707 | A Banach space is a left module. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ LMod) | ||
Theorem | bncms 24708 | A Banach space is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ Ban → 𝑊 ∈ CMetSp) | ||
Theorem | iscms 24709 | 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 24710 | The induced metric on a complete normed group is complete. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑋 = (Base‘𝑀) & ⊢ 𝐷 = ((dist‘𝑀) ↾ (𝑋 × 𝑋)) ⇒ ⊢ (𝑀 ∈ CMetSp → 𝐷 ∈ (CMet‘𝑋)) | ||
Theorem | bncmet 24711 | 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 24712 | A complete metric space is a metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝐺 ∈ CMetSp → 𝐺 ∈ MetSp) | ||
Theorem | cmspropd 24713 | Property deduction for a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝜑 → 𝐵 = (Base‘𝐾)) & ⊢ (𝜑 → 𝐵 = (Base‘𝐿)) & ⊢ (𝜑 → ((dist‘𝐾) ↾ (𝐵 × 𝐵)) = ((dist‘𝐿) ↾ (𝐵 × 𝐵))) & ⊢ (𝜑 → (TopOpen‘𝐾) = (TopOpen‘𝐿)) ⇒ ⊢ (𝜑 → (𝐾 ∈ CMetSp ↔ 𝐿 ∈ CMetSp)) | ||
Theorem | cmssmscld 24714 | 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 24715 | 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 24716 | 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 24717 | 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 24718 | 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 24719 | The field of complex numbers is a complete metric space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ℂfld ∈ CMetSp | ||
Theorem | cnflduss 24720 | 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 24721 | The field of complex numbers is a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℂfld ∈ CUnifSp | ||
Theorem | resscdrg 24722 | 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 24723 | 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 24724 | 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 24725 | 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 24726 | 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 24727 | Every subcomplex Hilbert space is a Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) |
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ Ban) | ||
Theorem | hlcph 24728 | Every subcomplex Hilbert space is a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ ℂPreHil) | ||
Theorem | hlphl 24729 | 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 24730 | Every subcomplex Hilbert space is a complete metric space. (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ (𝑊 ∈ ℂHil → 𝑊 ∈ CMetSp) | ||
Theorem | hlprlem 24731 | Lemma for hlpr 24733. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂHil → (𝐾 ∈ (SubRing‘ℂfld) ∧ (ℂfld ↾s 𝐾) ∈ DivRing ∧ (ℂfld ↾s 𝐾) ∈ CMetSp)) | ||
Theorem | hlress 24732 | The scalar field of a subcomplex Hilbert space contains ℝ. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂHil → ℝ ⊆ 𝐾) | ||
Theorem | hlpr 24733 | The scalar field of a subcomplex Hilbert space is either ℝ or ℂ. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (𝑊 ∈ ℂHil → 𝐾 ∈ {ℝ, ℂ}) | ||
Theorem | ishl2 24734 | 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 24735 | 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 24736 | 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 24700. (Contributed by AV, 8-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) ⇒ ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp) ∧ (𝑋 ∈ CMetSp ∧ 𝑈 ∈ 𝑆)) → 𝑋 ∈ Ban) | ||
Theorem | cmscsscms 24737 | 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 24738 | 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 24739 | 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 30163) of closed subspaces of a Hilbert space. It may be superseded by cmslssbn 24736. (Contributed by NM, 10-Apr-2008.) (Revised by AV, 6-Oct-2022.) |
⊢ 𝑋 = (𝑊 ↾s 𝑈) & ⊢ 𝑆 = (LSubSp‘𝑊) & ⊢ 𝐷 = ((dist‘𝑊) ↾ (𝑈 × 𝑈)) ⇒ ⊢ (((𝑊 ∈ NrmVec ∧ (Scalar‘𝑊) ∈ CMetSp ∧ 𝑈 ∈ 𝑆) ∧ (Cau‘𝐷) ⊆ dom (⇝𝑡‘(MetOpen‘𝐷))) → 𝑋 ∈ Ban) | ||
Theorem | csschl 24740 | 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 30163) 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 24741 | 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 24742 | 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) | ||
Theorem | retopn 24743 | The topology of the real numbers. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ (topGen‘ran (,)) = (TopOpen‘ℝfld) | ||
Theorem | recms 24744 | The real numbers form a complete metric space. (Contributed by Thierry Arnoux, 1-Nov-2017.) |
⊢ ℝfld ∈ CMetSp | ||
Theorem | reust 24745 | The Uniform structure of the real numbers. (Contributed by Thierry Arnoux, 14-Feb-2018.) |
⊢ (UnifSt‘ℝfld) = (metUnif‘((dist‘ℝfld) ↾ (ℝ × ℝ))) | ||
Theorem | recusp 24746 | The real numbers form a complete uniform space. (Contributed by Thierry Arnoux, 17-Dec-2017.) |
⊢ ℝfld ∈ CUnifSp | ||
Syntax | crrx 24747 | Extend class notation with generalized real Euclidean spaces. |
class ℝ^ | ||
Syntax | cehl 24748 | Extend class notation with real Euclidean spaces. |
class 𝔼hil | ||
Definition | df-rrx 24749 | 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 24750 | 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 24781). 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 24751 | Value of the generalized Euclidean space. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐻 = (toℂPreHil‘(ℝfld freeLMod 𝐼))) | ||
Theorem | rrxbase 24752* | 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 24753 | 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 24754* | The inner product of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ (ℝ ↑m 𝐼), 𝑔 ∈ (ℝ ↑m 𝐼) ↦ (ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥) · (𝑔‘𝑥))))) = (·𝑖‘𝐻)) | ||
Theorem | rrxnm 24755* | The norm of the generalized real Euclidean spaces. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ ((𝑓‘𝑥)↑2))))) = (norm‘𝐻)) | ||
Theorem | rrxcph 24756 | 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 24757* | The distance over generalized Euclidean spaces. Compare with df-rrn 36285. (Contributed by Thierry Arnoux, 20-Jun-2019.) (Proof shortened by AV, 20-Jul-2019.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) ⇒ ⊢ (𝐼 ∈ 𝑉 → (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘(ℝfld Σg (𝑥 ∈ 𝐼 ↦ (((𝑓‘𝑥) − (𝑔‘𝑥))↑2))))) = (dist‘𝐻)) | ||
Theorem | rrxvsca 24758 | The scalar product over generalized Euclidean spaces is the componentwise real number multiplication. (Contributed by Thierry Arnoux, 18-Jan-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (Base‘𝐻) & ⊢ ∙ = ( ·𝑠 ‘𝐻) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐽 ∈ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ ℝ) & ⊢ (𝜑 → 𝑋 ∈ (Base‘𝐻)) ⇒ ⊢ (𝜑 → ((𝐴 ∙ 𝑋)‘𝐽) = (𝐴 · (𝑋‘𝐽))) | ||
Theorem | rrxplusgvscavalb 24759* | 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 24760 | 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 24761 | The zero ("origin") in a generalized real Euclidean space. (Contributed by AV, 11-Feb-2023.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 0 = (𝐼 × {0}) ⇒ ⊢ (𝐼 ∈ 𝑉 → (0g‘𝐻) = 0 ) | ||
Theorem | rrx0el 24762 | 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 24763* | 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 24764* | 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 24765* | Euclidean vectors as functions. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → 𝐹:𝐼⟶ℝ) | ||
Theorem | rrxfsupp 24766* | Euclidean vectors are of finite support. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 supp 0) ∈ Fin) | ||
Theorem | rrxsuppss 24767* | Support of Euclidean vectors. (Contributed by Thierry Arnoux, 7-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ (𝜑 → 𝐹 ∈ 𝑋) ⇒ ⊢ (𝜑 → (𝐹 supp 0) ⊆ 𝐼) | ||
Theorem | rrxmvallem 24768* | 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 24769* | The value of the Euclidean metric. Compare with rrnmval 36287. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ ((𝐼 ∈ 𝑉 ∧ 𝐹 ∈ 𝑋 ∧ 𝐺 ∈ 𝑋) → (𝐹𝐷𝐺) = (√‘Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2))) | ||
Theorem | rrxmfval 24770* | The value of the Euclidean metric. Compare with rrnval 36286. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ 𝑉 → 𝐷 = (𝑓 ∈ 𝑋, 𝑔 ∈ 𝑋 ↦ (√‘Σ𝑘 ∈ ((𝑓 supp 0) ∪ (𝑔 supp 0))(((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxmetlem 24771* | Lemma for rrxmet 24772. (Contributed by Thierry Arnoux, 5-Jul-2019.) |
⊢ 𝑋 = {ℎ ∈ (ℝ ↑m 𝐼) ∣ ℎ finSupp 0} & ⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) & ⊢ (𝜑 → 𝐼 ∈ 𝑉) & ⊢ (𝜑 → 𝐹 ∈ 𝑋) & ⊢ (𝜑 → 𝐺 ∈ 𝑋) & ⊢ (𝜑 → 𝐴 ⊆ 𝐼) & ⊢ (𝜑 → 𝐴 ∈ Fin) & ⊢ (𝜑 → ((𝐹 supp 0) ∪ (𝐺 supp 0)) ⊆ 𝐴) ⇒ ⊢ (𝜑 → Σ𝑘 ∈ ((𝐹 supp 0) ∪ (𝐺 supp 0))(((𝐹‘𝑘) − (𝐺‘𝑘))↑2) = Σ𝑘 ∈ 𝐴 (((𝐹‘𝑘) − (𝐺‘𝑘))↑2)) | ||
Theorem | rrxmet 24772* | 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 24773* | 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 24774 | 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 24775* | The distance over generalized Euclidean spaces. Finite dimensional case. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐻 = (ℝ^‘𝐼) & ⊢ 𝐵 = (ℝ ↑m 𝐼) ⇒ ⊢ (𝐼 ∈ Fin → (dist‘𝐻) = (𝑓 ∈ 𝐵, 𝑔 ∈ 𝐵 ↦ (√‘Σ𝑘 ∈ 𝐼 (((𝑓‘𝑘) − (𝑔‘𝑘))↑2)))) | ||
Theorem | rrxmetfi 24776 | Euclidean space is a metric space. Finite dimensional version. (Contributed by Glauco Siliprandi, 24-Dec-2020.) |
⊢ 𝐷 = (dist‘(ℝ^‘𝐼)) ⇒ ⊢ (𝐼 ∈ Fin → 𝐷 ∈ (Met‘(ℝ ↑m 𝐼))) | ||
Theorem | rrxdsfival 24777* | 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 24778 | Value of the Euclidean space of dimension 𝑁. (Contributed by Thierry Arnoux, 16-Jun-2019.) |
⊢ 𝐸 = (𝔼hil‘𝑁) ⇒ ⊢ (𝑁 ∈ ℕ0 → 𝐸 = (ℝ^‘(1...𝑁))) | ||
Theorem | ehlbase 24779 | 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 24780 | 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 24781 | 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 24782* | 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 24783* | 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 24784* | 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 24785 | 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 24786* | 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 24787 | 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)))) | ||
Theorem | minveclem1 24788* | Lemma for minvec 24800. 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 24789* | Lemma for minvec 24800. 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 24790* | Lemma for minvec 24800. 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 24791* | Lemma for minvec 24800. 𝐷 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 24792* | Lemma for minvec 24800. 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 24793* | Lemma for minvec 24800. 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 24794* | Lemma for minvec 24800. 𝐹 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 24795* | Lemma for minvec 24800. 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 24796* | Lemma for minvec 24800. 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 24797* | Lemma for minvec 24800. Discharge the assumptions in minveclem4 24796. (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 24798* | Lemma for minvec 24800. 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 24799* | Lemma for minvec 24800. 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 24800* | 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) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴 − 𝑥)) ≤ (𝑁‘(𝐴 − 𝑦))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |