Home | Metamath
Proof Explorer Theorem List (p. 295 of 470) | < 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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nvge0 29401 | The norm of a normed complex vector space is nonnegative. Second part of Problem 2 of [Kreyszig] p. 64. (Contributed by NM, 28-Nov-2006.) (Proof shortened by AV, 10-Jul-2022.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) β β’ ((π β NrmCVec β§ π΄ β π) β 0 β€ (πβπ΄)) | ||
Theorem | nvgt0 29402 | A nonzero norm is positive. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (normCVβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (π΄ β π β 0 < (πβπ΄))) | ||
Theorem | nv1 29403 | From any nonzero vector, construct a vector whose norm is one. (Contributed by NM, 6-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) & β’ π = (normCVβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΄ β π) β (πβ((1 / (πβπ΄))ππ΄)) = 1) | ||
Theorem | nvop 29404 | A complex inner product space in terms of ordered pair components. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) β β’ (π β NrmCVec β π = β¨β¨πΊ, πβ©, πβ©) | ||
Theorem | cnnv 29405 | The set of complex numbers is a normed complex vector space. The vector operation is +, the scalar product is Β·, and the norm function is abs. (Contributed by Steve Rodriguez, 3-Dec-2006.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ π β NrmCVec | ||
Theorem | cnnvg 29406 | The vector addition (group) operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ + = ( +π£ βπ) | ||
Theorem | cnnvba 29407 | The base set of the normed complex vector space of complex numbers. (Contributed by NM, 7-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ β = (BaseSetβπ) | ||
Theorem | cnnvs 29408 | The scalar product operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ Β· = ( Β·π OLD βπ) | ||
Theorem | cnnvnm 29409 | The norm operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ abs = (normCVβπ) | ||
Theorem | cnnvm 29410 | The vector subtraction operation of the normed complex vector space of complex numbers. (Contributed by NM, 12-Jan-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ β = ( βπ£ βπ) | ||
Theorem | elimnv 29411 | Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π β NrmCVec β β’ if(π΄ β π, π΄, π) β π | ||
Theorem | elimnvu 29412 | Hypothesis elimination lemma for normed complex vector spaces to assist weak deduction theorem. (Contributed by NM, 16-May-2007.) (New usage is discouraged.) |
β’ if(π β NrmCVec, π, β¨β¨ + , Β· β©, absβ©) β NrmCVec | ||
Theorem | imsval 29413 | Value of the induced metric of a normed complex vector space. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) β β’ (π β NrmCVec β π· = (π β π)) | ||
Theorem | imsdval 29414 | Value of the induced metric (distance function) of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 11-Sep-2007.) (Revised by Mario Carneiro, 27-Dec-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΄ππ΅))) | ||
Theorem | imsdval2 29415 | Value of the distance function of the induced metric of a normed complex vector space. Equation 1 of [Kreyszig] p. 59. (Contributed by NM, 28-Nov-2006.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄π·π΅) = (πβ(π΄πΊ(-1ππ΅)))) | ||
Theorem | nvnd 29416 | The norm of a normed complex vector space expressed in terms of the distance function of its induced metric. Problem 1 of [Kreyszig] p. 63. (Contributed by NM, 4-Dec-2006.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (πβπ΄) = (π΄π·π)) | ||
Theorem | imsdf 29417 | Mapping for the induced metric distance function of a normed complex vector space. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β NrmCVec β π·:(π Γ π)βΆβ) | ||
Theorem | imsmetlem 29418 | Lemma for imsmet 29419. (Contributed by NM, 29-Nov-2006.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (invβπΊ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π β NrmCVec β β’ π· β (Metβπ) | ||
Theorem | imsmet 29419 | The induced metric of a normed complex vector space is a metric space. Part of Definition 2.2-1 of [Kreyszig] p. 58. (Contributed by NM, 4-Dec-2006.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β NrmCVec β π· β (Metβπ)) | ||
Theorem | imsxmet 29420 | The induced metric of a normed complex vector space is an extended metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β NrmCVec β π· β (βMetβπ)) | ||
Theorem | cnims 29421 | The metric induced on the complex numbers. cnmet 24057 proves that it is a metric. (Contributed by Steve Rodriguez, 5-Dec-2006.) (Revised by NM, 15-Jan-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© & β’ π· = (abs β β ) β β’ π· = (IndMetβπ) | ||
Theorem | vacn 29422 | Vector addition is jointly continuous in both arguments. (Contributed by Jeff Hankins, 16-Jun-2009.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΊ = ( +π£ βπ) β β’ (π β NrmCVec β πΊ β ((π½ Γt π½) Cn π½)) | ||
Theorem | nmcvcn 29423 | The norm of a normed complex vector space is a continuous function. (Contributed by NM, 16-May-2007.) (Proof shortened by Mario Carneiro, 10-Jan-2014.) (New usage is discouraged.) |
β’ π = (normCVβπ) & β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (topGenβran (,)) β β’ (π β NrmCVec β π β (π½ Cn πΎ)) | ||
Theorem | nmcnc 29424 | The norm of a normed complex vector space is a continuous function to β. (For β, see nmcvcn 29423.) (Contributed by NM, 12-Aug-2007.) (New usage is discouraged.) |
β’ π = (normCVβπ) & β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (TopOpenββfld) β β’ (π β NrmCVec β π β (π½ Cn πΎ)) | ||
Theorem | smcnlem 29425* | Lemma for smcn 29426. (Contributed by Mario Carneiro, 5-May-2014.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ π = ( Β·π OLD βπ) & β’ πΎ = (TopOpenββfld) & β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π β NrmCVec & β’ π = (1 / (1 + ((((πβπ¦) + (absβπ₯)) + 1) / π))) β β’ π β ((πΎ Γt π½) Cn π½) | ||
Theorem | smcn 29426 | Scalar multiplication is jointly continuous in both arguments. (Contributed by NM, 16-Jun-2009.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ π = ( Β·π OLD βπ) & β’ πΎ = (TopOpenββfld) β β’ (π β NrmCVec β π β ((πΎ Γt π½) Cn π½)) | ||
Theorem | vmcn 29427 | Vector subtraction is jointly continuous in both arguments. (Contributed by Mario Carneiro, 6-May-2014.) (New usage is discouraged.) |
β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ π = ( βπ£ βπ) β β’ (π β NrmCVec β π β ((π½ Γt π½) Cn π½)) | ||
Syntax | cdip 29428 | Extend class notation with the class inner product functions. |
class Β·πOLD | ||
Definition | df-dip 29429* | Define a function that maps a normed complex vector space to its inner product operation in case its norm satisfies the parallelogram identity (otherwise the operation is still defined, but not meaningful). Based on Exercise 4(a) of [ReedSimon] p. 63 and Theorem 6.44 of [Ponnusamy] p. 361. Vector addition is (1st βπ€), the scalar product is (2nd βπ€), and the norm is π. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.) |
β’ Β·πOLD = (π’ β NrmCVec β¦ (π₯ β (BaseSetβπ’), π¦ β (BaseSetβπ’) β¦ (Ξ£π β (1...4)((iβπ) Β· (((normCVβπ’)β(π₯( +π£ βπ’)((iβπ)( Β·π OLD βπ’)π¦)))β2)) / 4))) | ||
Theorem | dipfval 29430* | The inner product function on a normed complex vector space. The definition is meaningful for vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law. (Contributed by NM, 10-Apr-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ (π β NrmCVec β π = (π₯ β π, π¦ β π β¦ (Ξ£π β (1...4)((iβπ) Β· ((πβ(π₯πΊ((iβπ)ππ¦)))β2)) / 4))) | ||
Theorem | ipval 29431* | Value of the inner product. The definition is meaningful for normed complex vector spaces that are also inner product spaces, i.e. satisfy the parallelogram law, although for convenience we define it for any normed complex vector space. The vector (group) addition operation is πΊ, the scalar product is π, the norm is π, and the set of vectors is π. Equation 6.45 of [Ponnusamy] p. 361. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (Ξ£π β (1...4)((iβπ) Β· ((πβ(π΄πΊ((iβπ)ππ΅)))β2)) / 4)) | ||
Theorem | ipval2lem2 29432 | Lemma for ipval3 29437. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ πΆ β β) β ((πβ(π΄πΊ(πΆππ΅)))β2) β β) | ||
Theorem | ipval2lem3 29433 | Lemma for ipval3 29437. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((πβ(π΄πΊπ΅))β2) β β) | ||
Theorem | ipval2lem4 29434 | Lemma for ipval3 29437. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ (((π β NrmCVec β§ π΄ β π β§ π΅ β π) β§ πΆ β β) β ((πβ(π΄πΊ(πΆππ΅)))β2) β β) | ||
Theorem | ipval2 29435 | Expansion of the inner product value ipval 29431. (Contributed by NM, 31-Jan-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2)))) / 4)) | ||
Theorem | 4ipval2 29436 | Four times the inner product value ipval3 29437, useful for simplifying certain proofs. (Contributed by NM, 10-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (4 Β· (π΄ππ΅)) = ((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄πΊ(-1ππ΅)))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄πΊ(-iππ΅)))β2))))) | ||
Theorem | ipval3 29437 | Expansion of the inner product value ipval 29431. (Contributed by NM, 17-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π = ( βπ£ βπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) = (((((πβ(π΄πΊπ΅))β2) β ((πβ(π΄ππ΅))β2)) + (i Β· (((πβ(π΄πΊ(iππ΅)))β2) β ((πβ(π΄π(iππ΅)))β2)))) / 4)) | ||
Theorem | ipidsq 29438 | The inner product of a vector with itself is the square of the vector's norm. Equation I4 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (π΄ππ΄) = ((πβπ΄)β2)) | ||
Theorem | ipnm 29439 | Norm expressed in terms of inner product. (Contributed by NM, 11-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (πβπ΄) = (ββ(π΄ππ΄))) | ||
Theorem | dipcl 29440 | An inner product is a complex number. (Contributed by NM, 1-Feb-2007.) (Revised by Mario Carneiro, 5-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (π΄ππ΅) β β) | ||
Theorem | ipf 29441 | Mapping for the inner product operation. (Contributed by NM, 28-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ (π β NrmCVec β π:(π Γ π)βΆβ) | ||
Theorem | dipcj 29442 | The complex conjugate of an inner product reverses its arguments. Equation I1 of [Ponnusamy] p. 362. (Contributed by NM, 1-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β (ββ(π΄ππ΅)) = (π΅ππ΄)) | ||
Theorem | ipipcj 29443 | An inner product times its conjugate. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄ππ΅) Β· (π΅ππ΄)) = ((absβ(π΄ππ΅))β2)) | ||
Theorem | diporthcom 29444 | Orthogonality (meaning inner product is 0) is commutative. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π β§ π΅ β π) β ((π΄ππ΅) = 0 β (π΅ππ΄) = 0)) | ||
Theorem | dip0r 29445 | Inner product with a zero second argument. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (π΄ππ) = 0) | ||
Theorem | dip0l 29446 | Inner product with a zero first argument. Part of proof of Theorem 6.44 of [Ponnusamy] p. 361. (Contributed by NM, 5-Feb-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π) β (πππ΄) = 0) | ||
Theorem | ipz 29447 | The inner product of a vector with itself is zero iff the vector is zero. Part of Definition 3.1-1 of [Kreyszig] p. 129. (Contributed by NM, 24-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (Β·πOLDβπ) β β’ ((π β NrmCVec β§ π΄ β π) β ((π΄ππ΄) = 0 β π΄ = π)) | ||
Theorem | dipcn 29448 | Inner product is jointly continuous in both arguments. (Contributed by NM, 21-Aug-2007.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π = (Β·πOLDβπ) & β’ πΆ = (IndMetβπ) & β’ π½ = (MetOpenβπΆ) & β’ πΎ = (TopOpenββfld) β β’ (π β NrmCVec β π β ((π½ Γt π½) Cn πΎ)) | ||
Syntax | css 29449 | Extend class notation with the class of all subspaces of normed complex vector spaces. |
class SubSp | ||
Definition | df-ssp 29450* | Define the class of all subspaces of normed complex vector spaces. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ SubSp = (π’ β NrmCVec β¦ {π€ β NrmCVec β£ (( +π£ βπ€) β ( +π£ βπ’) β§ ( Β·π OLD βπ€) β ( Β·π OLD βπ’) β§ (normCVβπ€) β (normCVβπ’))}) | ||
Theorem | sspval 29451* | The set of all subspaces of a normed complex vector space. (Contributed by NM, 26-Jan-2008.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π» = (SubSpβπ) β β’ (π β NrmCVec β π» = {π€ β NrmCVec β£ (( +π£ βπ€) β πΊ β§ ( Β·π OLD βπ€) β π β§ (normCVβπ€) β π)}) | ||
Theorem | isssp 29452 | The predicate "is a subspace." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ πΊ = ( +π£ βπ) & β’ πΉ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) & β’ π = (normCVβπ) & β’ π» = (SubSpβπ) β β’ (π β NrmCVec β (π β π» β (π β NrmCVec β§ (πΉ β πΊ β§ π β π β§ π β π)))) | ||
Theorem | sspid 29453 | A normed complex vector space is a subspace of itself. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
β’ π» = (SubSpβπ) β β’ (π β NrmCVec β π β π») | ||
Theorem | sspnv 29454 | A subspace is a normed complex vector space. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.) |
β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β π β NrmCVec) | ||
Theorem | sspba 29455 | The base set of a subspace is included in the parent base set. (Contributed by NM, 27-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β π β π) | ||
Theorem | sspg 29456 | Vector addition on a subspace is a restriction of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ πΉ = ( +π£ βπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β πΉ = (πΊ βΎ (π Γ π))) | ||
Theorem | sspgval 29457 | Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ πΉ = ( +π£ βπ) & β’ π» = (SubSpβπ) β β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄πΉπ΅) = (π΄πΊπ΅)) | ||
Theorem | ssps 29458 | Scalar multiplication on a subspace is a restriction of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = ( Β·π OLD βπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β π = (π βΎ (β Γ π))) | ||
Theorem | sspsval 29459 | Scalar multiplication on a subspace in terms of scalar multiplication on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = ( Β·π OLD βπ) & β’ π» = (SubSpβπ) β β’ (((π β NrmCVec β§ π β π») β§ (π΄ β β β§ π΅ β π)) β (π΄π π΅) = (π΄ππ΅)) | ||
Theorem | sspmlem 29460* | Lemma for sspm 29462 and others. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π» = (SubSpβπ) & β’ (((π β NrmCVec β§ π β π») β§ (π₯ β π β§ π¦ β π)) β (π₯πΉπ¦) = (π₯πΊπ¦)) & β’ (π β NrmCVec β πΉ:(π Γ π)βΆπ ) & β’ (π β NrmCVec β πΊ:((BaseSetβπ) Γ (BaseSetβπ))βΆπ) β β’ ((π β NrmCVec β§ π β π») β πΉ = (πΊ βΎ (π Γ π))) | ||
Theorem | sspmval 29461 | Vector addition on a subspace in terms of vector addition on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ πΏ = ( βπ£ βπ) & β’ π» = (SubSpβπ) β β’ (((π β NrmCVec β§ π β π») β§ (π΄ β π β§ π΅ β π)) β (π΄πΏπ΅) = (π΄ππ΅)) | ||
Theorem | sspm 29462 | Vector subtraction on a subspace is a restriction of vector subtraction on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ πΏ = ( βπ£ βπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β πΏ = (π βΎ (π Γ π))) | ||
Theorem | sspz 29463 | The zero vector of a subspace is the same as the parent's. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (0vecβπ) & β’ π = (0vecβπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β π = π) | ||
Theorem | sspn 29464 | The norm on a subspace is a restriction of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (normCVβπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π») β π = (π βΎ π)) | ||
Theorem | sspnval 29465 | The norm on a subspace in terms of the norm on the parent space. (Contributed by NM, 28-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (normCVβπ) & β’ π» = (SubSpβπ) β β’ ((π β NrmCVec β§ π β π» β§ π΄ β π) β (πβπ΄) = (πβπ΄)) | ||
Theorem | sspimsval 29466 | 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 29467 | 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 29468 | Extend class notation with the class of linear operators on normed complex vector spaces. |
class LnOp | ||
Syntax | cnmoo 29469 | Extend class notation with the class of operator norms on normed complex vector spaces. |
class normOpOLD | ||
Syntax | cblo 29470 | Extend class notation with the class of bounded linear operators on normed complex vector spaces. |
class BLnOp | ||
Syntax | c0o 29471 | Extend class notation with the class of zero operators on normed complex vector spaces. |
class 0op | ||
Definition | df-lno 29472* | 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 29473* | 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 29474* | 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 29475* | 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 29476 | Adjoint of an operator. |
class adj | ||
Syntax | chmo 29477 | Set of Hermitional (self-adjoint) operators. |
class HmOp | ||
Definition | df-aj 29478* | 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 29479* | 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 29480* | 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 29481* | 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 29482 | 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 29483 | 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 29484 | 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 29485 | 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 29486 | 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 29487 | 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 29488 | 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 29489 | Two ways to express a zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) β β’ ((π β NrmCVec β§ π:πβΆπ) β (π = (π Γ {π}) β ran π = {π})) | ||
Theorem | nmoofval 29490* | 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 29491* | 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 29492* | The set in the supremum of the operator norm definition df-nmoo 29473 is a set of reals. (Contributed by NM, 13-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) β β’ ((π β NrmCVec β§ π:πβΆπ) β {π₯ β£ βπ§ β π ((πβπ§) β€ 1 β§ π₯ = (πβ(πβπ§)))} β β) | ||
Theorem | nmosetn0 29493* | The set in the supremum of the operator norm definition df-nmoo 29473 is nonempty. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (normCVβπ) β β’ (π β NrmCVec β (πβ(πβπ)) β {π₯ β£ βπ¦ β π ((πβπ¦) β€ 1 β§ π₯ = (πβ(πβπ¦)))}) | ||
Theorem | nmoxr 29494 | 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 29495 | 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 29496 | 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 29497 | 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 29498 | 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 29499 | 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 29500* | 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 β (πβ(πβπ₯)) β€ π΄))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |