HomeTheorem List (p. 291 of 464)
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. 291 of 464) | < 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-29181) |
Hilbert Space Explorer
(29182-30704) |
Users' Mathboxes
(30705-46395) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | sspimsval 29001 | The induced metric on a subspace in terms of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) ∧ (𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌)) → (𝐴𝐶𝐵) = (𝐴𝐷𝐵)) | ||
| Theorem | sspims 29002 | The induced metric on a subspace is a restriction of the induced metric on the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐷 = (IndMet‘𝑈) & ⊢ 𝐶 = (IndMet‘𝑊) & ⊢ 𝐻 = (SubSp‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ 𝐻) → 𝐶 = (𝐷 ↾ (𝑌 × 𝑌))) | ||
| Syntax | clno 29003 | Extend class notation with the class of linear operators on normed complex vector spaces. |
| class LnOp | ||
| Syntax | cnmoo 29004 | Extend class notation with the class of operator norms on normed complex vector spaces. |
| class normOpOLD | ||
| Syntax | cblo 29005 | Extend class notation with the class of bounded linear operators on normed complex vector spaces. |
| class BLnOp | ||
| Syntax | c0o 29006 | Extend class notation with the class of zero operators on normed complex vector spaces. |
| class 0op | ||
| Definition | df-lno 29007* | Define the class of linear operators between two normed complex vector spaces. In the literature, an operator may be a partial function, i.e., the domain of an operator is not necessarily the entire vector space. However, since the domain of a linear operator is a vector subspace, we define it with a complete function for convenience and will use subset relations to specify the partial function case. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ LnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ (BaseSet‘𝑢)∀𝑧 ∈ (BaseSet‘𝑢)(𝑡‘((𝑥( ·𝑠OLD ‘𝑢)𝑦)( +𝑣 ‘𝑢)𝑧)) = ((𝑥( ·𝑠OLD ‘𝑤)(𝑡‘𝑦))( +𝑣 ‘𝑤)(𝑡‘𝑧))}) | ||
| Definition | df-nmoo 29008* | Define the norm of an operator between two normed complex vector spaces. This definition produces an operator norm function for each pair of vector spaces ⟨𝑢, 𝑤⟩. Based on definition of linear operator norm in [AkhiezerGlazman] p. 39, although we define it for all operators for convenience. It isn't necessarily meaningful for nonlinear operators, since it doesn't take into account operator values at vectors with norm greater than 1. See Equation 2 of [Kreyszig] p. 92 for a definition that does (although it ignores the value at the zero vector). However, operator norms are rarely if ever used for nonlinear operators. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ normOpOLD = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ (𝑡 ∈ ((BaseSet‘𝑤) ↑m (BaseSet‘𝑢)) ↦ sup({𝑥 ∣ ∃𝑧 ∈ (BaseSet‘𝑢)(((normCV‘𝑢)‘𝑧) ≤ 1 ∧ 𝑥 = ((normCV‘𝑤)‘(𝑡‘𝑧)))}, ℝ*, < ))) | ||
| Definition | df-blo 29009* | Define the class of bounded linear operators between two normed complex vector spaces. (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ BLnOp = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {𝑡 ∈ (𝑢 LnOp 𝑤) ∣ ((𝑢 normOpOLD 𝑤)‘𝑡) < +∞}) | ||
| Definition | df-0o 29010* | Define the zero operator between two normed complex vector spaces. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 0op = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ ((BaseSet‘𝑢) × {(0vec‘𝑤)})) | ||
| Syntax | caj 29011 | Adjoint of an operator. |
| class adj | ||
| Syntax | chmo 29012 | Set of Hermitional (self-adjoint) operators. |
| class HmOp | ||
| Definition | df-aj 29013* | Define the adjoint of an operator (if it exists). The domain of 𝑈adj𝑊 is the set of all operators from 𝑈 to 𝑊 that have an adjoint. Definition 3.9-1 of [Kreyszig] p. 196, although we don't require that 𝑈 and 𝑊 be Hilbert spaces nor that the operators be linear. Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
| ⊢ adj = (𝑢 ∈ NrmCVec, 𝑤 ∈ NrmCVec ↦ {⟨𝑡, 𝑠⟩ ∣ (𝑡:(BaseSet‘𝑢)⟶(BaseSet‘𝑤) ∧ 𝑠:(BaseSet‘𝑤)⟶(BaseSet‘𝑢) ∧ ∀𝑥 ∈ (BaseSet‘𝑢)∀𝑦 ∈ (BaseSet‘𝑤)((𝑡‘𝑥)(·𝑖OLD‘𝑤)𝑦) = (𝑥(·𝑖OLD‘𝑢)(𝑠‘𝑦)))}) | ||
| Definition | df-hmo 29014* | Define the set of Hermitian (self-adjoint) operators on a normed complex vector space (normally a Hilbert space). Although we define it for any normed vector space for convenience, the definition is meaningful only for inner product spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ HmOp = (𝑢 ∈ NrmCVec ↦ {𝑡 ∈ dom (𝑢adj𝑢) ∣ ((𝑢adj𝑢)‘𝑡) = 𝑡}) | ||
| Theorem | lnoval 29015* | The set of 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.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝐿 = {𝑡 ∈ (𝑌 ↑m 𝑋) ∣ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑡‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑡‘𝑦))𝐻(𝑡‘𝑧))}) | ||
| Theorem | islno 29016* | The predicate "is a linear operator." (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐿 ↔ (𝑇:𝑋⟶𝑌 ∧ ∀𝑥 ∈ ℂ ∀𝑦 ∈ 𝑋 ∀𝑧 ∈ 𝑋 (𝑇‘((𝑥𝑅𝑦)𝐺𝑧)) = ((𝑥𝑆(𝑇‘𝑦))𝐻(𝑇‘𝑧))))) | ||
| Theorem | lnolin 29017 | Basic linearity property of a linear operator. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋 ∧ 𝐶 ∈ 𝑋)) → (𝑇‘((𝐴𝑅𝐵)𝐺𝐶)) = ((𝐴𝑆(𝑇‘𝐵))𝐻(𝑇‘𝐶))) | ||
| Theorem | lnof 29018 | A linear operator is a mapping. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → 𝑇:𝑋⟶𝑌) | ||
| Theorem | lno0 29019 | The value of a linear operator at zero is zero. (Contributed by NM, 4-Dec-2007.) (Revised by Mario Carneiro, 18-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑄 = (0vec‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) → (𝑇‘𝑄) = 𝑍) | ||
| Theorem | lnocoi 29020 | The composition of two linear operators is linear. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝑀 = (𝑊 LnOp 𝑋) & ⊢ 𝑁 = (𝑈 LnOp 𝑋) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec & ⊢ 𝑋 ∈ NrmCVec & ⊢ 𝑆 ∈ 𝐿 & ⊢ 𝑇 ∈ 𝑀 ⇒ ⊢ (𝑇 ∘ 𝑆) ∈ 𝑁 | ||
| Theorem | lnoadd 29021 | Addition property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝐻 = ( +𝑣 ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝐺𝐵)) = ((𝑇‘𝐴)𝐻(𝑇‘𝐵))) | ||
| Theorem | lnosub 29022 | Subtraction property of a linear operator. (Contributed by NM, 7-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑀 = ( −𝑣 ‘𝑈) & ⊢ 𝑁 = ( −𝑣 ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ 𝑋 ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝑀𝐵)) = ((𝑇‘𝐴)𝑁(𝑇‘𝐵))) | ||
| Theorem | lnomul 29023 | Scalar multiplication property of a linear operator. (Contributed by NM, 5-Dec-2007.) (Revised by Mario Carneiro, 19-Nov-2013.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑅 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) ⇒ ⊢ (((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐿) ∧ (𝐴 ∈ ℂ ∧ 𝐵 ∈ 𝑋)) → (𝑇‘(𝐴𝑅𝐵)) = (𝐴𝑆(𝑇‘𝐵))) | ||
| Theorem | nvo00 29024 | Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → (𝑇 = (𝑋 × {𝑍}) ↔ ran 𝑇 = {𝑍})) | ||
| Theorem | nmoofval 29025* | 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) → 𝑁 = (𝑡 ∈ (𝑌 ↑m 𝑋) ↦ sup({𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝐿‘𝑧) ≤ 1 ∧ 𝑥 = (𝑀‘(𝑡‘𝑧)))}, ℝ*, < ))) | ||
| Theorem | nmooval 29026* | 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 29027* | The set in the supremum of the operator norm definition df-nmoo 29008 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑁 = (normCV‘𝑊) ⇒ ⊢ ((𝑊 ∈ NrmCVec ∧ 𝑇:𝑋⟶𝑌) → {𝑥 ∣ ∃𝑧 ∈ 𝑋 ((𝑀‘𝑧) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑧)))} ⊆ ℝ) | ||
| Theorem | nmosetn0 29028* | The set in the supremum of the operator norm definition df-nmoo 29008 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑈) & ⊢ 𝑀 = (normCV‘𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑁‘(𝑇‘𝑍)) ∈ {𝑥 ∣ ∃𝑦 ∈ 𝑋 ((𝑀‘𝑦) ≤ 1 ∧ 𝑥 = (𝑁‘(𝑇‘𝑦)))}) | ||
| Theorem | nmoxr 29029 | 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 29030 | 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 29031 | 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 29032 | 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 29033 | 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 29034 | 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 29035* | 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 29036* | 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 29037* | 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 29038* | 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 29039* | 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 29040* | 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 29041* | Alternate shorter proof of nmounbseqi 29040 based on Axioms ax-reg 9281 and ax-ac2 10150 instead of ax-cc 10122. (Contributed by NM, 11-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ (𝑁‘𝑇) = +∞) → ∃𝑓(𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ ((𝐿‘(𝑓‘𝑘)) ≤ 1 ∧ 𝑘 < (𝑀‘(𝑇‘(𝑓‘𝑘)))))) | ||
| Theorem | nmobndseqi 29042* | 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 29043* | Alternate shorter proof of nmobndseqi 29042 based on Axioms ax-reg 9281 and ax-ac2 10150 instead of ax-cc 10122. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐿 = (normCV‘𝑈) & ⊢ 𝑀 = (normCV‘𝑊) & ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑈 ∈ NrmCVec & ⊢ 𝑊 ∈ NrmCVec ⇒ ⊢ ((𝑇:𝑋⟶𝑌 ∧ ∀𝑓((𝑓:ℕ⟶𝑋 ∧ ∀𝑘 ∈ ℕ (𝐿‘(𝑓‘𝑘)) ≤ 1) → ∃𝑘 ∈ ℕ (𝑀‘(𝑇‘(𝑓‘𝑘))) ≤ 𝑘)) → (𝑁‘𝑇) ∈ ℝ) | ||
| Theorem | bloval 29044* | 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 29045 | The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) < +∞))) | ||
| Theorem | isblo2 29046 | The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑇 ∈ 𝐵 ↔ (𝑇 ∈ 𝐿 ∧ (𝑁‘𝑇) ∈ ℝ))) | ||
| Theorem | bloln 29047 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝐿 = (𝑈 LnOp 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇 ∈ 𝐿) | ||
| Theorem | blof 29048 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝑇 ∈ 𝐵) → 𝑇:𝑋⟶𝑌) | ||
| Theorem | nmblore 29049 | 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 29050 | 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 29051 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑍 = (0vec‘𝑊) & ⊢ 𝑂 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec ∧ 𝐴 ∈ 𝑋) → (𝑂‘𝐴) = 𝑍) | ||
| Theorem | 0oo 29052 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝑌 = (BaseSet‘𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍:𝑋⟶𝑌) | ||
| Theorem | 0lno 29053 | 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 29054 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
| ⊢ 𝑁 = (𝑈 normOpOLD 𝑊) & ⊢ 𝑍 = (𝑈 0op 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → (𝑁‘𝑍) = 0) | ||
| Theorem | 0blo 29055 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
| ⊢ 𝑍 = (𝑈 0op 𝑊) & ⊢ 𝐵 = (𝑈 BLnOp 𝑊) ⇒ ⊢ ((𝑈 ∈ NrmCVec ∧ 𝑊 ∈ NrmCVec) → 𝑍 ∈ 𝐵) | ||
| Theorem | nmlno0lem 29056 | Lemma for nmlno0i 29057. (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 29057 | 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 29058 | 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 29059* | 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 29060 | 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 29061* | 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 29062 | 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 29063 | 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 29064* | 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 29065* | 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 29066 | 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 29067 | Lemma for blocni 29068 and lnocni 29069. 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 29068 | 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 29069 | 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 29070 | 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 29071 | 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 29072* | 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 29073* | 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 29074 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
| ⊢ 𝐻 = (HmOp‘𝑈) & ⊢ 𝐴 = (𝑈adj𝑈) ⇒ ⊢ (𝑈 ∈ NrmCVec → (𝑇 ∈ 𝐻 ↔ (𝑇 ∈ dom 𝐴 ∧ (𝐴‘𝑇) = 𝑇))) | ||
| Syntax | ccphlo 29075 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
| class CPreHilOLD | ||
| Definition | df-ph 29076* | 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 29077 | 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 29078 | 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 29079 | 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 29080* | 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 29081 | 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 29082 | 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 29083 | 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 29084 | 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 29085* | 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 29086 | 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 29087 | 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 29088 | 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 29089 | Lemma for ip1i 29090. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 & ⊢ 𝑁 = (normCV‘𝑈) & ⊢ 𝐽 ∈ ℂ ⇒ ⊢ (((𝐴𝐺𝐵)𝑃𝐶) + ((𝐴𝐺(-1𝑆𝐵))𝑃𝐶)) = (2 · (𝐴𝑃𝐶)) | ||
| Theorem | ip1i 29090 | 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 29091 | 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 29092 | Lemma for ipdiri 29093. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
| ⊢ 𝑋 = (BaseSet‘𝑈) & ⊢ 𝐺 = ( +𝑣 ‘𝑈) & ⊢ 𝑆 = ( ·𝑠OLD ‘𝑈) & ⊢ 𝑃 = (·𝑖OLD‘𝑈) & ⊢ 𝑈 ∈ CPreHilOLD & ⊢ 𝐴 ∈ 𝑋 & ⊢ 𝐵 ∈ 𝑋 & ⊢ 𝐶 ∈ 𝑋 ⇒ ⊢ ((𝐴𝐺𝐵)𝑃𝐶) = ((𝐴𝑃𝐶) + (𝐵𝑃𝐶)) | ||
| Theorem | ipdiri 29093 | 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 29094 | Lemma for ipassi 29104. 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 29095 | Lemma for ipassi 29104. 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 29096 | Lemma for ipassi 29104. 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 29097 | Lemma for ipassi 29104. 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 29098 | Lemma for ipassi 29104. 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 29099* | Lemma for ipassi 29104. 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 29100* | Lemma for ipassi 29104. By ipasslem5 29098, 𝐹 is 0 for all ℚ; since it is continuous and ℚ is dense in ℝ by qdensere2 23866, 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} | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |