Home | Metamath
Proof Explorer Theorem List (p. 231 of 426) | < 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: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cphorthcom 23001 | Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 19980. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) = 0 ↔ (𝐵 , 𝐴) = 0)) | ||
Theorem | cphip0l 23002 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 19981. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ( 0 , 𝐴) = 0) | ||
Theorem | cphip0r 23003 | Inner product with a zero second argument. Complex version of ip0r 19982. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 0 ) = 0) | ||
Theorem | cphipeq0 23004 | The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. Complex version of ipeq0 19983. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 0 = (0g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ((𝐴 , 𝐴) = 0 ↔ 𝐴 = 0 )) | ||
Theorem | cphdir 23005 | Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 19984. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 + 𝐵) , 𝐶) = ((𝐴 , 𝐶) + (𝐵 , 𝐶))) | ||
Theorem | cphdi 23006 | Distributive law for inner product (left-distributivity). Complex version of ipdi 19985. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 + 𝐶)) = ((𝐴 , 𝐵) + (𝐴 , 𝐶))) | ||
Theorem | cph2di 23007 | Distributive law for inner product. Complex version of ip2di 19986. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 + 𝐵) , (𝐶 + 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) + ((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | cphsubdir 23008 | Distributive law for inner product subtraction. Complex version of ipsubdir 19987. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) = ((𝐴 , 𝐶) − (𝐵 , 𝐶))) | ||
Theorem | cphsubdi 23009 | Distributive law for inner product subtraction. Complex version of ipsubdi 19988. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 − 𝐶)) = ((𝐴 , 𝐵) − (𝐴 , 𝐶))) | ||
Theorem | cph2subdi 23010 | Distributive law for inner product subtraction. Complex version of ip2subdi 19989. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝐶 ∈ 𝑉) & ⊢ (𝜑 → 𝐷 ∈ 𝑉) ⇒ ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) − ((𝐴 , 𝐷) + (𝐵 , 𝐶)))) | ||
Theorem | cphass 23011 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 19990, his5 27943. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 · 𝐵) , 𝐶) = (𝐴 · (𝐵 , 𝐶))) | ||
Theorem | cphassr 23012 | "Associative" law for second argument of inner product (compare cphass 23011). See ipassr 19991, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 , (𝐴 · 𝐶)) = ((∗‘𝐴) · (𝐵 , 𝐶))) | ||
Theorem | cph2ass 23013 | Move scalar multiplication to outside of inner product. See his35 27945. (Contributed by Mario Carneiro, 17-Oct-2015.) |
⊢ , = (·𝑖‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 · 𝐶) , (𝐵 · 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 , 𝐷))) | ||
Theorem | cphassi 23014 | Associative law for the first argument of an inner product with scalar _𝑖. (Contributed by AV, 17-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → ((i · 𝐵) , 𝐴) = (i · (𝐵 , 𝐴))) | ||
Theorem | cphassir 23015 | "Associative" law for the second argument of an inner product with scalar _𝑖. (Contributed by AV, 17-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , (i · 𝐵)) = (-i · (𝐴 , 𝐵))) | ||
Theorem | tchex 23016* | Lemma for tchbas 23018 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))) ∈ V | ||
Theorem | tchval 23017* | Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ 𝐺 = (𝑊 toNrmGrp (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) | ||
Theorem | tchbas 23018 | The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) ⇒ ⊢ 𝑉 = (Base‘𝐺) | ||
Theorem | tchplusg 23019 | The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ + = (+g‘𝑊) ⇒ ⊢ + = (+g‘𝐺) | ||
Theorem | tchsub 23020 | The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ − = (-g‘𝑊) ⇒ ⊢ − = (-g‘𝐺) | ||
Theorem | tchmulr 23021 | The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ · = (.r‘𝑊) ⇒ ⊢ · = (.r‘𝐺) | ||
Theorem | tchsca 23022 | The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) ⇒ ⊢ 𝐹 = (Scalar‘𝐺) | ||
Theorem | tchvsca 23023 | The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) ⇒ ⊢ · = ( ·𝑠 ‘𝐺) | ||
Theorem | tchip 23024 | The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ · = (·𝑖‘𝑊) ⇒ ⊢ · = (·𝑖‘𝐺) | ||
Theorem | tchtopn 23025 | The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝐷 = (dist‘𝐺) & ⊢ 𝐽 = (TopOpen‘𝐺) ⇒ ⊢ (𝑊 ∈ 𝑉 → 𝐽 = (MetOpen‘𝐷)) | ||
Theorem | tchphl 23026 | Augmentation of a subcomplex pre-Hilbert space with a norm does not affect whether it is still a pre-Hilbert space because all the original components are the same. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) ⇒ ⊢ (𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil) | ||
Theorem | tchnmfval 23027* | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥)))) | ||
Theorem | tchnmval 23028 | The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋))) | ||
Theorem | cphtchnm 23029 | The norm of a norm-augmented subcomplex pre-Hilbert space is the same as the original norm on it. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ (𝑊 ∈ ℂPreHil → 𝑁 = (norm‘𝐺)) | ||
Theorem | tchds 23030 | The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ − = (-g‘𝑊) ⇒ ⊢ (𝑊 ∈ Grp → (𝑁 ∘ − ) = (dist‘𝐺)) | ||
Theorem | tchclm 23031 | Lemma for tchcph 23036. (Contributed by Mario Carneiro, 16-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) ⇒ ⊢ (𝜑 → 𝑊 ∈ ℂMod) | ||
Theorem | tchcphlem3 23032 | Lemma for tchcph 23036: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) ⇒ ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ) | ||
Theorem | ipcau2 23033* | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ 𝑁 = (norm‘𝐺) & ⊢ 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌)) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | tchcphlem1 23034* | Lemma for tchcph 23036: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ − = (-g‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌)))) | ||
Theorem | tchcphlem2 23035* | Lemma for tchcph 23036: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ (𝜑 → 𝑋 ∈ 𝐾) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) ⇒ ⊢ (𝜑 → (√‘((𝑋 · 𝑌) , (𝑋 · 𝑌))) = ((abs‘𝑋) · (√‘(𝑌 , 𝑌)))) | ||
Theorem | tchcph 23036* | The standard definition of a norm turns any pre-Hilbert space over a quadratically closed subfield of ℂfld into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝐺 = (toℂHil‘𝑊) & ⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ PreHil) & ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾)) & ⊢ , = (·𝑖‘𝑊) & ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾) & ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥)) ⇒ ⊢ (𝜑 → 𝐺 ∈ ℂPreHil) | ||
Theorem | ipcau 23037 | The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. (Contributed by Mario Carneiro, 11-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌))) | ||
Theorem | nmparlem 23038 | Lemma for nmpar 23039. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) ⇒ ⊢ (𝜑 → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
Theorem | nmpar 23039 | A subcomplex pre-Hilbert space satisfies the parallelogram law. (Contributed by Mario Carneiro, 7-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
Theorem | cphipval2 23040 | Value of the inner product expressed by the norm defined by it. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2)))) / 4)) | ||
Theorem | 4cphipval2 23041 | Four times the inner product value cphipval2 23040. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 18-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ − = (-g‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (4 · (𝐴 , 𝐵)) = ((((𝑁‘(𝐴 + 𝐵))↑2) − ((𝑁‘(𝐴 − 𝐵))↑2)) + (i · (((𝑁‘(𝐴 + (i · 𝐵)))↑2) − ((𝑁‘(𝐴 − (i · 𝐵)))↑2))))) | ||
Theorem | cphipval 23042* | Value of the inner product expressed by a sum of terms with the norm defined by the inner product. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by AV, 18-Oct-2021.) |
⊢ 𝑋 = (Base‘𝑊) & ⊢ + = (+g‘𝑊) & ⊢ · = ( ·𝑠 ‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐹 = (Scalar‘𝑊) & ⊢ 𝐾 = (Base‘𝐹) ⇒ ⊢ (((𝑊 ∈ ℂPreHil ∧ i ∈ 𝐾) ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴 , 𝐵) = (Σ𝑘 ∈ (1...4)((i↑𝑘) · ((𝑁‘(𝐴 + ((i↑𝑘) · 𝐵)))↑2)) / 4)) | ||
Theorem | ipcnlem2 23043 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → 𝑋 ∈ 𝑉) & ⊢ (𝜑 → 𝑌 ∈ 𝑉) & ⊢ (𝜑 → (𝐴𝐷𝑋) < 𝑈) & ⊢ (𝜑 → (𝐵𝐷𝑌) < 𝑇) ⇒ ⊢ (𝜑 → (abs‘((𝐴 , 𝐵) − (𝑋 , 𝑌))) < 𝑅) | ||
Theorem | ipcnlem1 23044* | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ , = (·𝑖‘𝑊) & ⊢ 𝐷 = (dist‘𝑊) & ⊢ 𝑁 = (norm‘𝑊) & ⊢ 𝑇 = ((𝑅 / 2) / ((𝑁‘𝐴) + 1)) & ⊢ 𝑈 = ((𝑅 / 2) / ((𝑁‘𝐵) + 𝑇)) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐴 ∈ 𝑉) & ⊢ (𝜑 → 𝐵 ∈ 𝑉) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑟 ∈ ℝ+ ∀𝑥 ∈ 𝑉 ∀𝑦 ∈ 𝑉 (((𝐴𝐷𝑥) < 𝑟 ∧ (𝐵𝐷𝑦) < 𝑟) → (abs‘((𝐴 , 𝐵) − (𝑥 , 𝑦))) < 𝑅)) | ||
Theorem | ipcn 23045 | The inner product operation of a subcomplex pre-Hilbert space is continuous. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ , = (·if‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ (𝑊 ∈ ℂPreHil → , ∈ ((𝐽 ×t 𝐽) Cn 𝐾)) | ||
Theorem | cnmpt1ip 23046* | Continuity of inner product; analogue of cnmpt12f 21469 which cannot be used directly because ·𝑖 is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐶 = (TopOpen‘ℂfld) & ⊢ , = (·𝑖‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐴) ∈ (𝐾 Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ 𝐵) ∈ (𝐾 Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋 ↦ (𝐴 , 𝐵)) ∈ (𝐾 Cn 𝐶)) | ||
Theorem | cnmpt2ip 23047* | Continuity of inner product; analogue of cnmpt22f 21478 which cannot be used directly because ·𝑖 is not a function. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐽 = (TopOpen‘𝑊) & ⊢ 𝐶 = (TopOpen‘ℂfld) & ⊢ , = (·𝑖‘𝑊) & ⊢ (𝜑 → 𝑊 ∈ ℂPreHil) & ⊢ (𝜑 → 𝐾 ∈ (TopOn‘𝑋)) & ⊢ (𝜑 → 𝐿 ∈ (TopOn‘𝑌)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐴) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) & ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ 𝐵) ∈ ((𝐾 ×t 𝐿) Cn 𝐽)) ⇒ ⊢ (𝜑 → (𝑥 ∈ 𝑋, 𝑦 ∈ 𝑌 ↦ (𝐴 , 𝐵)) ∈ ((𝐾 ×t 𝐿) Cn 𝐶)) | ||
Theorem | csscld 23048 | A "closed subspace" in a subcomplex pre-Hilbert space is actually closed in the topology induced by the norm, thus justifying the terminology "closed subspace". (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐶 = (CSubSp‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶) → 𝑆 ∈ (Clsd‘𝐽)) | ||
Theorem | clsocv 23049 | The orthogonal complement of the closure of a subset is the same as the orthogonal complement of the subset itself. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑉 = (Base‘𝑊) & ⊢ 𝑂 = (ocv‘𝑊) & ⊢ 𝐽 = (TopOpen‘𝑊) ⇒ ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ⊆ 𝑉) → (𝑂‘((cls‘𝐽)‘𝑆)) = (𝑂‘𝑆)) | ||
Syntax | ccfil 23050 | Extend class notation with the set of Cauchy filters. |
class CauFil | ||
Syntax | cca 23051 | Extend class notation with a function on metric spaces whose value is the set of all Cauchy sequences of the space. |
class Cau | ||
Syntax | cms 23052 | Extend class notation with class of complete metric spaces. |
class CMet | ||
Definition | df-cfil 23053* | Define the set of Cauchy filters on a metric space. A Cauchy filter is a filter on the set such that for every 0 < 𝑥 there is an element of the filter whose metric diameter is less than 𝑥. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ CauFil = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (Fil‘dom dom 𝑑) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝑑 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) | ||
Definition | df-cau 23054* | Define a function on metric spaces whose value is the set of Cauchy sequences of the space. (Contributed by NM, 8-Sep-2006.) |
⊢ Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)}) | ||
Definition | df-cmet 23055* | Define the class of complete metrics. (Contributed by Mario Carneiro, 1-May-2014.) |
⊢ CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅}) | ||
Theorem | lmmbr 23056* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21033. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥)))) | ||
Theorem | lmmbr2 23057* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21033. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥)))) | ||
Theorem | lmmbr3 23058* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥)))) | ||
Theorem | lmmcvg 23059* | Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) ⇒ ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝑃) < 𝑅)) | ||
Theorem | lmmbrf 23060* | Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 23057 presupposes that 𝐹 is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) ⇒ ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴𝐷𝑃) < 𝑥))) | ||
Theorem | lmnn 23061* | A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘)) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) | ||
Theorem | cfilfval 23062* | The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)}) | ||
Theorem | iscfil 23063* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)))) | ||
Theorem | iscfil2 23064* | The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))) | ||
Theorem | cfilfil 23065 | A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → 𝐹 ∈ (Fil‘𝑋)) | ||
Theorem | cfili 23066* | Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦𝐷𝑧) < 𝑅) | ||
Theorem | cfil3i 23067* | A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑅) ∈ 𝐹) | ||
Theorem | cfilss 23068 | A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) ∧ (𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺)) → 𝐺 ∈ (CauFil‘𝐷)) | ||
Theorem | fgcfil 23069* | The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)) | ||
Theorem | fmcfil 23070* | The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((𝑋 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝐹‘𝑧)𝐷(𝐹‘𝑤)) < 𝑥)) | ||
Theorem | iscfil3 23071* | A filter is Cauchy iff it contains a ball of any chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑟 ∈ ℝ+ ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑟) ∈ 𝐹))) | ||
Theorem | cfilfcls 23072 | Similar to ultrafilters (uffclsflim 21835), the cluster points and limit points of a Cauchy filter coincide. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑋 = dom dom 𝐷 ⇒ ⊢ (𝐹 ∈ (CauFil‘𝐷) → (𝐽 fClus 𝐹) = (𝐽 fLim 𝐹)) | ||
Theorem | caufval 23073* | The set of Cauchy sequences on a metric space. (Contributed by NM, 8-Sep-2006.) (Revised by Mario Carneiro, 5-Sep-2015.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘𝐷) = {𝑓 ∈ (𝑋 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝑓‘𝑘)(ball‘𝐷)𝑥)}) | ||
Theorem | iscau 23074* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷." Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition 𝐹 ⊆ (ℂ × 𝑋) allows us to use objects more general than sequences when convenient; see the comment in df-lm 21033. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝐹‘𝑘)(ball‘𝐷)𝑥)))) | ||
Theorem | iscau2 23075* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷," using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷(𝐹‘𝑗)) < 𝑥)))) | ||
Theorem | iscau3 23076* | Express the Cauchy sequence property in the more conventional three-quantifier form. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ∀𝑚 ∈ (ℤ≥‘𝑘)((𝐹‘𝑘)𝐷(𝐹‘𝑚)) < 𝑥)))) | ||
Theorem | iscau4 23077* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷," using an arbitrary upper set of integers. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ 𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝐵) < 𝑥)))) | ||
Theorem | iscauf 23078* | Express the property "𝐹 is a Cauchy sequence of metric 𝐷 " presupposing 𝐹 is a function. (Contributed by NM, 24-Jul-2007.) (Revised by Mario Carneiro, 23-Dec-2013.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋)) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴) & ⊢ ((𝜑 ∧ 𝑗 ∈ 𝑍) → (𝐹‘𝑗) = 𝐵) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) ⇒ ⊢ (𝜑 → (𝐹 ∈ (Cau‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐵𝐷𝐴) < 𝑥)) | ||
Theorem | caun0 23079 | A metric with a Cauchy sequence cannot be empty. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝑋 ≠ ∅) | ||
Theorem | caufpm 23080 | Inclusion of a Cauchy sequence, under our definition. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 24-Dec-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ (𝑋 ↑pm ℂ)) | ||
Theorem | caucfil 23081 | A Cauchy sequence predicate can be expressed in terms of the Cauchy filter predicate for a suitably chosen filter. (Contributed by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐿 = ((𝑋 FilMap 𝐹)‘(ℤ≥ “ 𝑍)) ⇒ ⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝑀 ∈ ℤ ∧ 𝐹:𝑍⟶𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐿 ∈ (CauFil‘𝐷))) | ||
Theorem | iscmet 23082* | The property "𝐷 is a complete metric." meaning all Cauchy filters converge to a point in the space. (Contributed by Mario Carneiro, 1-May-2014.) (Revised by Mario Carneiro, 13-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ (𝐷 ∈ (CMet‘𝑋) ↔ (𝐷 ∈ (Met‘𝑋) ∧ ∀𝑓 ∈ (CauFil‘𝐷)(𝐽 fLim 𝑓) ≠ ∅)) | ||
Theorem | cmetcvg 23083 | The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝐹) ≠ ∅) | ||
Theorem | cmetmet 23084 | A complete metric space is a metric space. (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 29-Jan-2014.) |
⊢ (𝐷 ∈ (CMet‘𝑋) → 𝐷 ∈ (Met‘𝑋)) | ||
Theorem | cmetmeti 23085 | A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.) |
⊢ 𝐷 ∈ (CMet‘𝑋) ⇒ ⊢ 𝐷 ∈ (Met‘𝑋) | ||
Theorem | cmetcaulem 23086* | Lemma for cmetcau 23087. (Contributed by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋)) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) & ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹‘𝑥), 𝑃)) ⇒ ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | cmetcau 23087 | The convergence of a Cauchy sequence in a complete metric space. (Contributed by NM, 19-Dec-2006.) (Revised by Mario Carneiro, 14-Oct-2015.) |
⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
Theorem | iscmet3lem3 23088* | Lemma for iscmet3 23091. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) ⇒ ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅) | ||
Theorem | iscmet3lem1 23089* | Lemma for iscmet3 23091. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) | ||
Theorem | iscmet3lem2 23090* | Lemma for iscmet3 23091. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) & ⊢ (𝜑 → 𝐹:𝑍⟶𝑋) & ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘)) & ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛)) & ⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋)) & ⊢ (𝜑 → 𝑆:ℤ⟶𝐺) & ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽)) ⇒ ⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅) | ||
Theorem | iscmet3 23091* | The property "𝐷 is a complete metric" expressed in terms of functions on ℕ (or any other upper integer set). Thus, we only have to look at functions on ℕ, and not all possible Cauchy filters, to determine completeness. (The proof uses countable choice.) (Contributed by NM, 18-Dec-2006.) (Revised by Mario Carneiro, 5-May-2014.) |
⊢ 𝑍 = (ℤ≥‘𝑀) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ (𝜑 → 𝑀 ∈ ℤ) & ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋)) ⇒ ⊢ (𝜑 → (𝐷 ∈ (CMet‘𝑋) ↔ ∀𝑓 ∈ (Cau‘𝐷)(𝑓:𝑍⟶𝑋 → 𝑓 ∈ dom (⇝𝑡‘𝐽)))) | ||
Theorem | iscmet2 23092 | 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 23093 | 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 23094 | Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ↾t 𝑌) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌))))) | ||
Theorem | caussi 23095 | Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ⊆ (Cau‘𝐷)) | ||
Theorem | causs 23096 | Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.) |
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌))))) | ||
Theorem | equivcfil 23097* | 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 23098* | 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 23099* | 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 23100* | 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) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑋) & ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃) & ⊢ (𝜑 → 𝑅 ∈ ℝ*) & ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑁‘(𝐹‘𝑘)) ≤ 𝑅) ⇒ ⊢ (𝜑 → (𝑁‘𝑃) ≤ 𝑅) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |