HomeTheorem List (p. 310 of 503)
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. 310 of 503) | < 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-31014) |
Hilbert Space Explorer
(31015-32537) |
Users' Mathboxes
(32538-50296) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | blocni 30901 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 ⇒ ⊢ (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵) | ||
| Theorem | lnocni 30902 | If a linear operator is continuous at any point, it is continuous everywhere. Theorem 2.7-9(b) of [Kreyszig] p. 97. (Contributed by NM, 18-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 & ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | blocn 30903 | A linear operator is continuous iff it is bounded. Theorem 2.7-9(a) of [Kreyszig] p. 97. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (𝑇 ∈ 𝐿 → (𝑇 ∈ (𝐽 Cn 𝐾) ↔ 𝑇 ∈ 𝐵)) | ||
| Theorem | blocn2 30904 | A bounded linear operator is continuous. (Contributed by NM, 25-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇 ∈ 𝐵 → 𝑇 ∈ (𝐽 Cn 𝐾)) | ||
| Theorem | ajfval 30905* | The adjoint function. (Contributed by NM, 25-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑄 = (·𝑖OLD‘𝑊) & ⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐴 = {⟨𝑡, 𝑠⟩ ∣ (𝑡:𝑋⟶𝑌 ∧ 𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑡‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦)))}) | ||
| Theorem | hmoval 30906* | The set of Hermitian (self-adjoint) operators on a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝐻 = (HmOp‘𝑈) & ⊢ 𝐴 = (𝑈adj𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → 𝐻 = {𝑡 ∈ dom 𝐴 ∣ (𝐴‘𝑡) = 𝑡}) | ||
| Theorem | ishmo 30907 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (HmOp‘𝑈) & ⊢ 𝐴 = (𝑈adj𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑇 ∈ 𝐻 ↔ (𝑇 ∈ dom 𝐴 ∧ (𝐴‘𝑇) = 𝑇))) | ||
| Syntax | ccphlo 30908 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
| class CPreHilOLD | ||
| Definition | df-ph 30909* | Define the class of all complex inner product spaces. An inner product space is a normed vector space whose norm satisfies the parallelogram law (a property that induces an inner product). Based on Exercise 4(b) of [ReedSimon] p. 63. The vector 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.) |
| ⊢ CPreHilOLD = (NrmCVec ∩ {⟨⟨𝑔, 𝑠⟩, 𝑛⟩ ∣ ∀𝑥 ∈ ran 𝑔∀𝑦 ∈ ran 𝑔(((𝑛‘(𝑥𝑔𝑦))↑2) + ((𝑛‘(𝑥𝑔(-1𝑠𝑦)))↑2)) = (2 · (((𝑛‘𝑥)↑2) + ((𝑛‘𝑦)↑2)))}) | ||
| Theorem | phnv 30910 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CPreHilOLD → 𝑈 ∈ NrmCVec) | ||
| Theorem | phrel 30911 | The class of all complex inner product spaces is a relation. (Contributed by NM, 2-Apr-2007.) (New usage is discouraged.) |
| ⊢ Rel CPreHilOLD | ||
| Theorem | phnvi 30912 | Every complex inner product space is a normed complex vector space. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
| Theorem | isphg 30913* | 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 30914 | 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 30915 | 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 30916 | 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 30917 | 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 30918* | 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 30919 | 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 30920 | 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 30921 | 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 30922 | Lemma for ip1i 30923. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐽 ∈ ℂ ⇒ ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶)) | ||
| Theorem | ip1i 30923 | 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 30924 | 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 30925 | Lemma for ipdiri 30926. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)) | ||
| Theorem | ipdiri 30926 | 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 30927 | Lemma for ipassi 30937. 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 30928 | Lemma for ipassi 30937. 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 30929 | Lemma for ipassi 30937. 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 30930 | Lemma for ipassi 30937. 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 30931 | Lemma for ipassi 30937. 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 30932* | Lemma for ipassi 30937. 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 30933* | Lemma for ipassi 30937. By ipasslem5 30931, 𝐹 is 0 for all ℚ; since it is continuous and ℚ is dense in ℝ by qdensere2 24787, 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 30934 | Lemma for ipassi 30937. Conclude from ipasslem8 30933 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (𝐶 ∈ ℝ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵))) | ||
| Theorem | ipasslem10 30935 | Lemma for ipassi 30937. 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 30936 | Lemma for ipassi 30937. 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 30937 | 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 30938 | 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 30939 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝐺𝐶)) = ((𝐴𝑃𝐵) + (𝐴𝑃𝐶))) | ||
| Theorem | ip2dii 30940 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝐷 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃(𝐶𝐺𝐷)) = (((𝐴𝑃𝐶) + (𝐵𝑃𝐷)) + ((𝐴𝑃𝐷) + (𝐵𝑃𝐶))) | ||
| Theorem | dipass 30941 | 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 30942 | "Associative" law for second argument of inner product (compare dipass 30941). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑆𝐶)) = ((∗‘𝐵) · (𝐴𝑃𝐶))) | ||
| Theorem | dipassr2 30943 | "Associative" law for inner product. Conjugate version of dipassr 30942. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃((∗‘𝐵)𝑆𝐶)) = (𝐵 · (𝐴𝑃𝐶))) | ||
| Theorem | dipsubdir 30944 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) − (𝐵𝑃𝐶))) | ||
| Theorem | dipsubdi 30945 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) | ||
| Theorem | pythi 30946 | 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 30947 | Lemma for sii 30950. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ & ⊢ 0 ≤ (𝐶 · (𝐴𝑃𝐵)) ⇒ ⊢ ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
| Theorem | siilem2 30948 | Lemma for sii 30950. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝐶 ∈ ℂ ∧ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ ∧ 0 ≤ (𝐶 · (𝐴𝑃𝐵))) → ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))) | ||
| Theorem | siii 30949 | Inference from sii 30950. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)) | ||
| Theorem | sii 30950 | Obsolete version of ipcau 25230 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 31216, bcsiALT 31275, bcsiHIL 31276, csbren 25391. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
| Theorem | ipblnfi 30951* | 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 30952* | 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 30953* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇)) | ||
| Theorem | ajmoi 30954* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ∃*𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) | ||
| Theorem | ajfuni 30955 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝑈adj𝑊) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ Fun 𝐴 | ||
| Theorem | ajfun 30956 | The adjoint function is a function. This is not immediately apparent from df-aj 30846 but results from the uniqueness shown by ajmoi 30954. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec) → Fun 𝐴) | ||
| Theorem | ajval 30957* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑄 = (·𝑖OLD‘𝑊) & ⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝐴‘𝑇) = (℩𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))))) | ||
| Syntax | ccbn 30958 | Extend class notation with the class of all complex Banach spaces. |
| class CBan | ||
| Definition | df-cbn 30959 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25328 instead. (New usage is discouraged.) |
| ⊢ CBan = {𝑢 ∈ NrmCVec ∣ (IndMet‘𝑢) ∈ (CMet‘(BaseSet‘𝑢))} | ||
| Theorem | iscbn 30960 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25330 instead. (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CBan ↔ (𝑈 ∈ NrmCVec ∧ 𝐷 ∈ (CMet‘𝑋))) | ||
| Theorem | cbncms 30961 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25339 (or preferably bncms 25336) instead. (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CBan → 𝐷 ∈ (CMet‘𝑋)) | ||
| Theorem | bnnv 30962 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25332 instead. (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CBan → 𝑈 ∈ NrmCVec) | ||
| Theorem | bnrel 30963 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| ⊢ Rel CBan | ||
| Theorem | bnsscmcl 30964 | 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 30965 | 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 30966* | Lemma for ubth 30969. 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 25322, 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 30967* | Lemma for ubth 30969. 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 30968* | Lemma for ubth 30969. Prove the reverse implication, using nmblolbi 30896. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐽 = (MetOpen‘𝐷) & ⊢ 𝑈 ∈ CBan & ⊢ 𝑊 ∈ NrmCVec & ⊢ (𝜑 → 𝑇 ⊆ (𝑈 BLnOp 𝑊)) ⇒ ⊢ (𝜑 → (∀𝑥 ∈ 𝑋 ∃𝑐 ∈ ℝ ∀𝑡 ∈ 𝑇 (𝑁‘(𝑡‘𝑥)) ≤ 𝑐 ↔ ∃𝑑 ∈ ℝ ∀𝑡 ∈ 𝑇 ((𝑈 normOpOLD 𝑊)‘𝑡) ≤ 𝑑)) | ||
| Theorem | ubth 30969* | 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 30970* | Lemma for minveco 30980. 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 30971* | Lemma for minveco 30980. 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 30972* | Lemma for minveco 30980. 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 30973* | Lemma for minveco 30980. 𝐹 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 30974* | Lemma for minveco 30980. 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 30975* | Lemma for minveco 30980. 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 30976* | Lemma for minveco 30980. 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 30977* | Lemma for minveco 30980. Discharge the assumption about the sequence 𝐹 by applying countable choice ax-cc 10355. (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 30978* | Lemma for minveco 30980. 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 30979* | Lemma for minveco 30980. 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 30980* | 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 30981 | Extend class notation with the class of all complex Hilbert spaces. |
| class CHilOLD | ||
| Definition | df-hlo 30982 | 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 30983 | 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 30984 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ CBan) | ||
| Theorem | hlph 30985 | 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 30986 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| ⊢ Rel CHilOLD | ||
| Theorem | hlnv 30987 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
| ⊢ (𝑈 ∈ CHilOLD → 𝑈 ∈ NrmCVec) | ||
| Theorem | hlnvi 30988 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
| ⊢ 𝑈 ∈ CHilOLD ⇒ ⊢ 𝑈 ∈ NrmCVec | ||
| Theorem | hlvc 30989 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑊 = (1st ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑊 ∈ CVecOLD) | ||
| Theorem | hlcmet 30990 | 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 30991 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝐷 ∈ (Met‘𝑋)) | ||
| Theorem | hlpar2 30992 | 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 30993 | 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 30994 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ 𝑋 ∈ V | ||
| Theorem | hladdf 30995 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝐺:(𝑋 × 𝑋)⟶𝑋) | ||
| Theorem | hlcom 30996 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (𝐴𝐺𝐵) = (𝐵𝐺𝐴)) | ||
| Theorem | hlass 30997 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝐺𝐵)𝐺𝐶) = (𝐴𝐺(𝐵𝐺𝐶))) | ||
| Theorem | hl0cl 30998 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑍 ∈ 𝑋) | ||
| Theorem | hladdid 30999 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) ⇒ ⊢ ((𝑈 ∈ CHilOLD ∧ 𝐴 ∈ 𝑋) → (𝐴𝐺𝑍) = 𝐴) | ||
| Theorem | hlmulf 31000 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ (𝑈 ∈ CHilOLD → 𝑆:(ℂ × 𝑋)⟶𝑋) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |