Home | Metamath
Proof Explorer Theorem List (p. 271 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nmoofval 27001* | The operator norm function. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑁 = (𝑡 ∈ (𝑌 ↑𝑚 𝑋) ↦ sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑡‘𝑧)))}, ℝ*, < ))) | ||
Theorem | nmooval 27002* | The operator norm function. (Contributed by NM, 27-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) = sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑇‘𝑧)))}, ℝ*, < )) | ||
Theorem | nmosetre 27003* | The set in the supremum of the operator norm definition df-nmoo 26984 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (normCV‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ) | ||
Theorem | nmosetn0 27004* | The set in the supremum of the operator norm definition df-nmoo 26984 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))}) | ||
Theorem | nmoxr 27005 | The norm of an operator is an extended real. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑁‘𝑇) ∈ ℝ*) | ||
Theorem | nmooge0 27006 | The norm of an operator is nonnegative. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → 0 ≤ (𝑁‘𝑇)) | ||
Theorem | nmorepnf 27007 | The norm of an operator is either real or plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → ((𝑁‘𝑇) ∈ ℝ ↔ (𝑁‘𝑇) ≠ +∞)) | ||
Theorem | nmoreltpnf 27008 | The norm of any operator is real iff it is less than plus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → ((𝑁‘𝑇) ∈ ℝ ↔ (𝑁‘𝑇) < +∞)) | ||
Theorem | nmogtmnf 27009 | The norm of an operator is greater than minus infinity. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → -∞ < (𝑁‘𝑇)) | ||
Theorem | nmoolb 27010 | A lower bound for an operator norm. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) ∧ (𝐴 ∈ 𝑋 ∧ (𝐿‘𝐴) ≤ 1)) → (𝑀‘(𝑇‘𝐴)) ≤ (𝑁‘𝑇)) | ||
Theorem | nmoubi 27011* | An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ*) → ((𝑁‘𝑇) ≤ 𝐴 ↔ ∀𝑥 ∈ 𝑋 ((𝐿‘𝑥) ≤ 1 → (𝑀‘(𝑇‘𝑥)) ≤ 𝐴))) | ||
Theorem | nmoub3i 27012* | An upper bound for an operator norm. (Contributed by NM, 12-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ 𝐴 ∈ ℝ ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ (abs‘𝐴)) | ||
Theorem | nmoub2i 27013* | An upper bound for an operator norm. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐿‘𝑥))) → (𝑁‘𝑇) ≤ 𝐴) | ||
Theorem | nmobndi 27014* | Two ways to express that an operator is bounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇:𝑋⟶𝑌 → ((𝑁‘𝑇) ∈ ℝ ↔ ∃𝑟 ∈ ℝ ∀𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 → (𝑀‘(𝑇‘𝑦)) ≤ 𝑟))) | ||
Theorem | nmounbi 27015* | Two ways two express that an operator is unbounded. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇:𝑋⟶𝑌 → ((𝑁‘𝑇) = +∞ ↔ ∀𝑟 ∈ ℝ ∃𝑦 ∈ 𝑋 ((𝐿‘𝑦) ≤ 1 ∧ 𝑟 < (𝑀‘(𝑇‘𝑦))))) | ||
Theorem | nmounbseqi 27016* | An unbounded operator determines an unbounded sequence. (Contributed by NM, 11-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘)))))) | ||
Theorem | nmounbseqiALT 27017* | Alternate shorter proof of nmounbseqi 27016 based on axioms ax-reg 8380 and ax-ac2 9168 instead of ax-cc 9140. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘)))))) | ||
Theorem | nmobndseqi 27018* | A bounded sequence determines a bounded operator. (Contributed by NM, 18-Jan-2008.) (Revised by Mario Carneiro, 7-Apr-2013.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ) | ||
Theorem | nmobndseqiALT 27019* | Alternate shorter proof of nmobndseqi 27018 based on axioms ax-reg 8380 and ax-ac2 9168 instead of ax-cc 9140. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ) | ||
Theorem | bloval 27020* | The class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐵 = {𝑡 ∈ 𝐿 ∣ (𝑁‘𝑡) < +∞}) | ||
Theorem | isblo 27021 | The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) < +∞))) | ||
Theorem | isblo2 27022 | The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) ∈ ℝ))) | ||
Theorem | bloln 27023 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿) | ||
Theorem | blof 27024 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶𝑌) | ||
Theorem | nmblore 27025 | The norm of a bounded operator is a real number. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → (𝑁‘𝑇) ∈ ℝ) | ||
Theorem | 0ofval 27026 | The zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝑂 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑂 = (𝑋 × {𝑍})) | ||
Theorem | 0oval 27027 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝑂 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = 𝑍) | ||
Theorem | 0oo 27028 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌) | ||
Theorem | 0lno 27029 | The zero operator is linear. (Contributed by NM, 28-Nov-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐿) | ||
Theorem | nmoo0 27030 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0) | ||
Theorem | 0blo 27031 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐵) | ||
Theorem | nmlno0lem 27032 | Lemma for nmlno0i 27033. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 & ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝑃 = (0vec‘𝑈) & ⊢ 𝑄 = (0vec‘𝑊) & ⊢ 𝐾 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) ⇒ ⊢ ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍) | ||
Theorem | nmlno0i 27033 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇 ∈ 𝐿 → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) | ||
Theorem | nmlno0 27034 | The norm of a linear operator is zero iff the operator is zero. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → ((𝑁‘𝑇) = 0 ↔ 𝑇 = 𝑍)) | ||
Theorem | nmlnoubi 27035* | An upper bound for the operator norm of a linear operator, using only the properties of nonzero arguments. (Contributed by NM, 1-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝐾 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐿 ∧ (𝐴 ∈ ℝ ∧ 0 ≤ 𝐴) ∧ ∀𝑥 ∈ 𝑋 (𝑥 ≠ 𝑍 → (𝑀‘(𝑇‘𝑥)) ≤ (𝐴 · (𝐾‘𝑥)))) → (𝑁‘𝑇) ≤ 𝐴) | ||
Theorem | nmlnogt0 27036 | The norm of a nonzero linear operator is positive. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇 ≠ 𝑍 ↔ 0 < (𝑁‘𝑇))) | ||
Theorem | lnon0 27037* | The domain of a nonzero linear operator contains a nonzero vector. (Contributed by NM, 15-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑂 = (𝑈 0op 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ 𝑇 ≠ 𝑂) → ∃𝑥 ∈ 𝑋 𝑥 ≠ 𝑍) | ||
Theorem | nmblolbii 27038 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 7-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐵 ⇒ ⊢ (𝐴 ∈ 𝑋 → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴))) | ||
Theorem | nmblolbi 27039 | A lower bound for the norm of a bounded linear operator. (Contributed by NM, 10-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐵 ∧ 𝐴 ∈ 𝑋) → (𝑀‘(𝑇‘𝐴)) ≤ ((𝑁‘𝑇) · (𝐿‘𝐴))) | ||
Theorem | isblo3i 27040* | The predicate "is a bounded linear operator." Definition 2.7-1 of [Kreyszig] p. 91. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ ∃𝑥 ∈ ℝ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝑥 · (𝑀‘𝑦)))) | ||
Theorem | blo3i 27041* | Properties that determine a bounded linear operator. (Contributed by NM, 13-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) & ⊢ 𝑁 = (normCV‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐿 ∧ 𝐴 ∈ ℝ ∧ ∀𝑦 ∈ 𝑋 (𝑁‘(𝑇‘𝑦)) ≤ (𝐴 · (𝑀‘𝑦))) → 𝑇 ∈ 𝐵) | ||
Theorem | blometi 27042 | Upper bound for the distance between the values of a bounded linear operator. (Contributed by NM, 11-Dec-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇 ∈ 𝐵 ∧ 𝑃 ∈ 𝑋 ∧ 𝑄 ∈ 𝑋) → ((𝑇‘𝑃)𝐷(𝑇‘𝑄)) ≤ ((𝑁‘𝑇) · (𝑃𝐶𝑄))) | ||
Theorem | blocnilem 27043 | Lemma for blocni 27044 and lnocni 27045. If a linear operator is continuous at any point, it is bounded. (Contributed by NM, 17-Dec-2007.) (Revised by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
⊢ 𝐶 = (IndMet‘𝑈) & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐽 = (MetOpen‘𝐶) & ⊢ 𝐾 = (MetOpen‘𝐷) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑇 ∈ 𝐿 & ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑃 ∈ 𝑋 ∧ 𝑇 ∈ ((𝐽 CnP 𝐾)‘𝑃)) → 𝑇 ∈ 𝐵) | ||
Theorem | blocni 27044 | 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 27045 | 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 27046 | 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 27047 | 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 27048* | 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 27049* | 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 27050 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
⊢ 𝐻 = (HmOp‘𝑈) & ⊢ 𝐴 = (𝑈adj𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑇 ∈ 𝐻 ↔ (𝑇 ∈ dom 𝐴 ∧ (𝐴‘𝑇) = 𝑇))) | ||
Syntax | ccphlo 27051 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
class CPreHilOLD | ||
Definition | df-ph 27052* | 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 27053 | 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 27054 | 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 27055 | 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 27056* | 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 27057 | 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 27058 | 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 27059 | 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 27060 | 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 27061* | 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 27062 | 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 27063 | 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 27064 | 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 27065 | Lemma for ip1i 27066. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐽 ∈ ℂ ⇒ ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶)) | ||
Theorem | ip1i 27066 | 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 27067 | 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 27068 | Lemma for ipdiri 27069. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)) | ||
Theorem | ipdiri 27069 | 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 27070 | Lemma for ipassi 27080. 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 27071 | Lemma for ipassi 27080. 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 27072 | Lemma for ipassi 27080. 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 27073 | Lemma for ipassi 27080. 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 27074 | Lemma for ipassi 27080. 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 27075* | Lemma for ipassi 27080. 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 27076* | Lemma for ipassi 27080. By ipasslem5 27074, 𝐹 is 0 for all ℚ; since it is continuous and ℚ is dense in ℝ by qdensere2 22408, 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 27077 | Lemma for ipassi 27080. Conclude from ipasslem8 27076 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (𝐶 ∈ ℝ → ((𝐶𝑆𝐴)𝑃𝐵) = (𝐶 · (𝐴𝑃𝐵))) | ||
Theorem | ipasslem10 27078 | Lemma for ipassi 27080. 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 27079 | Lemma for ipassi 27080. 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 27080 | 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 27081 | 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 27082 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝐺𝐶)) = ((𝐴𝑃𝐵) + (𝐴𝑃𝐶))) | ||
Theorem | ip2dii 27083 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝐷 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃(𝐶𝐺𝐷)) = (((𝐴𝑃𝐶) + (𝐵𝑃𝐷)) + ((𝐴𝑃𝐷) + (𝐵𝑃𝐶))) | ||
Theorem | dipass 27084 | 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 27085 | "Associative" law for second argument of inner product (compare dipass 27084). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑆𝐶)) = ((∗‘𝐵) · (𝐴𝑃𝐶))) | ||
Theorem | dipassr2 27086 | "Associative" law for inner product. Conjugate version of dipassr 27085. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃((∗‘𝐵)𝑆𝐶)) = (𝐵 · (𝐴𝑃𝐶))) | ||
Theorem | dipsubdir 27087 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → ((𝐴𝑀𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) − (𝐵𝑃𝐶))) | ||
Theorem | dipsubdi 27088 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝐴𝑃(𝐵𝑀𝐶)) = ((𝐴𝑃𝐵) − (𝐴𝑃𝐶))) | ||
Theorem | pythi 27089 | 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. This is Metamath 100 proof #4. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ ((𝐴𝑃𝐵) = 0 → ((𝑁‘(𝐴𝐺𝐵))↑2) = (((𝑁‘𝐴)↑2) + ((𝑁‘𝐵)↑2))) | ||
Theorem | siilem1 27090 | Lemma for sii 27093. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝐶 ∈ ℂ & ⊢ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ & ⊢ 0 ≤ (𝐶 · (𝐴𝑃𝐵)) ⇒ ⊢ ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
Theorem | siilem2 27091 | Lemma for sii 27093. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) ⇒ ⊢ ((𝐶 ∈ ℂ ∧ (𝐶 · (𝐴𝑃𝐵)) ∈ ℝ ∧ 0 ≤ (𝐶 · (𝐴𝑃𝐵))) → ((𝐵𝑃𝐴) = (𝐶 · ((𝑁‘𝐵)↑2)) → (√‘((𝐴𝑃𝐵) · (𝐶 · ((𝑁‘𝐵)↑2)))) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)))) | ||
Theorem | siii 27092 | Inference from sii 27093. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 ⇒ ⊢ (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵)) | ||
Theorem | sii 27093 | 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 27361, bcsiALT 27420, bcsiHIL 27421, csbren 22990. This is Metamath 100 proof #78. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋) → (abs‘(𝐴𝑃𝐵)) ≤ ((𝑁‘𝐴) · (𝑁‘𝐵))) | ||
Theorem | sspph 27094 | A subspace of an inner product space is an inner product space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ 𝐻) → 𝑊 ∈ CPreHilOLD) | ||
Theorem | ipblnfi 27095* | 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 27096* | 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 27097* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ((𝑆:𝑌⟶𝑋 ∧ 𝑇:𝑌⟶𝑋) → (∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 (𝑥𝑃(𝑆‘𝑦)) = (𝑥𝑃(𝑇‘𝑦)) ↔ 𝑆 = 𝑇)) | ||
Theorem | ajmoi 27098* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD ⇒ ⊢ ∃*𝑠(𝑠:𝑌⟶𝑋 ∧ ∀𝑥 ∈ 𝑋 ∀𝑦 ∈ 𝑌 ((𝑇‘𝑥)𝑄𝑦) = (𝑥𝑃(𝑠‘𝑦))) | ||
Theorem | ajfuni 27099 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
⊢ 𝐴 = (𝑈adj𝑊) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ Fun 𝐴 | ||
Theorem | ajfun 27100 | The adjoint function is a function. This is not immediately apparent from df-aj 26989 but results from the uniqueness shown by ajmoi 27098. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
⊢ 𝐴 = (𝑈adj𝑊) ⇒ ⊢ ((𝑈 ∈ CPreHilOLD ∧ 𝑊 ∈ NrmCVec) → Fun 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |