P. 252 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 25101-25200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cphorthcom 25101	Orthogonality (meaning inner product is 0) is commutative. Complex version of iporthcom 21544. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉) → ((𝐴 , 𝐵) = 0 ↔ (𝐵 , 𝐴) = 0))
Theorem	cphip0l 25102	Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. Complex version of ip0l 21545. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ( 0 , 𝐴) = 0)
Theorem	cphip0r 25103	Inner product with a zero second argument. Complex version of ip0r 21546. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → (𝐴 , 0 ) = 0)
Theorem	cphipeq0 25104	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 21547. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 0 = (0g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝐴 ∈ 𝑉) → ((𝐴 , 𝐴) = 0 ↔ 𝐴 = 0 ))
Theorem	cphdir 25105	Distributive law for inner product (right-distributivity). Equation I3 of [Ponnusamy] p. 362. Complex version of ipdir 21548. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 + 𝐵) , 𝐶) = ((𝐴 , 𝐶) + (𝐵 , 𝐶)))
Theorem	cphdi 25106	Distributive law for inner product (left-distributivity). Complex version of ipdi 21549. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 + 𝐶)) = ((𝐴 , 𝐵) + (𝐴 , 𝐶)))
Theorem	cph2di 25107	Distributive law for inner product. Complex version of ip2di 21550. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 + 𝐵) , (𝐶 + 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) + ((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	cphsubdir 25108	Distributive law for inner product subtraction. Complex version of ipsubdir 21551. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 − 𝐵) , 𝐶) = ((𝐴 , 𝐶) − (𝐵 , 𝐶)))
Theorem	cphsubdi 25109	Distributive law for inner product subtraction. Complex version of ipsubdi 21552. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝑉 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐴 , (𝐵 − 𝐶)) = ((𝐴 , 𝐵) − (𝐴 , 𝐶)))
Theorem	cph2subdi 25110	Distributive law for inner product subtraction. Complex version of ip2subdi 21553. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐶 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐷 ∈ 𝑉)    ⇒   ⊢ (𝜑 → ((𝐴 − 𝐵) , (𝐶 − 𝐷)) = (((𝐴 , 𝐶) + (𝐵 , 𝐷)) − ((𝐴 , 𝐷) + (𝐵 , 𝐶))))
Theorem	cphass 25111	Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. See ipass 21554, his5 31015. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → ((𝐴 · 𝐵) , 𝐶) = (𝐴 · (𝐵 , 𝐶)))
Theorem	cphassr 25112	"Associative" law for second argument of inner product (compare cphass 25111). See ipassr 21555, his52 . (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝑉 ∧ 𝐶 ∈ 𝑉)) → (𝐵 , (𝐴 · 𝐶)) = ((∗‘𝐴) · (𝐵 , 𝐶)))
Theorem	cph2ass 25113	Move scalar multiplication to outside of inner product. See his35 31017. (Contributed by Mario Carneiro, 17-Oct-2015.)
⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ (𝐴 ∈ 𝐾 ∧ 𝐵 ∈ 𝐾) ∧ (𝐶 ∈ 𝑉 ∧ 𝐷 ∈ 𝑉)) → ((𝐴 · 𝐶) , (𝐵 · 𝐷)) = ((𝐴 · (∗‘𝐵)) · (𝐶 , 𝐷)))
Theorem	cphassi 25114	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 25115	"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	cphpyth 25116	The pythagorean theorem for a subcomplex pre-Hilbert space. The square of the norm of the sum of two orthogonal vectors (i.e., whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008.) (Revised by SN, 22-Sep-2024.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ ((𝜑 ∧ (𝐴 , 𝐵) = 0) → ((𝑁‘(𝐴 + 𝐵))↑2) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))
Theorem	tcphex 25117*	Lemma for tcphbas 25119 and similar theorems. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))) ∈ V
Theorem	tcphval 25118*	Define a function to augment a subcomplex pre-Hilbert space with norm. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ 𝐺 = (𝑊 toNrmGrp (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))
Theorem	tcphbas 25119	The base set of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    ⇒   ⊢ 𝑉 = (Base‘𝐺)
Theorem	tchplusg 25120	The addition operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ + = (+g‘𝑊)    ⇒   ⊢ + = (+g‘𝐺)
Theorem	tcphsub 25121	The subtraction operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ − = (-g‘𝐺)
Theorem	tcphmulr 25122	The ring operation of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = (.r‘𝑊)    ⇒   ⊢ · = (.r‘𝐺)
Theorem	tcphsca 25123	The scalar field of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    ⇒   ⊢ 𝐹 = (Scalar‘𝐺)
Theorem	tcphvsca 25124	The scalar multiplication of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = ( ·𝑠 ‘𝑊)    ⇒   ⊢ · = ( ·𝑠 ‘𝐺)
Theorem	tcphip 25125	The inner product of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ · = (·𝑖‘𝑊)    ⇒   ⊢ · = (·𝑖‘𝐺)
Theorem	tcphtopn 25126	The topology of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝐷 = (dist‘𝐺)    &   ⊢ 𝐽 = (TopOpen‘𝐺)    ⇒   ⊢ (𝑊 ∈ 𝑉 → 𝐽 = (MetOpen‘𝐷))
Theorem	tcphphl 25127	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ℂPreHil‘𝑊)    ⇒   ⊢ (𝑊 ∈ PreHil ↔ 𝐺 ∈ PreHil)
Theorem	tchnmfval 25128*	The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ (𝑊 ∈ Grp → 𝑁 = (𝑥 ∈ 𝑉 ↦ (√‘(𝑥 , 𝑥))))
Theorem	tcphnmval 25129	The norm of a subcomplex pre-Hilbert space augmented with norm. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝑊 ∈ Grp ∧ 𝑋 ∈ 𝑉) → (𝑁‘𝑋) = (√‘(𝑋 , 𝑋)))
Theorem	cphtcphnm 25130	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ℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    ⇒   ⊢ (𝑊 ∈ ℂPreHil → 𝑁 = (norm‘𝐺))
Theorem	tcphds 25131	The distance of a pre-Hilbert space augmented with norm. (Contributed by Thierry Arnoux, 30-Jun-2019.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ − = (-g‘𝑊)    ⇒   ⊢ (𝑊 ∈ Grp → (𝑁 ∘ − ) = (dist‘𝐺))
Theorem	phclm 25132	A pre-Hilbert space whose field of scalars is a restriction of the field of complex numbers is a subcomplex module. TODO: redundant hypotheses. (Contributed by Mario Carneiro, 16-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    ⇒   ⊢ (𝜑 → 𝑊 ∈ ℂMod)
Theorem	tcphcphlem3 25133	Lemma for tcphcph 25137: real closure of an inner product of a vector with itself. (Contributed by Mario Carneiro, 10-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    ⇒   ⊢ ((𝜑 ∧ 𝑋 ∈ 𝑉) → (𝑋 , 𝑋) ∈ ℝ)
Theorem	ipcau2 25134*	The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space built from a pre-Hilbert space with certain properties. The main theorem is ipcau 25138. (Contributed by Mario Carneiro, 11-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ 𝑁 = (norm‘𝐺)    &   ⊢ 𝐶 = ((𝑌 , 𝑋) / (𝑌 , 𝑌))    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌)))
Theorem	tcphcphlem1 25135*	Lemma for tcphcph 25137: the triangle inequality. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ − = (-g‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝑉)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (√‘((𝑋 − 𝑌) , (𝑋 − 𝑌))) ≤ ((√‘(𝑋 , 𝑋)) + (√‘(𝑌 , 𝑌))))
Theorem	tcphcphlem2 25136*	Lemma for tcphcph 25137: homogeneity. (Contributed by Mario Carneiro, 8-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ · = ( ·𝑠 ‘𝑊)    &   ⊢ (𝜑 → 𝑋 ∈ 𝐾)    &   ⊢ (𝜑 → 𝑌 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (√‘((𝑋 · 𝑌) , (𝑋 · 𝑌))) = ((abs‘𝑋) · (√‘(𝑌 , 𝑌))))
Theorem	tcphcph 25137*	The standard definition of a norm turns any pre-Hilbert space over a subfield of ℂfld closed under square roots of nonnegative reals into a subcomplex pre-Hilbert space (which allows access to a norm, metric, and topology). (Contributed by Mario Carneiro, 11-Oct-2015.)
⊢ 𝐺 = (toℂPreHil‘𝑊)    &   ⊢ 𝑉 = (Base‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ (𝜑 → 𝑊 ∈ PreHil)    &   ⊢ (𝜑 → 𝐹 = (ℂfld ↾s 𝐾))    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ ((𝜑 ∧ (𝑥 ∈ 𝐾 ∧ 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) → (√‘𝑥) ∈ 𝐾)    &   ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑉) → 0 ≤ (𝑥 , 𝑥))    ⇒   ⊢ (𝜑 → 𝐺 ∈ ℂPreHil)
Theorem	ipcau 25138	The Cauchy-Schwarz inequality for a subcomplex pre-Hilbert space. Part of Lemma 3.2-1(a) of [Kreyszig] p. 137. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 11-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (abs‘(𝑋 , 𝑌)) ≤ ((𝑁‘𝑋) · (𝑁‘𝑌)))
Theorem	nmparlem 25139	Lemma for nmpar 25140. (Contributed by Mario Carneiro, 7-Oct-2015.)
⊢ 𝑉 = (Base‘𝑊)    &   ⊢ + = (+g‘𝑊)    &   ⊢ − = (-g‘𝑊)    &   ⊢ 𝑁 = (norm‘𝑊)    &   ⊢ , = (·𝑖‘𝑊)    &   ⊢ 𝐹 = (Scalar‘𝑊)    &   ⊢ 𝐾 = (Base‘𝐹)    &   ⊢ (𝜑 → 𝑊 ∈ ℂPreHil)    &   ⊢ (𝜑 → 𝐴 ∈ 𝑉)    &   ⊢ (𝜑 → 𝐵 ∈ 𝑉)    ⇒   ⊢ (𝜑 → (((𝑁‘(𝐴 + 𝐵))↑2) + ((𝑁‘(𝐴 − 𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))))
Theorem	nmpar 25140	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 25141	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 25142	Four times the inner product value cphipval2 25141. (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 25143*	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 25144	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 25145*	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 25146	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 25147*	Continuity of inner product; analogue of cnmpt12f 23553 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 25148*	Continuity of inner product; analogue of cnmpt22f 23562 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 25149	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.)
⊢ 𝐶 = (ClSubSp‘𝑊)    &   ⊢ 𝐽 = (TopOpen‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑆 ∈ 𝐶) → 𝑆 ∈ (Clsd‘𝐽))
Theorem	clsocv 25150	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‘𝐽)‘𝑆)) = (𝑂‘𝑆))
Theorem	cphsscph 25151	A subspace of a subcomplex pre-Hilbert space is a subcomplex pre-Hilbert space. (Contributed by NM, 1-Feb-2008.) (Revised by AV, 25-Sep-2022.)
⊢ 𝑋 = (𝑊 ↾s 𝑈)    &   ⊢ 𝑆 = (LSubSp‘𝑊)    ⇒   ⊢ ((𝑊 ∈ ℂPreHil ∧ 𝑈 ∈ 𝑆) → 𝑋 ∈ ℂPreHil)
12.5.5  Convergence and completeness
Syntax	ccfil 25152	Extend class notation with the class of Cauchy filters.
class CauFil
Syntax	ccau 25153	Extend class notation with the class of Cauchy sequences.
class Cau
Syntax	ccmet 25154	Extend class notation with the class of complete metrics.
class CMet
Definition	df-cfil 25155*	Define the set of Cauchy filters on a given extended 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 25156*	Define the set of Cauchy sequences on a given extended metric space. (Contributed by NM, 8-Sep-2006.)
⊢ Cau = (𝑑 ∈ ∪ ran ∞Met ↦ {𝑓 ∈ (dom dom 𝑑 ↑pm ℂ) ∣ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ (𝑓 ↾ (ℤ≥‘𝑗)):(ℤ≥‘𝑗)⟶((𝑓‘𝑗)(ball‘𝑑)𝑥)})
Definition	df-cmet 25157*	Define the set of complete metrics on a given set. (Contributed by Mario Carneiro, 1-May-2014.)
⊢ CMet = (𝑥 ∈ V ↦ {𝑑 ∈ (Met‘𝑥) ∣ ∀𝑓 ∈ (CauFil‘𝑑)((MetOpen‘𝑑) fLim 𝑓) ≠ ∅})
Theorem	lmmbr 25158*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23116. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ ran ℤ≥(𝐹 ↾ 𝑦):𝑦⟶(𝑃(ball‘𝐷)𝑥))))
Theorem	lmmbr2 25159*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space. Definition 1.4-1 of [Kreyszig] p. 25. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23116. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ 𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)(𝑘 ∈ dom 𝐹 ∧ (𝐹‘𝑘) ∈ 𝑋 ∧ ((𝐹‘𝑘)𝐷𝑃) < 𝑥))))
Theorem	lmmbr3 25160*	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 25161*	Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)    &   ⊢ (𝜑 → 𝑅 ∈ ℝ+)    ⇒   ⊢ (𝜑 → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴 ∈ 𝑋 ∧ (𝐴𝐷𝑃) < 𝑅))
Theorem	lmmbrf 25162*	Express the binary relation "sequence 𝐹 converges to point 𝑃 " in a metric space using an arbitrary upper set of integers. This version of lmmbr2 25159 presupposes that 𝐹 is a function. (Contributed by NM, 20-Jul-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ 𝑍) → (𝐹‘𝑘) = 𝐴)    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    ⇒   ⊢ (𝜑 → (𝐹(⇝𝑡‘𝐽)𝑃 ↔ (𝑃 ∈ 𝑋 ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)(𝐴𝐷𝑃) < 𝑥)))
Theorem	lmnn 25163*	A condition that implies convergence. (Contributed by NM, 8-Jun-2007.) (Revised by Mario Carneiro, 1-May-2014.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (∞Met‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹:ℕ⟶𝑋)    &   ⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝐹‘𝑘)𝐷𝑃) < (1 / 𝑘))    ⇒   ⊢ (𝜑 → 𝐹(⇝𝑡‘𝐽)𝑃)
Theorem	cfilfval 25164*	The set of Cauchy filters on a metric space. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (CauFil‘𝐷) = {𝑓 ∈ (Fil‘𝑋) ∣ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝑓 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥)})
Theorem	iscfil 25165*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 (𝐷 “ (𝑦 × 𝑦)) ⊆ (0[,)𝑥))))
Theorem	iscfil2 25166*	The property of being a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ∈ (Fil‘𝑋) ∧ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐹 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥)))
Theorem	cfilfil 25167	A Cauchy filter is a filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → 𝐹 ∈ (Fil‘𝑋))
Theorem	cfili 25168*	Property of a Cauchy filter. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝐹 ∀𝑦 ∈ 𝑥 ∀𝑧 ∈ 𝑥 (𝑦𝐷𝑧) < 𝑅)
Theorem	cfil3i 25169*	A Cauchy filter contains balls of any pre-chosen size. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷) ∧ 𝑅 ∈ ℝ+) → ∃𝑥 ∈ 𝑋 (𝑥(ball‘𝐷)𝑅) ∈ 𝐹)
Theorem	cfilss 25170	A filter finer than a Cauchy filter is Cauchy. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ (((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) ∧ (𝐺 ∈ (Fil‘𝑋) ∧ 𝐹 ⊆ 𝐺)) → 𝐺 ∈ (CauFil‘𝐷))
Theorem	fgcfil 25171*	The Cauchy filter condition for a filter base. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑋)) → ((𝑋filGen𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 (𝑧𝐷𝑤) < 𝑥))
Theorem	fmcfil 25172*	The Cauchy filter condition for a filter map. (Contributed by Mario Carneiro, 13-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐵 ∈ (fBas‘𝑌) ∧ 𝐹:𝑌⟶𝑋) → (((𝑋 FilMap 𝐹)‘𝐵) ∈ (CauFil‘𝐷) ↔ ∀𝑥 ∈ ℝ+ ∃𝑦 ∈ 𝐵 ∀𝑧 ∈ 𝑦 ∀𝑤 ∈ 𝑦 ((𝐹‘𝑧)𝐷(𝐹‘𝑤)) < 𝑥))
Theorem	iscfil3 25173*	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 25174	Similar to ultrafilters (uffclsflim 23918), 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 25175*	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 25176*	Express the property "𝐹 is a Cauchy sequence of metric 𝐷". Part of Definition 1.4-3 of [Kreyszig] p. 28. The condition 𝐹 ⊆ (ℂ × 𝑋) allows to use objects more general than sequences when convenient; see the comment in df-lm 23116. (Contributed by NM, 7-Dec-2006.) (Revised by Mario Carneiro, 14-Nov-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (𝐹 ∈ (Cau‘𝐷) ↔ (𝐹 ∈ (𝑋 ↑pm ℂ) ∧ ∀𝑥 ∈ ℝ+ ∃𝑘 ∈ ℤ (𝐹 ↾ (ℤ≥‘𝑘)):(ℤ≥‘𝑘)⟶((𝐹‘𝑘)(ball‘𝐷)𝑥))))
Theorem	iscau2 25177*	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 25178*	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 25179*	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 25180*	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 25181	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 25182	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 25183	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 25184*	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 25185	The convergence of a Cauchy filter in a complete metric space. (Contributed by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    ⇒   ⊢ ((𝐷 ∈ (CMet‘𝑋) ∧ 𝐹 ∈ (CauFil‘𝐷)) → (𝐽 fLim 𝐹) ≠ ∅)
Theorem	cmetmet 25186	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 25187	A complete metric space is a metric space. (Contributed by NM, 26-Oct-2007.)
⊢ 𝐷 ∈ (CMet‘𝑋)    ⇒   ⊢ 𝐷 ∈ (Met‘𝑋)
Theorem	cmetcaulem 25188*	Lemma for cmetcau 25189. (Contributed by Mario Carneiro, 14-Oct-2015.)
⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝐷 ∈ (CMet‘𝑋))    &   ⊢ (𝜑 → 𝑃 ∈ 𝑋)    &   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))    &   ⊢ 𝐺 = (𝑥 ∈ ℕ ↦ if(𝑥 ∈ dom 𝐹, (𝐹‘𝑥), 𝑃))    ⇒   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))
Theorem	cmetcau 25189	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 25190*	Lemma for iscmet3 25193. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    ⇒   ⊢ ((𝑀 ∈ ℤ ∧ 𝑅 ∈ ℝ+) → ∃𝑗 ∈ 𝑍 ∀𝑘 ∈ (ℤ≥‘𝑗)((1 / 2)↑𝑘) < 𝑅)
Theorem	iscmet3lem1 25191*	Lemma for iscmet3 25193. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))    ⇒   ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷))
Theorem	iscmet3lem2 25192*	Lemma for iscmet3 25193. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ 𝑍 = (ℤ≥‘𝑀)    &   ⊢ 𝐽 = (MetOpen‘𝐷)    &   ⊢ (𝜑 → 𝑀 ∈ ℤ)    &   ⊢ (𝜑 → 𝐷 ∈ (Met‘𝑋))    &   ⊢ (𝜑 → 𝐹:𝑍⟶𝑋)    &   ⊢ (𝜑 → ∀𝑘 ∈ ℤ ∀𝑢 ∈ (𝑆‘𝑘)∀𝑣 ∈ (𝑆‘𝑘)(𝑢𝐷𝑣) < ((1 / 2)↑𝑘))    &   ⊢ (𝜑 → ∀𝑘 ∈ 𝑍 ∀𝑛 ∈ (𝑀...𝑘)(𝐹‘𝑘) ∈ (𝑆‘𝑛))    &   ⊢ (𝜑 → 𝐺 ∈ (Fil‘𝑋))    &   ⊢ (𝜑 → 𝑆:ℤ⟶𝐺)    &   ⊢ (𝜑 → 𝐹 ∈ dom (⇝𝑡‘𝐽))    ⇒   ⊢ (𝜑 → (𝐽 fLim 𝐺) ≠ ∅)
Theorem	iscmet3 25193*	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 25194	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 25195	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 25196	Cauchy filter on a metric subspace. (Contributed by Mario Carneiro, 15-Oct-2015.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹 ∈ (Fil‘𝑋) ∧ 𝑌 ∈ 𝐹) → (𝐹 ∈ (CauFil‘𝐷) ↔ (𝐹 ↾t 𝑌) ∈ (CauFil‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	caussi 25197	Cauchy sequence on a metric subspace. (Contributed by NM, 30-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ (𝐷 ∈ (∞Met‘𝑋) → (Cau‘(𝐷 ↾ (𝑌 × 𝑌))) ⊆ (Cau‘𝐷))
Theorem	causs 25198	Cauchy sequence on a metric subspace. (Contributed by NM, 29-Jan-2008.) (Revised by Mario Carneiro, 30-Dec-2013.)
⊢ ((𝐷 ∈ (∞Met‘𝑋) ∧ 𝐹:ℕ⟶𝑌) → (𝐹 ∈ (Cau‘𝐷) ↔ 𝐹 ∈ (Cau‘(𝐷 ↾ (𝑌 × 𝑌)))))
Theorem	equivcfil 25199*	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 25200*	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‘𝐶))