![]() |
Metamath
Proof Explorer Theorem List (p. 302 of 480) | < 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-30209) |
![]() (30210-31732) |
![]() (31733-47936) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hmoval 30101* | 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 30102 | The predicate "is a hermitian operator." (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π» = (HmOpβπ) & β’ π΄ = (πadjπ) β β’ (π β NrmCVec β (π β π» β (π β dom π΄ β§ (π΄βπ) = π))) | ||
Syntax | ccphlo 30103 | Extend class notation with the class of all complex inner product spaces (also called pre-Hilbert spaces). |
class CPreHilOLD | ||
Definition | df-ph 30104* | 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 30105 | 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 30106 | 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 30107 | 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 30108* | 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 30109 | 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 30110 | 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 30111 | 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 30112 | 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 30113* | 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 30114 | 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 30115 | 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 30116 | 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 30117 | Lemma for ip1i 30118. (Contributed by NM, 21-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π = (normCVβπ) & β’ π½ β β β β’ (((π΄πΊπ΅)ππΆ) + ((π΄πΊ(-1ππ΅))ππΆ)) = (2 Β· (π΄ππΆ)) | ||
Theorem | ip1i 30118 | 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 30119 | 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 30120 | Lemma for ipdiri 30121. (Contributed by NM, 26-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π β β’ ((π΄πΊπ΅)ππΆ) = ((π΄ππΆ) + (π΅ππΆ)) | ||
Theorem | ipdiri 30121 | 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 30122 | Lemma for ipassi 30132. 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 30123 | Lemma for ipassi 30132. 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 30124 | Lemma for ipassi 30132. 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 30125 | Lemma for ipassi 30132. 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 30126 | Lemma for ipassi 30132. 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 30127* | Lemma for ipassi 30132. 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 30128* | Lemma for ipassi 30132. By ipasslem5 30126, πΉ is 0 for all β; since it is continuous and β is dense in β by qdensere2 24320, 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 30129 | Lemma for ipassi 30132. Conclude from ipasslem8 30128 the inner product associative law for real numbers. (Contributed by NM, 24-Aug-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (πΆ β β β ((πΆππ΄)ππ΅) = (πΆ Β· (π΄ππ΅))) | ||
Theorem | ipasslem10 30130 | Lemma for ipassi 30132. 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 30131 | Lemma for ipassi 30132. 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 30132 | 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 30133 | 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 30134 | Distributive law for inner product. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅) + (π΄ππΆ))) | ||
Theorem | ip2dii 30135 | Inner product of two sums. (Contributed by NM, 17-Apr-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ πΆ β π & β’ π· β π β β’ ((π΄πΊπ΅)π(πΆπΊπ·)) = (((π΄ππΆ) + (π΅ππ·)) + ((π΄ππ·) + (π΅ππΆ))) | ||
Theorem | dipass 30136 | 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 30137 | "Associative" law for second argument of inner product (compare dipass 30136). (Contributed by NM, 22-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((ββπ΅) Β· (π΄ππΆ))) | ||
Theorem | dipassr2 30138 | "Associative" law for inner product. Conjugate version of dipassr 30137. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β β β§ πΆ β π)) β (π΄π((ββπ΅)ππΆ)) = (π΅ Β· (π΄ππΆ))) | ||
Theorem | dipsubdir 30139 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄ππ΅)ππΆ) = ((π΄ππΆ) β (π΅ππΆ))) | ||
Theorem | dipsubdi 30140 | Distributive law for inner product subtraction. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (Β·πOLDβπ) β β’ ((π β CPreHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅ππΆ)) = ((π΄ππ΅) β (π΄ππΆ))) | ||
Theorem | pythi 30141 | 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 30142 | Lemma for sii 30145. (Contributed by NM, 23-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) & β’ πΆ β β & β’ (πΆ Β· (π΄ππ΅)) β β & β’ 0 β€ (πΆ Β· (π΄ππ΅)) β β’ ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | siilem2 30143 | Lemma for sii 30145. (Contributed by NM, 24-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π & β’ π = ( βπ£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((πΆ β β β§ (πΆ Β· (π΄ππ΅)) β β β§ 0 β€ (πΆ Β· (π΄ππ΅))) β ((π΅ππ΄) = (πΆ Β· ((πβπ΅)β2)) β (ββ((π΄ππ΅) Β· (πΆ Β· ((πβπ΅)β2)))) β€ ((πβπ΄) Β· (πβπ΅)))) | ||
Theorem | siii 30144 | Inference from sii 30145. (Contributed by NM, 20-Nov-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD & β’ π΄ β π & β’ π΅ β π β β’ (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅)) | ||
Theorem | sii 30145 | Obsolete version of ipcau 24762 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 30411, bcsiALT 30470, bcsiHIL 30471, csbren 24923. (Contributed by NM, 12-Jan-2008.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π΄ β π β§ π΅ β π) β (absβ(π΄ππ΅)) β€ ((πβπ΄) Β· (πβπ΅))) | ||
Theorem | ipblnfi 30146* | 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 30147* | 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 30148* | A condition implying that two operators are equal. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ ((π:πβΆπ β§ π:πβΆπ) β (βπ₯ β π βπ¦ β π (π₯π(πβπ¦)) = (π₯π(πβπ¦)) β π = π)) | ||
Theorem | ajmoi 30149* | Every operator has at most one adjoint. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π β CPreHilOLD β β’ β*π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))) | ||
Theorem | ajfuni 30150 | The adjoint function is a function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) & β’ π β CPreHilOLD & β’ π β NrmCVec β β’ Fun π΄ | ||
Theorem | ajfun 30151 | The adjoint function is a function. This is not immediately apparent from df-aj 30041 but results from the uniqueness shown by ajmoi 30149. (Contributed by NM, 26-Jan-2008.) (New usage is discouraged.) |
β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec) β Fun π΄) | ||
Theorem | ajval 30152* | Value of the adjoint function. (Contributed by NM, 25-Jan-2008.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (BaseSetβπ) & β’ π = (Β·πOLDβπ) & β’ π = (Β·πOLDβπ) & β’ π΄ = (πadjπ) β β’ ((π β CPreHilOLD β§ π β NrmCVec β§ π:πβΆπ) β (π΄βπ) = (β©π (π :πβΆπ β§ βπ₯ β π βπ¦ β π ((πβπ₯)ππ¦) = (π₯π(π βπ¦))))) | ||
Syntax | ccbn 30153 | Extend class notation with the class of all complex Banach spaces. |
class CBan | ||
Definition | df-cbn 30154 | Define the class of all complex Banach spaces. (Contributed by NM, 5-Dec-2006.) Use df-bn 24860 instead. (New usage is discouraged.) |
β’ CBan = {π’ β NrmCVec β£ (IndMetβπ’) β (CMetβ(BaseSetβπ’))} | ||
Theorem | iscbn 30155 | A complex Banach space is a normed complex vector space with a complete induced metric. (Contributed by NM, 5-Dec-2006.) Use isbn 24862 instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β (π β NrmCVec β§ π· β (CMetβπ))) | ||
Theorem | cbncms 30156 | The induced metric on complex Banach space is complete. (Contributed by NM, 8-Sep-2007.) Use bncmet 24871 (or preferably bncms 24868) instead. (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CBan β π· β (CMetβπ)) | ||
Theorem | bnnv 30157 | Every complex Banach space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) Use bnnvc 24864 instead. (New usage is discouraged.) |
β’ (π β CBan β π β NrmCVec) | ||
Theorem | bnrel 30158 | The class of all complex Banach spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CBan | ||
Theorem | bnsscmcl 30159 | 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 30160 | 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 30161* | Lemma for ubth 30164. 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 24854, 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 30162* | Lemma for ubth 30164. 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 30163* | Lemma for ubth 30164. Prove the reverse implication, using nmblolbi 30091. (Contributed by Mario Carneiro, 11-Jan-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (normCVβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CBan & β’ π β NrmCVec & β’ (π β π β (π BLnOp π)) β β’ (π β (βπ₯ β π βπ β β βπ‘ β π (πβ(π‘βπ₯)) β€ π β βπ β β βπ‘ β π ((π normOpOLD π)βπ‘) β€ π)) | ||
Theorem | ubth 30164* | 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 30165* | Lemma for minveco 30175. 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 30166* | Lemma for minveco 30175. 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 30167* | Lemma for minveco 30175. 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 30168* | Lemma for minveco 30175. πΉ 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 30169* | Lemma for minveco 30175. The convergent point of the cauchy sequence πΉ is a member of the base space. (Contributed by Mario Carneiro, 16-Jun-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β ((βπ‘βπ½)βπΉ) β π) | ||
Theorem | minvecolem4c 30170* | Lemma for minveco 30175. The infimum of the distances to π΄ is a real number. (Contributed by Mario Carneiro, 16-Jun-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) β β’ (π β π β β) | ||
Theorem | minvecolem4 30171* | Lemma for minveco 30175. The convergent point of the cauchy sequence πΉ attains the minimum distance, and so is closer to π΄ than any other point in π. (Contributed by Mario Carneiro, 7-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) & β’ (π β πΉ:ββΆπ) & β’ ((π β§ π β β) β ((π΄π·(πΉβπ))β2) β€ ((πβ2) + (1 / π))) & β’ π = (1 / (((((π΄π·((βπ‘βπ½)βπΉ)) + π) / 2)β2) β (πβ2))) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minvecolem5 30172* | Lemma for minveco 30175. Discharge the assumption about the sequence πΉ by applying countable choice ax-cc 10432. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ (π β βπ₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minvecolem6 30173* | Lemma for minveco 30175. Any minimal point is less than π away from π΄. (Contributed by Mario Carneiro, 9-May-2014.) (Revised by AV, 4-Oct-2020.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ ((π β§ π₯ β π) β (((π΄π·π₯)β2) β€ ((πβ2) + 0) β βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦)))) | ||
Theorem | minvecolem7 30174* | Lemma for minveco 30175. Since any two minimal points are distance zero away from each other, the minimal point is unique. (Contributed by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π = ran (π¦ β π β¦ (πβ(π΄ππ¦))) & β’ π = inf(π , β, < ) β β’ (π β β!π₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Theorem | minveco 30175* | Minimizing vector theorem, or the Hilbert projection theorem. There is exactly one vector in a complete subspace π that minimizes the distance to an arbitrary vector π΄ in a parent inner product space. Theorem 3.3-1 of [Kreyszig] p. 144, specialized to subspaces instead of convex subsets. (Contributed by NM, 11-Apr-2008.) (Proof shortened by Mario Carneiro, 9-May-2014.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) & β’ π = (BaseSetβπ) & β’ (π β π β CPreHilOLD) & β’ (π β π β ((SubSpβπ) β© CBan)) & β’ (π β π΄ β π) β β’ (π β β!π₯ β π βπ¦ β π (πβ(π΄ππ₯)) β€ (πβ(π΄ππ¦))) | ||
Syntax | chlo 30176 | Extend class notation with the class of all complex Hilbert spaces. |
class CHilOLD | ||
Definition | df-hlo 30177 | Define the class of all complex Hilbert spaces. A Hilbert space is a Banach space which is also an inner product space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ CHilOLD = (CBan β© CPreHilOLD) | ||
Theorem | ishlo 30178 | The predicate "is a complex Hilbert space." A Hilbert space is a Banach space which is also an inner product space, i.e. whose norm satisfies the parallelogram law. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β (π β CBan β§ π β CPreHilOLD)) | ||
Theorem | hlobn 30179 | Every complex Hilbert space is a complex Banach space. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β CBan) | ||
Theorem | hlph 30180 | Every complex Hilbert space is an inner product space (also called a pre-Hilbert space). (Contributed by NM, 28-Apr-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β CPreHilOLD) | ||
Theorem | hlrel 30181 | The class of all complex Hilbert spaces is a relation. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ Rel CHilOLD | ||
Theorem | hlnv 30182 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 17-Mar-2007.) (New usage is discouraged.) |
β’ (π β CHilOLD β π β NrmCVec) | ||
Theorem | hlnvi 30183 | Every complex Hilbert space is a normed complex vector space. (Contributed by NM, 6-Jun-2008.) (New usage is discouraged.) |
β’ π β CHilOLD β β’ π β NrmCVec | ||
Theorem | hlvc 30184 | Every complex Hilbert space is a complex vector space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (1st βπ) β β’ (π β CHilOLD β π β CVecOLD) | ||
Theorem | hlcmet 30185 | The induced metric on a complex Hilbert space is complete. (Contributed by NM, 8-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CHilOLD β π· β (CMetβπ)) | ||
Theorem | hlmet 30186 | The induced metric on a complex Hilbert space. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π· = (IndMetβπ) β β’ (π β CHilOLD β π· β (Metβπ)) | ||
Theorem | hlpar2 30187 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( βπ£ βπ) & β’ π = (normCVβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄ππ΅))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | hlpar 30188 | The parallelogram law satisfied by Hilbert space vectors. (Contributed by Steve Rodriguez, 28-Apr-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) & β’ π = (normCVβπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (((πβ(π΄πΊπ΅))β2) + ((πβ(π΄πΊ(-1ππ΅)))β2)) = (2 Β· (((πβπ΄)β2) + ((πβπ΅)β2)))) | ||
Theorem | hlex 30189 | The base set of a Hilbert space is a set. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) β β’ π β V | ||
Theorem | hladdf 30190 | Mapping for Hilbert space vector addition. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ (π β CHilOLD β πΊ:(π Γ π)βΆπ) | ||
Theorem | hlcom 30191 | Hilbert space vector addition is commutative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ π΄ β π β§ π΅ β π) β (π΄πΊπ΅) = (π΅πΊπ΄)) | ||
Theorem | hlass 30192 | Hilbert space vector addition is associative. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) β β’ ((π β CHilOLD β§ (π΄ β π β§ π΅ β π β§ πΆ β π)) β ((π΄πΊπ΅)πΊπΆ) = (π΄πΊ(π΅πΊπΆ))) | ||
Theorem | hl0cl 30193 | The Hilbert space zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = (0vecβπ) β β’ (π β CHilOLD β π β π) | ||
Theorem | hladdid 30194 | Hilbert space addition with the zero vector. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (π΄πΊπ) = π΄) | ||
Theorem | hlmulf 30195 | Mapping for Hilbert space scalar multiplication. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ (π β CHilOLD β π:(β Γ π)βΆπ) | ||
Theorem | hlmulid 30196 | Hilbert space scalar multiplication by one. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ π΄ β π) β (1ππ΄) = π΄) | ||
Theorem | hlmulass 30197 | Hilbert space scalar multiplication associative law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ Β· π΅)ππΆ) = (π΄π(π΅ππΆ))) | ||
Theorem | hldi 30198 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β π β§ πΆ β π)) β (π΄π(π΅πΊπΆ)) = ((π΄ππ΅)πΊ(π΄ππΆ))) | ||
Theorem | hldir 30199 | Hilbert space scalar multiplication distributive law. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ πΊ = ( +π£ βπ) & β’ π = ( Β·π OLD βπ) β β’ ((π β CHilOLD β§ (π΄ β β β§ π΅ β β β§ πΆ β π)) β ((π΄ + π΅)ππΆ) = ((π΄ππΆ)πΊ(π΅ππΆ))) | ||
Theorem | hlmul0 30200 | Hilbert space scalar multiplication by zero. (Contributed by NM, 7-Sep-2007.) (New usage is discouraged.) |
β’ π = (BaseSetβπ) & β’ π = ( Β·π OLD βπ) & β’ π = (0vecβπ) β β’ ((π β CHilOLD β§ π΄ β π) β (0ππ΄) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |