HomeTheorem List (p. 315 of 510)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 315 of 510) | < 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-31502) |
Hilbert Space Explorer
(31503-33025) |
Users' Mathboxes
(33026-50934) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | isphg 31401* | The predicate "is a complex inner product space." An inner product space is a normed vector space whose norm satisfies the parallelogram law. The vector (group) addition operation is 𝐺, the scalar product is 𝑆, and the norm is 𝑁. An inner product space is also called a pre-Hilbert space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = ran 𝐺 ⇒ ⊢ ((𝐺 ∈ 𝐴 ∧ 𝑆 ∈ 𝐵 ∧ 𝑁 ∈ 𝐶) → (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ CPreHilOLD ↔ (⟨⟨𝐺, 𝑆⟩, 𝑁⟩ ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝐺(-1𝑆𝑦)))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2)))))) | ||
| Theorem | phop 31402 | A complex inner product space in terms of ordered pair components. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 = ⟨⟨𝐺, 𝑆⟩, 𝑁⟩) | ||
| Theorem | cncph 31403 | The set of complex numbers is an inner product (pre-Hilbert) space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (Revised by Mario Carneiro, 7-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩ ⇒ ⊢ 𝑈 ∈ CPreHilOLD | ||
| Theorem | elimph 31404 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ if(𝐴 ∈ 𝑋, 𝐴, 𝑍) ∈ 𝑋 | ||
| Theorem | elimphu 31405 | Hypothesis elimination lemma for complex inner product spaces to assist weak deduction theorem. (Contributed by NM, 6-May-2007.) (New usage is discouraged.) |
| ⊢ if(𝑈 ∈ CPreHilOLD, 𝑈, ⟨⟨ + , · ⟩, abs⟩) ∈ CPreHilOLD | ||
| Theorem | isph 31406* | The predicate "is an inner product space." (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ CPreHilOLD ↔ (𝑈 ∈ NrmCVec ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑋 (((𝑁‘(𝑥𝐺𝑦))↑2) + ((𝑁‘(𝑥𝑀𝑦))↑2)) = (2 · (((𝑁‘𝑥)↑2) + ((𝑁‘𝑦)↑2))))) | ||
| Theorem | phpar2 31407 | The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝑀𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
| Theorem | phpar 31408 | The parallelogram law for an inner product space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
| Theorem | ip0i 31409 | A slight variant of Equation 6.46 of [Ponnusamy] p. 362, where 𝐽 is either 1 or -1 to represent +-1. (Contributed by NM, 23-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐽 ∈ ℂ ⇒ ⊢ ((((𝑁‘((𝐴𝐺𝐵)𝐺(𝐽𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺𝐵)𝐺(-𝐽𝑆𝐶)))↑2)) + (((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(𝐽𝑆𝐶)))↑2) − ((𝑁‘((𝐴𝐺(-1𝑆𝐵))𝐺(-𝐽𝑆𝐶)))↑2))) = (2 · (((𝑁‘(𝐴𝐺(𝐽𝑆𝐶)))↑2) − ((𝑁‘(𝐴𝐺(-𝐽𝑆𝐶)))↑2))) | ||
| Theorem | ip1ilem 31410 | Lemma for ip1i 31411. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐽 ∈ ℂ ⇒ ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶)) | ||
| Theorem | ip1i 31411 | Equation 6.47 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 ⇒ ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶)) | ||
| Theorem | ip2i 31412 | Equation 6.48 of [Ponnusamy] p. 362. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((2𝑆𝐴)𝑃𝐵) = (2 · (𝐴𝑃𝐵)) | ||
| Theorem | ipdirilem 31413 | Lemma for ipdiri 31414. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)) | ||
| Theorem | ipdiri 31414 | Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))) | ||
| Theorem | ipasslem1 31415 | Lemma for ipassi 31425. Show the inner product associative law for nonnegative integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem2 31416 | Lemma for ipassi 31425. Show the inner product associative law for nonpositive integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝑁 ∈ ℕ0 ∧ 𝐴 ∈ 𝑋) → ((-𝑁𝑆𝐴)𝑃𝐵) = (-𝑁 · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem3 31417 | Lemma for ipassi 31425. Show the inner product associative law for all integers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝑁 ∈ ℤ ∧ 𝐴 ∈ 𝑋) → ((𝑁𝑆𝐴)𝑃𝐵) = (𝑁 · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem4 31418 | Lemma for ipassi 31425. Show the inner product associative law for positive integer reciprocals. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝑁 ∈ ℕ ∧ 𝐴 ∈ 𝑋) → (((1 / 𝑁)𝑆𝐴)𝑃𝐵) = ((1 / 𝑁) · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem5 31419 | Lemma for ipassi 31425. Show the inner product associative law for rational numbers. (Contributed by NM, 27-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝐶 ∈ ℚ ∧ 𝐴 ∈ 𝑋) → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem7 31420* | Lemma for ipassi 31425. Show that ((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)) is continuous on ℝ. (Contributed by NM, 23-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) & ⊢ 𝐽 = (topGen‘ran (,)) & ⊢ 𝐾 = (TopOpen‘ℂfld) ⇒ ⊢ 𝐹 ∈ (𝐽 Cn 𝐾) | ||
| Theorem | ipasslem8 31421* | Lemma for ipassi 31425. By ipasslem5 31419, 𝐹 is 0 for all ℚ; since it is continuous and ℚ is dense in ℝ by qdensere2 25096, we conclude 𝐹 is 0 for all ℝ. (Contributed by NM, 24-Aug-2007.) (Revised by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐹 = (𝑤 ∈ ℝ ↦ (((𝑤𝑆𝐴)𝑃𝐵) − (𝑤 · (𝐴𝑃𝐵)))) ⇒ ⊢ 𝐹:ℝ⟶{0} | ||
| Theorem | ipasslem9 31422 | Lemma for ipassi 31425. Conclude from ipasslem8 31421 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (𝐶 ∈ ℝ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem10 31423 | Lemma for ipassi 31425. Show the inner product associative law for the imaginary number i. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((i𝑆𝐴)𝑃𝐵) = (i · (𝐴𝑃𝐵)) | ||
| Theorem | ipasslem11 31424 | Lemma for ipassi 31425. Show the inner product associative law for all complex numbers. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (𝐶 ∈ ℂ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵))) | ||
| Theorem | ipassi 31425 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶))) | ||
| Theorem | dipdir 31426 | Distributive law for inner product. Equation I3 of [Ponnusamy] p. 362. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))) | ||
| Theorem | dipdi 31427 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝐺𝐶)) = ((𝐴𝑃𝐵) + (𝐴𝑃𝐶))) | ||
| Theorem | ip2dii 31428 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝐷 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃(𝐶𝐺𝐷)) = (((𝐴𝑃𝐶) + (𝐵𝑃𝐷)) + ((𝐴𝑃𝐷) + (𝐵𝑃𝐶))) | ||
| Theorem | dipass 31429 | Associative law for inner product. Equation I2 of [Ponnusamy] p. 363. (Contributed by NM, 25-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶))) | ||
| Theorem | dipassr 31430 | "Associative" law for second argument of inner product (compare dipass 31429). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑆𝐶)) = ((∗‘𝐵) · (𝐴𝑃𝐶))) | ||
| Theorem | dipassr2 31431 | "Associative" law for inner product. Conjugate version of dipassr 31430. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃((∗‘𝐵)𝑆𝐶)) = (𝐵 · (𝐴𝑃𝐶))) | ||
| Theorem | dipsubdir 31432 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) − (𝐵𝑃𝐶))) | ||
| Theorem | dipsubdi 31433 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) | ||
| Theorem | pythi 31434 | The Pythagorean theorem for an arbitrary complex inner product (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. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝐴𝑃𝐵) = 0 → ((𝑁‘(𝐴𝐺𝐵))↑2) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))) | ||
| Theorem | siilem1 31435 | Lemma for sii 31438. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ & ⊢ 0 ≤ (𝐶 · (𝐴𝑃𝐵)) ⇒ ⊢ ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
| Theorem | siilem2 31436 | Lemma for sii 31438. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝐶 ∈ ℂ ∧ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ ∧ 0 ≤ (𝐶 · (𝐴𝑃𝐵))) → ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))) | ||
| Theorem | siii 31437 | Inference from sii 31438. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)) | ||
| Theorem | sii 31438 | Obsolete version of ipcau 25539 as of 22-Sep-2024. Schwarz inequality. Part of Lemma 3-2.1(a) of [Kreyszig] p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also Theorems bcseqi 31704, bcsiALT 31763, bcsiHIL 31764, csbren 25700. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
| Theorem | ipblnfi 31439* | A function 𝐹 generated by varying the first argument of an inner product (with its second argument a fixed vector 𝐴) is a bounded linear functional, i.e. a bounded linear operator from the vector space to ℂ. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐶 = ⟨⟨ + , · ⟩, abs⟩ & ⊢ 𝐵 = (𝑈 BLnOp 𝐶) & ⊢ 𝐹 = (𝑥 ∈ 𝑋 ↦ (𝑥𝑃𝐴)) ⇒ ⊢ (𝐴 ∈ 𝑋 → 𝐹 ∈ 𝐵) | ||
| Theorem | ip2eqi 31440* | Two vectors are equal iff their inner products with all other vectors are equal. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (∀𝑥 ∈ 𝑋 (𝑥𝑃𝐴) = (𝑥𝑃𝐵) ↔ 𝐴 = 𝐵)) | ||
| Theorem | phoeqi 31441* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇)) | ||
| Theorem | ajmoi 31442* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ∃*𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) | ||
| Theorem | ajfuni 31443 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝑈adj𝑊) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ Fun 𝐴 | ||
| Theorem | ajfun 31444 | The adjoint function is a function. This is not immediately apparent from df-aj 31334 but results from the uniqueness shown by ajmoi 31442. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec) → Fun 𝐴) | ||
| Theorem | ajval 31445* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑄 = (·𝑖OLD‘𝑊) & ⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝐴‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) | ||
| Syntax | ccbn 31446 | Extend class notation with the class of all complex Banach spaces. |
| class CBan | ||
| Definition | df-cbn 31447 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25637 instead. (New usage is discouraged.) |
| ⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))} | ||
| Theorem | iscbn 31448 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25639 instead. (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋))) | ||
| Theorem | cbncms 31449 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25648 (or preferably bncms 25645) instead. (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋)) | ||
| Theorem | bnnv 31450 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25641 instead. (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec) | ||
| Theorem | bnrel 31451 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| ⊢ Rel CBan | ||
| Theorem | bnsscmcl 31452 | A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝐻 = (SubSp‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) ⇒ ⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ 𝐻) → (𝑊 ∈ CBan ↔ 𝑌 ∈ (Clsd‘𝐽))) | ||
| Theorem | cnbn 31453 | The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩ ⇒ ⊢ 𝑈 ∈ CBan | ||
| Theorem | ubthlem1 31454* | Lemma for ubth 31457. The function 𝐴 exhibits a countable collection of sets that are closed, being the inverse image under 𝑡 of the closed ball of radius 𝑘, and by assumption they cover 𝑋. Thus, by the Baire Category theorem bcth2 25631, for some 𝑛 the set 𝐴‘𝑛 has an interior, meaning that there is a closed ball {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑈 ∈ CBan & ⊢ 𝑊 ∈ NrmCVec & ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) & ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) ⇒ ⊢ (𝜑 → ∃𝑛 ∈ ℕ ∃𝑦 ∈ 𝑋 ∃𝑟 ∈ ℝ+ {𝑧 ∈ 𝑋 ∣ (𝑦𝐷𝑧) ≤ 𝑟} ⊆ (𝐴‘𝑛)) | ||
| Theorem | ubthlem2 31455* | Lemma for ubth 31457. Given that there is a closed ball 𝐵(𝑃, 𝑅) in 𝐴‘𝐾, for any 𝑥 ∈ 𝐵(0, 1), we have 𝑃 + 𝑅 · 𝑥 ∈ 𝐵(𝑃, 𝑅) and 𝑃 ∈ 𝐵(𝑃, 𝑅), so both of these have norm(𝑡(𝑧)) ≤ 𝐾 and so norm(𝑡(𝑥 )) ≤ (norm(𝑡(𝑃)) + norm(𝑡(𝑃 + 𝑅 · 𝑥))) / 𝑅 ≤ ( 𝐾 + 𝐾) / 𝑅, which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑈 ∈ CBan & ⊢ 𝑊 ∈ NrmCVec & ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) & ⊢ (𝜑 → ∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐) & ⊢ 𝐴 = (𝑘 ∈ ℕ ↦ {𝑧 ∈ 𝑋 ∣ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑧)) ≤ 𝑘}) & ⊢ (𝜑 → 𝐾 ∈ ℕ) & ⊢ (𝜑 → 𝑃 ∈ 𝑋) & ⊢ (𝜑 → 𝑅 ∈ ℝ+) & ⊢ (𝜑 → {𝑧 ∈ 𝑋 ∣ (𝑃𝐷𝑧) ≤ 𝑅} ⊆ (𝐴‘𝐾)) ⇒ ⊢ (𝜑 → ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑) | ||
| Theorem | ubthlem3 31456* | Lemma for ubth 31457. Prove the reverse implication, using nmblolbi 31384. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑈 ∈ CBan & ⊢ 𝑊 ∈ NrmCVec & ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) | ||
| Theorem | ubth 31457* | Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let 𝑇 be a collection of bounded linear operators on a Banach space. If, for every vector 𝑥, the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of [Kreyszig] p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle. (Contributed by NM, 7-Nov-2007.) (Proof shortened by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝑀 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ CBan ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ⊆ (𝑈 BLnOp 𝑊)) → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑀‘𝑡) ≤ 𝑑)) | ||
| Theorem | minvecolem1 31458* | Lemma for minveco 31468. The set of all distances from points of 𝑌 to 𝐴 are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) ⇒ ⊢ (𝜑 → (𝑅 ⊆ ℝ ∧ 𝑅 ≠ ∅ ∧ ∀𝑤 ∈ 𝑅 0 ≤ 𝑤)) | ||
| Theorem | minvecolem2 31459* | Lemma for minveco 31468. 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 AV, 4-Oct-2020.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝐵 ∈ ℝ) & ⊢ (𝜑 → 0 ≤ 𝐵) & ⊢ (𝜑 → 𝐾 ∈ 𝑌) & ⊢ (𝜑 → 𝐿 ∈ 𝑌) & ⊢ (𝜑 → ((𝐴𝐷𝐾)↑2) ≤ ((𝑆↑2) + 𝐵)) & ⊢ (𝜑 → ((𝐴𝐷𝐿)↑2) ≤ ((𝑆↑2) + 𝐵)) ⇒ ⊢ (𝜑 → ((𝐾𝐷𝐿)↑2) ≤ (4 · 𝐵)) | ||
| Theorem | minvecolem3 31460* | Lemma for minveco 31468. The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑌) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) ⇒ ⊢ (𝜑 → 𝐹 ∈ (Cau‘𝐷)) | ||
| Theorem | minvecolem4a 31461* | Lemma for minveco 31468. 𝐹 is convergent in the subspace topology on 𝑌. (Contributed by Mario Carneiro, 7-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑌) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) ⇒ ⊢ (𝜑 → 𝐹(⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))((⇝𝑡‘(MetOpen‘(𝐷 ↾ (𝑌 × 𝑌))))‘𝐹)) | ||
| Theorem | minvecolem4b 31462* | Lemma for minveco 31468. The convergent point of the Cauchy sequence 𝐹 is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑌) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) ⇒ ⊢ (𝜑 → ((⇝𝑡‘𝐽)‘𝐹) ∈ 𝑋) | ||
| Theorem | minvecolem4c 31463* | Lemma for minveco 31468. The infimum of the distances to 𝐴 is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑌) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) ⇒ ⊢ (𝜑 → 𝑆 ∈ ℝ) | ||
| Theorem | minvecolem4 31464* | Lemma for minveco 31468. 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 AV, 4-Oct-2020.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) & ⊢ (𝜑 → 𝐹:ℕ⟶𝑌) & ⊢ ((𝜑 ∧ 𝑛 ∈ ℕ) → ((𝐴𝐷(𝐹‘𝑛))↑2) ≤ ((𝑆↑2) + (1 / 𝑛))) & ⊢ 𝑇 = (1 / (((((𝐴𝐷((⇝𝑡‘𝐽)‘𝐹)) + 𝑆) / 2)↑2) − (𝑆↑2))) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) | ||
| Theorem | minvecolem5 31465* | Lemma for minveco 31468. Discharge the assumption about the sequence 𝐹 by applying countable choice ax-cc 10494. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) ⇒ ⊢ (𝜑 → ∃𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) | ||
| Theorem | minvecolem6 31466* | Lemma for minveco 31468. Any minimal point is less than 𝑆 away from 𝐴. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) ⇒ ⊢ ((𝜑 ∧ 𝑥 ∈ 𝑌) → (((𝐴𝐷𝑥)↑2) ≤ ((𝑆↑2) + 0) ↔ ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦)))) | ||
| Theorem | minvecolem7 31467* | Lemma for minveco 31468. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑅 = ran (𝑦 ∈ 𝑌 ↦ (𝑁‘(𝐴𝑀𝑦))) & ⊢ 𝑆 = inf(𝑅, ℝ, < ) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) | ||
| Theorem | minveco 31468* | 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.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ (𝜑 → 𝑈 ∈ CPreHilOLD) & ⊢ (𝜑 → 𝑊 ∈ ((SubSp‘𝑈) ∩ CBan)) & ⊢ (𝜑 → 𝐴 ∈ 𝑋) ⇒ ⊢ (𝜑 → ∃!𝑥 ∈ 𝑌 ∀𝑦 ∈ 𝑌 (𝑁‘(𝐴𝑀𝑥)) ≤ (𝑁‘(𝐴𝑀𝑦))) | ||
| Syntax | chlo 31469 | Extend class notation with the class of all complex Hilbert spaces. |
| class CHilOLD | ||
| Definition | df-hlo 31470 | Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ CHilOLD = (CBan ∩ CPreHilOLD) | ||
| Theorem | ishlo 31471 | The predicate "is a complex 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.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CHilOLD ↔ (𝑈 ∈ CBan ∧ 𝑈 ∈ CPreHilOLD)) | ||
| Theorem | hlobn 31472 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CBan) | ||
| Theorem | hlph 31473 | Every complex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CPreHilOLD) | ||
| Theorem | hlrel 31474 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| ⊢ Rel CHilOLD | ||
| Theorem | hlnv 31475 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec) | ||
| Theorem | hlnvi 31476 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
| Theorem | hlvc 31477 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑊 = (1st ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑊 ∈ CVecOLD) | ||
| Theorem | hlcmet 31478 | The induced metric on a complex Hilbert space is complete. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝐷 ∈ (CMet‘𝑋)) | ||
| Theorem | hlmet 31479 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝐷 ∈ (Met‘𝑋)) | ||
| Theorem | hlpar2 31480 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝑀𝐵))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
| Theorem | hlpar 31481 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (((𝑁‘(𝐴𝐺𝐵))↑2) + ((𝑁‘(𝐴𝐺(-1𝑆𝐵)))↑2)) = (2 · (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2)))) | ||
| Theorem | hlex 31482 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ 𝑋 ∈ V | ||
| Theorem | hladdf 31483 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | hlcom 31484 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
| Theorem | hlass 31485 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
| Theorem | hl0cl 31486 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋) | ||
| Theorem | hladdid 31487 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) | ||
| Theorem | hlmulf 31488 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
| Theorem | hlmulid 31489 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (1𝑆𝐴) = 𝐴) | ||
| Theorem | hlmulass 31490 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 · 𝐵)𝑆𝐶) = (𝐴𝑆(𝐵𝑆𝐶))) | ||
| Theorem | hldi 31491 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑆(𝐵𝐺𝐶)) = ((𝐴𝑆𝐵)𝐺(𝐴𝑆𝐶))) | ||
| Theorem | hldir 31492 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → ((𝐴 + 𝐵)𝑆𝐶) = ((𝐴𝑆𝐶)𝐺(𝐵𝑆𝐶))) | ||
| Theorem | hlmul0 31493 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (0𝑆𝐴) = 𝑍) | ||
| Theorem | hlipf 31494 | Mapping for Hilbert space inner product. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑃:(𝑋 × 𝑋)⟶ℂ) | ||
| Theorem | hlipcj 31495 | Conjugate law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝑃𝐵) = (∗‘(𝐵𝑃𝐴))) | ||
| Theorem | hlipdir 31496 | Distributive law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶))) | ||
| Theorem | hlipass 31497 | Associative law for Hilbert space inner product. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑆𝐵)𝑃𝐶) = (𝐴 · (𝐵𝑃𝐶))) | ||
| Theorem | hlipgt0 31498 | The inner product of a Hilbert space vector by itself is positive. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐴 ≠ 𝑍) → 0 < (𝐴𝑃𝐴)) | ||
| Theorem | hlcompl 31499 | Completeness of a Hilbert space. (Contributed by NM, 8-Sep-2007.) (Revised by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐹 ∈ (Cau‘𝐷)) → 𝐹 ∈ dom (⇝𝑡‘𝐽)) | ||
| Theorem | cnchl 31500 | The set of complex numbers is a complex Hilbert space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 = ⟨⟨ + , · ⟩, abs⟩ ⇒ ⊢ 𝑈 ∈ CHilOLD | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |