![]() |
Metamath
Proof Explorer Theorem List (p. 306 of 481) | < 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: | ![]() (1-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | nmobndseqi 30501* | 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 30502* | Alternate shorter proof of nmobndseqi 30501 based on Axioms ax-reg 9583 and ax-ac2 10454 instead of ax-cc 10426. (Contributed by NM, 18-Jan-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ πΏ = (normCVβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) & β’ π β NrmCVec & β’ π β NrmCVec β β’ ((π:πβΆπ β§ βπ((π:ββΆπ β§ βπ β β (πΏβ(πβπ)) β€ 1) β βπ β β (πβ(πβ(πβπ))) β€ π)) β (πβπ) β β) | ||
Theorem | bloval 30503* | 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 30504 | The predicate "is a bounded linear operator." (Contributed by NM, 6-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (π β π΅ β (π β πΏ β§ (πβπ) < +β))) | ||
Theorem | isblo2 30505 | The predicate "is a bounded linear operator." (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (π β π΅ β (π β πΏ β§ (πβπ) β β))) | ||
Theorem | bloln 30506 | A bounded operator is a linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ πΏ = (π LnOp π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π β πΏ) | ||
Theorem | blof 30507 | A bounded operator is an operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π β π΅) β π:πβΆπ) | ||
Theorem | nmblore 30508 | 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 30509 | 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 30510 | Value of the zero operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec β§ π΄ β π) β (πβπ΄) = π) | ||
Theorem | 0oo 30511 | The zero operator is an operator. (Contributed by NM, 28-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π:πβΆπ) | ||
Theorem | 0lno 30512 | 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 30513 | The operator norm of the zero operator. (Contributed by NM, 27-Nov-2007.) (New usage is discouraged.) |
β’ π = (π normOpOLD π) & β’ π = (π 0op π) β β’ ((π β NrmCVec β§ π β NrmCVec) β (πβπ) = 0) | ||
Theorem | 0blo 30514 | The zero operator is a bounded linear operator. (Contributed by NM, 8-Dec-2007.) (New usage is discouraged.) |
β’ π = (π 0op π) & β’ π΅ = (π BLnOp π) β β’ ((π β NrmCVec β§ π β NrmCVec) β π β π΅) | ||
Theorem | nmlno0lem 30515 | Lemma for nmlno0i 30516. (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 30516 | 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 30517 | 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 30518* | 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 30519 | 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 30520* | 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 30521 | 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 30522 | 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 30523* | 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 30524* | 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 30525 | 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 30526 | Lemma for blocni 30527 and lnocni 30528. 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 30527 | 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 30528 | 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 30529 | 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 30530 | 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 30531* | 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 30532* | 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 30533 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π» = (HmOpβπ) & β’ π΄ = (πadjπ) β β’ (π β NrmCVec β (π β π» β (π β dom π΄ β§ (π΄βπ) = π))) | ||
Syntax | ccphlo 30534 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
class CPreHilOLD | ||
Definition | df-ph 30535* | 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 30536 | 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 30537 | 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 30538 | 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 30539* | 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 30540 | 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 30541 | 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 30542 | 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 30543 | 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 30544* | 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 30545 | 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 30546 | 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 30547 | 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 30548 | Lemma for ip1i 30549. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π = (normCVβπ) & β’ π½ β β β β’ (((π΄πΊπ΅)ππΆ) + ((π΄πΊ(-1ππ΅))ππΆ)) = (2 Β· (π΄ππΆ)) | ||
Theorem | ip1i 30549 | 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 30550 | 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 30551 | Lemma for ipdiri 30552. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π β β’ ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)) | ||
Theorem | ipdiri 30552 | 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 30553 | Lemma for ipassi 30563. 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 30554 | Lemma for ipassi 30563. 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 30555 | Lemma for ipassi 30563. 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 30556 | Lemma for ipassi 30563. 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 30557 | Lemma for ipassi 30563. 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 30558* | Lemma for ipassi 30563. 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 30559* | Lemma for ipassi 30563. By ipasslem5 30557, πΉ is 0 for all β; since it is continuous and β is dense in β by qdensere2 24635, 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 30560 | Lemma for ipassi 30563. Conclude from ipasslem8 30559 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (πΆ β β β ((πΆππ΄)ππ΅) = (πΆ Β· (π΄ππ΅))) | ||
Theorem | ipasslem10 30561 | Lemma for ipassi 30563. 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 30562 | Lemma for ipassi 30563. 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 30563 | 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 30564 | 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 30565 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅) + (π΄ππΆ))) | ||
Theorem | ip2dii 30566 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π· β π β β’ ((π΄πΊπ΅)π(πΆπΊπ·)) = (((π΄ππΆ) + (π΅ππ·)) + ((π΄ππ·) + (π΅ππΆ))) | ||
Theorem | dipass 30567 | 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 30568 | "Associative" law for second argument of inner product (compare dipass 30567). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((ββπ΅) Β· (π΄ππΆ))) | ||
Theorem | dipassr2 30569 | "Associative" law for inner product. Conjugate version of dipassr 30568. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π((ββπ΅)ππΆ)) = (π΅ Β· (π΄ππΆ))) | ||
Theorem | dipsubdir 30570 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = ((π΄ππΆ) β (π΅ππΆ))) | ||
Theorem | dipsubdi 30571 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((π΄ππ΅) β (π΄ππΆ))) | ||
Theorem | pythi 30572 | The Pythagorean theorem for an arbitrary complex inner product (pre-Hilbert) space π. The square of the norm of the sum of two orthogonal vectors (i.e. whose inner product is 0) is the sum of the squares of their norms. Problem 2 in [Kreyszig] p. 135. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ ((π΄ππ΅) = 0 β ((πβ(π΄πΊπ΅))β2) = (((πβπ΄)β2) + ((πβπ΅)β2))) | ||
Theorem | siilem1 30573 | Lemma for sii 30576. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) & β’ πΆ β β & β’ (πΆ Β· (π΄ππ΅)) β β & β’ 0 β€ (πΆ Β· (π΄ππ΅)) β β’ ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | siilem2 30574 | Lemma for sii 30576. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((πΆ β β β§ (πΆ Β· (π΄ππ΅)) β β β§ 0 β€ (πΆ Β· (π΄ππ΅))) β ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅)))) | ||
Theorem | siii 30575 | Inference from sii 30576. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅)) | ||
Theorem | sii 30576 | Obsolete version of ipcau 25088 as of 22-Sep-2024. Schwarz inequality. Part of Lemma 3-2.1(a) of [Kreyszig] p. 137. This is also called the Cauchy-Schwarz inequality by some authors and Bunjakovaskij-Cauchy-Schwarz inequality by others. See also Theorems bcseqi 30842, bcsiALT 30901, bcsiHIL 30902, csbren 25249. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β π β§ π΅ β π) β (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | ipblnfi 30577* | 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 30578* | 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 30579* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π:πβΆπ β§ π:πβΆπ) β (βπ₯ β π βπ¦ β π (π₯π(πβπ¦)) = (π₯π(πβπ¦)) β π = π)) | ||
Theorem | ajmoi 30580* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ β*π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))) | ||
Theorem | ajfuni 30581 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) & β’ π β CPreHilOLD & β’ π β NrmCVec β β’ Fun π΄ | ||
Theorem | ajfun 30582 | The adjoint function is a function. This is not immediately apparent from df-aj 30472 but results from the uniqueness shown by ajmoi 30580. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec) β Fun π΄) | ||
Theorem | ajval 30583* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π = (Β·πOLDβπ) & β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec β§ π:πβΆπ) β (π΄βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) | ||
Syntax | ccbn 30584 | Extend class notation with the class of all complex Banach spaces. |
class CBan | ||
Definition | df-cbn 30585 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 25186 instead. (New usage is discouraged.) |
β’ CBan = {π’ β NrmCVec β£ (IndMetβπ’) β (CMetβ(BaseSetβπ’))} | ||
Theorem | iscbn 30586 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 25188 instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β (π β NrmCVec β§ π· β (CMetβπ))) | ||
Theorem | cbncms 30587 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 25197 (or preferably bncms 25194) instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β π· β (CMetβπ)) | ||
Theorem | bnnv 30588 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 25190 instead. (New usage is discouraged.) |
β’ (π β CBan β π β NrmCVec) | ||
Theorem | bnrel 30589 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CBan | ||
Theorem | bnsscmcl 30590 | A subspace of a Banach space is a Banach space iff it is closed in the norm-induced metric of the parent space. (Contributed by NM, 1-Feb-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π» = (SubSpβπ) & β’ π = (BaseSetβπ) β β’ ((π β CBan β§ π β π») β (π β CBan β π β (Clsdβπ½))) | ||
Theorem | cnbn 30591 | The set of complex numbers is a complex Banach space. (Contributed by Steve Rodriguez, 4-Jan-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ + , Β· β©, absβ© β β’ π β CBan | ||
Theorem | ubthlem1 30592* | Lemma for ubth 30595. The function π΄ exhibits a countable collection of sets that are closed, being the inverse image under π‘ of the closed ball of radius π, and by assumption they cover π. Thus, by the Baire Category theorem bcth2 25180, for some π the set π΄βπ has an interior, meaning that there is a closed ball {π§ β π β£ (π¦π·π§) β€ π} in the set. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) & β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) & β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) β β’ (π β βπ β β βπ¦ β π βπ β β+ {π§ β π β£ (π¦π·π§) β€ π} β (π΄βπ)) | ||
Theorem | ubthlem2 30593* | Lemma for ubth 30595. Given that there is a closed ball π΅(π, π ) in π΄βπΎ, for any π₯ β π΅(0, 1), we have π + π Β· π₯ β π΅(π, π ) and π β π΅(π, π ), so both of these have norm(π‘(π§)) β€ πΎ and so norm(π‘(π₯ )) β€ (norm(π‘(π)) + norm(π‘(π + π Β· π₯))) / π β€ ( πΎ + πΎ) / π , which is our desired uniform bound. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) & β’ (π β βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π) & β’ π΄ = (π β β β¦ {π§ β π β£ βπ‘ β π (πβ(π‘βπ§)) β€ π}) & β’ (π β πΎ β β) & β’ (π β π β π) & β’ (π β π β β+) & β’ (π β {π§ β π β£ (ππ·π§) β€ π } β (π΄βπΎ)) β β’ (π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π) | ||
Theorem | ubthlem3 30594* | Lemma for ubth 30595. Prove the reverse implication, using nmblolbi 30522. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) β β’ (π β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π)) | ||
Theorem | ubth 30595* | Uniform Boundedness Theorem, also called the Banach-Steinhaus Theorem. Let π be a collection of bounded linear operators on a Banach space. If, for every vector π₯, the norms of the operators' values are bounded, then the operators' norms are also bounded. Theorem 4.7-3 of [Kreyszig] p. 249. See also http://en.wikipedia.org/wiki/Uniform_boundedness_principle. (Contributed by NM, 7-Nov-2007.) (Proof shortened by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (π normOpOLD π) β β’ ((π β CBan β§ π β NrmCVec β§ π β (π BLnOp π)) β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π (πβπ‘) β€ π)) | ||
Theorem | minvecolem1 30596* | Lemma for minveco 30606. The set of all distances from points of π to π΄ are a nonempty set of nonnegative reals. (Contributed by Mario Carneiro, 8-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) β β’ (π β (π β β β§ π β β β§ βπ€ β π 0 β€ π€)) | ||
Theorem | minvecolem2 30597* | Lemma for minveco 30606. Any two points πΎ and πΏ in π are close to each other if they are close to the infimum of distance to π΄. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β π΅ β β) & β’ (π β 0 β€ π΅) & β’ (π β πΎ β π) & β’ (π β πΏ β π) & β’ (π β ((π΄π·πΎ)β2) β€ ((πβ2) + π΅)) & β’ (π β ((π΄π·πΏ)β2) β€ ((πβ2) + π΅)) β β’ (π β ((πΎπ·πΏ)β2) β€ (4 Β· π΅)) | ||
Theorem | minvecolem3 30598* | Lemma for minveco 30606. The sequence formed by taking elements successively closer to the infimum is Cauchy. (Contributed by Mario Carneiro, 8-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β πΉ β (Cauβπ·)) | ||
Theorem | minvecolem4a 30599* | Lemma for minveco 30606. πΉ is convergent in the subspace topology on π. (Contributed by Mario Carneiro, 7-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β πΉ(βπ‘β(MetOpenβ(π· βΎ (π Γ π))))((βπ‘β(MetOpenβ(π· βΎ (π Γ π))))βπΉ)) | ||
Theorem | minvecolem4b 30600* | Lemma for minveco 30606. The convergent point of the cauchy sequence πΉ is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β ((βπ‘βπ½)βπΉ) β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |