![]() |
Metamath
Proof Explorer Theorem List (p. 313 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pjcji 31201 | The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
โข ๐ป โ Cโ & โข ๐ด โ โ & โข ๐บ โ Cโ โ โข (๐ป โ (โฅโ๐บ) โ ((projโโ(๐ป โจโ ๐บ))โ๐ด) = (((projโโ๐ป)โ๐ด) +โ ((projโโ๐บ)โ๐ด))) | ||
Theorem | pjadji 31202 | A projection is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ((๐ด โ โ โง ๐ต โ โ) โ (((projโโ๐ป)โ๐ด) ยทih ๐ต) = (๐ด ยทih ((projโโ๐ป)โ๐ต))) | ||
Theorem | pjaddi 31203 | Projection of vector sum is sum of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ((๐ด โ โ โง ๐ต โ โ) โ ((projโโ๐ป)โ(๐ด +โ ๐ต)) = (((projโโ๐ป)โ๐ด) +โ ((projโโ๐ป)โ๐ต))) | ||
Theorem | pjinormi 31204 | The inner product of a projection and its argument is the square of the norm of the projection. Remark in [Halmos] p. 44. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข (๐ด โ โ โ (((projโโ๐ป)โ๐ด) ยทih ๐ด) = ((normโโ((projโโ๐ป)โ๐ด))โ2)) | ||
Theorem | pjsubi 31205 | Projection of vector difference is difference of projections. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ((๐ด โ โ โง ๐ต โ โ) โ ((projโโ๐ป)โ(๐ด โโ ๐ต)) = (((projโโ๐ป)โ๐ด) โโ ((projโโ๐ป)โ๐ต))) | ||
Theorem | pjmuli 31206 | Projection of scalar product is scalar product of projection. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ((๐ด โ โ โง ๐ต โ โ) โ ((projโโ๐ป)โ(๐ด ยทโ ๐ต)) = (๐ด ยทโ ((projโโ๐ป)โ๐ต))) | ||
Theorem | pjige0i 31207 | The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข (๐ด โ โ โ 0 โค (((projโโ๐ป)โ๐ด) ยทih ๐ด)) | ||
Theorem | pjige0 31208 | The inner product of a projection and its argument is nonnegative. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ โ) โ 0 โค (((projโโ๐ป)โ๐ด) ยทih ๐ด)) | ||
Theorem | pjcjt2 31209 | The projection on a subspace join is the sum of the projections. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐บ โ Cโ โง ๐ด โ โ) โ (๐ป โ (โฅโ๐บ) โ ((projโโ(๐ป โจโ ๐บ))โ๐ด) = (((projโโ๐ป)โ๐ด) +โ ((projโโ๐บ)โ๐ด)))) | ||
Theorem | pj0i 31210 | The projection of the zero vector. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ((projโโ๐ป)โ0โ) = 0โ | ||
Theorem | pjch 31211 | Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ โ) โ (๐ด โ ๐ป โ ((projโโ๐ป)โ๐ด) = ๐ด)) | ||
Theorem | pjid 31212 | The projection of a vector in the projection subspace is itself. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ ๐ป) โ ((projโโ๐ป)โ๐ด) = ๐ด) | ||
Theorem | pjvec 31213* | The set of vectors belonging to the subspace of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
โข (๐ป โ Cโ โ ๐ป = {๐ฅ โ โ โฃ ((projโโ๐ป)โ๐ฅ) = ๐ฅ}) | ||
Theorem | pjocvec 31214* | The set of vectors belonging to the orthocomplemented subspace of a projection. Second part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข (๐ป โ Cโ โ (โฅโ๐ป) = {๐ฅ โ โ โฃ ((projโโ๐ป)โ๐ฅ) = 0โ}) | ||
Theorem | pjocini 31215 | Membership of projection in orthocomplement of intersection. (Contributed by NM, 21-Apr-2001.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ โ โข (๐ด โ (โฅโ(๐บ โฉ ๐ป)) โ ((projโโ๐บ)โ๐ด) โ (โฅโ(๐บ โฉ ๐ป))) | ||
Theorem | pjini 31216 | Membership of projection in an intersection. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ โ โข (๐ด โ (๐บ โฉ ๐ป) โ ((projโโ๐บ)โ๐ด) โ (๐บ โฉ ๐ป)) | ||
Theorem | pjjsi 31217* | A sufficient condition for subspace join to be equal to subspace sum. (Contributed by NM, 29-May-2004.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Sโ โ โข (โ๐ฅ โ (๐บ โจโ ๐ป)((projโโ(โฅโ๐บ))โ๐ฅ) โ ๐ป โ (๐บ โจโ ๐ป) = (๐บ +โ ๐ป)) | ||
Theorem | pjfni 31218 | Functionality of a projection. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข (projโโ๐ป) Fn โ | ||
Theorem | pjrni 31219 | The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 30-Oct-1999.) (Revised by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ran (projโโ๐ป) = ๐ป | ||
Theorem | pjfoi 31220 | A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข (projโโ๐ป): โโontoโ๐ป | ||
Theorem | pjfi 31221 | The mapping of a projection. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข (projโโ๐ป): โโถ โ | ||
Theorem | pjvi 31222 | The value of a projection in terms of components. (Contributed by NM, 28-Nov-2000.) (New usage is discouraged.) |
โข ๐ป โ Cโ โ โข ((๐ด โ ๐ป โง ๐ต โ (โฅโ๐ป)) โ ((projโโ๐ป)โ(๐ด +โ ๐ต)) = ๐ด) | ||
Theorem | pjhfo 31223 | A projection maps onto its subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข (๐ป โ Cโ โ (projโโ๐ป): โโontoโ๐ป) | ||
Theorem | pjrn 31224 | The range of a projection. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข (๐ป โ Cโ โ ran (projโโ๐ป) = ๐ป) | ||
Theorem | pjhf 31225 | The mapping of a projection. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข (๐ป โ Cโ โ (projโโ๐ป): โโถ โ) | ||
Theorem | pjfn 31226 | Functionality of a projection. (Contributed by NM, 30-May-2006.) (New usage is discouraged.) |
โข (๐ป โ Cโ โ (projโโ๐ป) Fn โ) | ||
Theorem | pjsumi 31227 | The projection on a subspace sum is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ โ โข (๐ด โ โ โ (๐บ โ (โฅโ๐ป) โ ((projโโ(๐บ +โ ๐ป))โ๐ด) = (((projโโ๐บ)โ๐ด) +โ ((projโโ๐ป)โ๐ด)))) | ||
Theorem | pj11i 31228 | One-to-one correspondence of projection and subspace. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ โ โข ((projโโ๐บ) = (projโโ๐ป) โ ๐บ = ๐ป) | ||
Theorem | pjdsi 31229 | Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 21-Jun-2006.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ โ โข ((๐ด โ (๐บ โจโ ๐ป) โง ๐บ โ (โฅโ๐ป)) โ ๐ด = (((projโโ๐บ)โ๐ด) +โ ((projโโ๐ป)โ๐ด))) | ||
Theorem | pjds3i 31230 | Vector decomposition into sum of projections on orthogonal subspaces. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
โข ๐น โ Cโ & โข ๐บ โ Cโ & โข ๐ป โ Cโ โ โข (((๐ด โ ((๐น โจโ ๐บ) โจโ ๐ป) โง ๐น โ (โฅโ๐บ)) โง (๐น โ (โฅโ๐ป) โง ๐บ โ (โฅโ๐ป))) โ ๐ด = ((((projโโ๐น)โ๐ด) +โ ((projโโ๐บ)โ๐ด)) +โ ((projโโ๐ป)โ๐ด))) | ||
Theorem | pj11 31231 | One-to-one correspondence of projection and subspace. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข ((๐บ โ Cโ โง ๐ป โ Cโ ) โ ((projโโ๐บ) = (projโโ๐ป) โ ๐บ = ๐ป)) | ||
Theorem | pjmfn 31232 | Functionality of the projection function. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข projโ Fn Cโ | ||
Theorem | pjmf1 31233 | The projector function maps one-to-one into the set of Hilbert space operators. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
โข projโ: Cโ โ1-1โ( โ โm โ) | ||
Theorem | pjoi0 31234 | The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
โข (((๐บ โ Cโ โง ๐ป โ Cโ โง ๐ด โ โ) โง ๐บ โ (โฅโ๐ป)) โ (((projโโ๐บ)โ๐ด) ยทih ((projโโ๐ป)โ๐ด)) = 0) | ||
Theorem | pjoi0i 31235 | The inner product of projections on orthogonal subspaces vanishes. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ & โข ๐ด โ โ โ โข (๐บ โ (โฅโ๐ป) โ (((projโโ๐บ)โ๐ด) ยทih ((projโโ๐ป)โ๐ด)) = 0) | ||
Theorem | pjopythi 31236 | Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 1-Nov-1999.) (New usage is discouraged.) |
โข ๐บ โ Cโ & โข ๐ป โ Cโ & โข ๐ด โ โ โ โข (๐บ โ (โฅโ๐ป) โ ((normโโ(((projโโ๐บ)โ๐ด) +โ ((projโโ๐ป)โ๐ด)))โ2) = (((normโโ((projโโ๐บ)โ๐ด))โ2) + ((normโโ((projโโ๐ป)โ๐ด))โ2))) | ||
Theorem | pjopyth 31237 | Pythagorean theorem for projections on orthogonal subspaces. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐บ โ Cโ โง ๐ด โ โ) โ (๐ป โ (โฅโ๐บ) โ ((normโโ(((projโโ๐ป)โ๐ด) +โ ((projโโ๐บ)โ๐ด)))โ2) = (((normโโ((projโโ๐ป)โ๐ด))โ2) + ((normโโ((projโโ๐บ)โ๐ด))โ2)))) | ||
Theorem | pjnormi 31238 | The norm of the projection is less than or equal to the norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
โข ๐ป โ Cโ & โข ๐ด โ โ โ โข (normโโ((projโโ๐ป)โ๐ด)) โค (normโโ๐ด) | ||
Theorem | pjpythi 31239 | Pythagorean theorem for projections. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
โข ๐ป โ Cโ & โข ๐ด โ โ โ โข ((normโโ๐ด)โ2) = (((normโโ((projโโ๐ป)โ๐ด))โ2) + ((normโโ((projโโ(โฅโ๐ป))โ๐ด))โ2)) | ||
Theorem | pjneli 31240 | If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
โข ๐ป โ Cโ & โข ๐ด โ โ โ โข (ยฌ ๐ด โ ๐ป โ (normโโ((projโโ๐ป)โ๐ด)) < (normโโ๐ด)) | ||
Theorem | pjnorm 31241 | The norm of the projection is less than or equal to the norm. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ โ) โ (normโโ((projโโ๐ป)โ๐ด)) โค (normโโ๐ด)) | ||
Theorem | pjpyth 31242 | Pythagorean theorem for projectors. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ โ) โ ((normโโ๐ด)โ2) = (((normโโ((projโโ๐ป)โ๐ด))โ2) + ((normโโ((projโโ(โฅโ๐ป))โ๐ด))โ2))) | ||
Theorem | pjnel 31243 | If a vector does not belong to subspace, the norm of its projection is less than its norm. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ โ) โ (ยฌ ๐ด โ ๐ป โ (normโโ((projโโ๐ป)โ๐ด)) < (normโโ๐ด))) | ||
Theorem | pjnorm2 31244 | A vector belongs to the subspace of a projection iff the norm of its projection equals its norm. This and pjch 31211 yield Theorem 26.3 of [Halmos] p. 44. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
โข ((๐ป โ Cโ โง ๐ด โ โ) โ (๐ด โ ๐ป โ (normโโ((projโโ๐ป)โ๐ด)) = (normโโ๐ด))) | ||
Theorem | mayete3i 31245 | Mayet's equation E3. Part of Theorem 4.1 of [Mayet3] p. 1223. (Contributed by NM, 22-Jun-2006.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ & โข ๐ถ โ Cโ & โข ๐ท โ Cโ & โข ๐น โ Cโ & โข ๐บ โ Cโ & โข ๐ด โ (โฅโ๐ถ) & โข ๐ด โ (โฅโ๐น) & โข ๐ถ โ (โฅโ๐น) & โข ๐ด โ (โฅโ๐ต) & โข ๐ถ โ (โฅโ๐ท) & โข ๐น โ (โฅโ๐บ) & โข ๐ = ((๐ด โจโ ๐ถ) โจโ ๐น) & โข ๐ = (((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โฉ (๐น โจโ ๐บ)) & โข ๐ = ((๐ต โจโ ๐ท) โจโ ๐บ) โ โข (๐ โฉ ๐) โ ๐ | ||
Theorem | mayetes3i 31246 | Mayet's equation E^*3, derived from E3. Solution, for n = 3, to open problem in Remark (b) after Theorem 7.1 of [Mayet3] p. 1240. (Contributed by NM, 10-May-2009.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ & โข ๐ถ โ Cโ & โข ๐ท โ Cโ & โข ๐น โ Cโ & โข ๐บ โ Cโ & โข ๐ โ Cโ & โข ๐ด โ (โฅโ๐ถ) & โข ๐ด โ (โฅโ๐น) & โข ๐ถ โ (โฅโ๐น) & โข ๐ด โ (โฅโ๐ต) & โข ๐ถ โ (โฅโ๐ท) & โข ๐น โ (โฅโ๐บ) & โข ๐ โ (โฅโ๐) & โข ๐ = ((๐ด โจโ ๐ถ) โจโ ๐น) & โข ๐ = (((๐ด โจโ ๐ต) โฉ (๐ถ โจโ ๐ท)) โฉ (๐น โจโ ๐บ)) & โข ๐ = ((๐ต โจโ ๐ท) โจโ ๐บ) โ โข ((๐ โจโ ๐ ) โฉ ๐) โ (๐ โจโ ๐ ) | ||
Note on operators. Unlike some authors, we use the term "operator" to mean any function from โ to โ. This is the definition of operator in [Hughes] p. 14, the definition of operator in [AkhiezerGlazman] p. 30, and the definition of operator in [Goldberg] p. 10. For Reed and Simon, an operator is linear (definition of operator in [ReedSimon] p. 2). For Halmos, an operator is bounded and linear (definition of operator in [Halmos] p. 35). For Kalmbach and Beran, an operator is continuous and linear (definition of operator in [Kalmbach] p. 353; definition of operator in [Beran] p. 99). Note that "bounded and linear" and "continuous and linear" are equivalent by lncnbd 31555. | ||
Definition | df-hosum 31247* | Define the sum of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.) |
โข +op = (๐ โ ( โ โm โ), ๐ โ ( โ โm โ) โฆ (๐ฅ โ โ โฆ ((๐โ๐ฅ) +โ (๐โ๐ฅ)))) | ||
Definition | df-homul 31248* | Define the scalar product with a Hilbert space operator. Definition of [Beran] p. 111. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
โข ยทop = (๐ โ โ, ๐ โ ( โ โm โ) โฆ (๐ฅ โ โ โฆ (๐ ยทโ (๐โ๐ฅ)))) | ||
Definition | df-hodif 31249* | Define the difference of two Hilbert space operators. Definition of [Beran] p. 111. (Contributed by NM, 9-Nov-2000.) (New usage is discouraged.) |
โข โop = (๐ โ ( โ โm โ), ๐ โ ( โ โm โ) โฆ (๐ฅ โ โ โฆ ((๐โ๐ฅ) โโ (๐โ๐ฅ)))) | ||
Definition | df-hfsum 31250* | Define the sum of two Hilbert space functionals. Definition of [Beran] p. 111. Note that unlike some authors, we define a functional as any function from โ to โ, not just linear (or bounded linear) ones. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
โข +fn = (๐ โ (โ โm โ), ๐ โ (โ โm โ) โฆ (๐ฅ โ โ โฆ ((๐โ๐ฅ) + (๐โ๐ฅ)))) | ||
Definition | df-hfmul 31251* | Define the scalar product with a Hilbert space functional. Definition of [Beran] p. 111. (Contributed by NM, 23-May-2006.) (New usage is discouraged.) |
โข ยทfn = (๐ โ โ, ๐ โ (โ โm โ) โฆ (๐ฅ โ โ โฆ (๐ ยท (๐โ๐ฅ)))) | ||
Theorem | hosmval 31252* | Value of the sum of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op ๐) = (๐ฅ โ โ โฆ ((๐โ๐ฅ) +โ (๐โ๐ฅ)))) | ||
Theorem | hommval 31253* | Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ) โ (๐ด ยทop ๐) = (๐ฅ โ โ โฆ (๐ด ยทโ (๐โ๐ฅ)))) | ||
Theorem | hodmval 31254* | Value of the difference of two Hilbert space operators. (Contributed by NM, 9-Nov-2000.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop ๐) = (๐ฅ โ โ โฆ ((๐โ๐ฅ) โโ (๐โ๐ฅ)))) | ||
Theorem | hfsmval 31255* | Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
โข ((๐: โโถโ โง ๐: โโถโ) โ (๐ +fn ๐) = (๐ฅ โ โ โฆ ((๐โ๐ฅ) + (๐โ๐ฅ)))) | ||
Theorem | hfmmval 31256* | Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 23-Aug-2014.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถโ) โ (๐ด ยทfn ๐) = (๐ฅ โ โ โฆ (๐ด ยท (๐โ๐ฅ)))) | ||
Theorem | hosval 31257 | Value of the sum of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐ด โ โ) โ ((๐ +op ๐)โ๐ด) = ((๐โ๐ด) +โ (๐โ๐ด))) | ||
Theorem | homval 31258 | Value of the scalar product with a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐ต โ โ) โ ((๐ด ยทop ๐)โ๐ต) = (๐ด ยทโ (๐โ๐ต))) | ||
Theorem | hodval 31259 | Value of the difference of two Hilbert space operators. (Contributed by NM, 10-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ โง ๐ด โ โ) โ ((๐ โop ๐)โ๐ด) = ((๐โ๐ด) โโ (๐โ๐ด))) | ||
Theorem | hfsval 31260 | Value of the sum of two Hilbert space functionals. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐: โโถโ โง ๐: โโถโ โง ๐ด โ โ) โ ((๐ +fn ๐)โ๐ด) = ((๐โ๐ด) + (๐โ๐ด))) | ||
Theorem | hfmval 31261 | Value of the scalar product with a Hilbert space functional. (Contributed by NM, 23-May-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถโ โง ๐ต โ โ) โ ((๐ด ยทfn ๐)โ๐ต) = (๐ด ยท (๐โ๐ต))) | ||
Theorem | hoscl 31262 | Closure of the sum of two Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข (((๐: โโถ โ โง ๐: โโถ โ) โง ๐ด โ โ) โ ((๐ +op ๐)โ๐ด) โ โ) | ||
Theorem | homcl 31263 | Closure of the scalar product of a Hilbert space operator. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ โง ๐ต โ โ) โ ((๐ด ยทop ๐)โ๐ต) โ โ) | ||
Theorem | hodcl 31264 | Closure of the difference of two Hilbert space operators. (Contributed by NM, 15-Nov-2002.) (New usage is discouraged.) |
โข (((๐: โโถ โ โง ๐: โโถ โ) โง ๐ด โ โ) โ ((๐ โop ๐)โ๐ด) โ โ) | ||
Definition | df-h0op 31265 | Define the Hilbert space zero operator. See df0op2 31269 for alternate definition. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
โข 0hop = (projโโ0โ) | ||
Definition | df-iop 31266 | Define the Hilbert space identity operator. See dfiop2 31270 for alternate definition. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข Iop = (projโโ โ) | ||
Theorem | ho0val 31267 | Value of the zero Hilbert space operator (null projector). Remark in [Beran] p. 111. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
โข (๐ด โ โ โ ( 0hop โ๐ด) = 0โ) | ||
Theorem | ho0f 31268 | Functionality of the zero Hilbert space operator. (Contributed by NM, 10-Mar-2006.) (New usage is discouraged.) |
โข 0hop : โโถ โ | ||
Theorem | df0op2 31269 | Alternate definition of Hilbert space zero operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
โข 0hop = ( โ ร 0โ) | ||
Theorem | dfiop2 31270 | Alternate definition of Hilbert space identity operator. (Contributed by NM, 7-Aug-2006.) (New usage is discouraged.) |
โข Iop = ( I โพ โ) | ||
Theorem | hoif 31271 | Functionality of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
โข Iop : โโ1-1-ontoโ โ | ||
Theorem | hoival 31272 | The value of the Hilbert space identity operator. (Contributed by NM, 8-Aug-2006.) (New usage is discouraged.) |
โข (๐ด โ โ โ ( Iop โ๐ด) = ๐ด) | ||
Theorem | hoico1 31273 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ (๐ โ Iop ) = ๐) | ||
Theorem | hoico2 31274 | Composition with the Hilbert space identity operator. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข (๐: โโถ โ โ ( Iop โ ๐) = ๐) | ||
Theorem | hoaddcl 31275 | The sum of Hilbert space operators is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op ๐): โโถ โ) | ||
Theorem | homulcl 31276 | The scalar product of a Hilbert space operator is an operator. (Contributed by NM, 21-Feb-2006.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ((๐ด โ โ โง ๐: โโถ โ) โ (๐ด ยทop ๐): โโถ โ) | ||
Theorem | hoeq 31277* | Equality of Hilbert space operators. (Contributed by NM, 12-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (โ๐ฅ โ โ (๐โ๐ฅ) = (๐โ๐ฅ) โ ๐ = ๐)) | ||
Theorem | hoeqi 31278* | Equality of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (โ๐ฅ โ โ (๐โ๐ฅ) = (๐โ๐ฅ) โ ๐ = ๐) | ||
Theorem | hoscli 31279 | Closure of Hilbert space operator sum. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ +op ๐)โ๐ด) โ โ) | ||
Theorem | hodcli 31280 | Closure of Hilbert space operator difference. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ โop ๐)โ๐ด) โ โ) | ||
Theorem | hocoi 31281 | Composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ โ ๐)โ๐ด) = (๐โ(๐โ๐ด))) | ||
Theorem | hococli 31282 | Closure of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ ((๐ โ ๐)โ๐ด) โ โ) | ||
Theorem | hocofi 31283 | Mapping of composition of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โ ๐): โโถ โ | ||
Theorem | hocofni 31284 | Functionality of composition of Hilbert space operators. (Contributed by NM, 12-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โ ๐) Fn โ | ||
Theorem | hoaddcli 31285 | Mapping of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐): โโถ โ | ||
Theorem | hosubcli 31286 | Mapping of difference of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (Revised by Mario Carneiro, 16-Nov-2013.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โop ๐): โโถ โ | ||
Theorem | hoaddfni 31287 | Functionality of sum of Hilbert space operators. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐) Fn โ | ||
Theorem | hosubfni 31288 | Functionality of difference of Hilbert space operators. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ โop ๐) Fn โ | ||
Theorem | hoaddcomi 31289 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 15-Nov-2000.) (New usage is discouraged.) |
โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op ๐) = (๐ +op ๐) | ||
Theorem | hosubcl 31290 | Mapping of difference of Hilbert space operators. (Contributed by NM, 23-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ โop ๐): โโถ โ) | ||
Theorem | hoaddcom 31291 | Commutativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐: โโถ โ โง ๐: โโถ โ) โ (๐ +op ๐) = (๐ +op ๐)) | ||
Theorem | hodsi 31292 | Relationship between Hilbert space operator difference and sum. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) = ๐ โ (๐ +op ๐) = ๐ ) | ||
Theorem | hoaddassi 31293 | Associativity of sum of Hilbert space operators. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐)) | ||
Theorem | hoadd12i 31294 | Commutative/associative law for Hilbert space operator sum that swaps the first two terms. (Contributed by NM, 27-Aug-2004.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ +op (๐ +op ๐)) = (๐ +op (๐ +op ๐)) | ||
Theorem | hoadd32i 31295 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 27-Jul-2006.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) +op ๐) = ((๐ +op ๐) +op ๐) | ||
Theorem | hocadddiri 31296 | Distributive law for Hilbert space operator sum. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ +op ๐) โ ๐) = ((๐ โ ๐) +op (๐ โ ๐)) | ||
Theorem | hocsubdiri 31297 | Distributive law for Hilbert space operator difference. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข ((๐ โop ๐) โ ๐) = ((๐ โ ๐) โop (๐ โ ๐)) | ||
Theorem | ho2coi 31298 | Double composition of Hilbert space operators. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
โข ๐ : โโถ โ & โข ๐: โโถ โ & โข ๐: โโถ โ โ โข (๐ด โ โ โ (((๐ โ ๐) โ ๐)โ๐ด) = (๐ โ(๐โ(๐โ๐ด)))) | ||
Theorem | hoaddass 31299 | Associativity of sum of Hilbert space operators. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) +op ๐) = (๐ +op (๐ +op ๐))) | ||
Theorem | hoadd32 31300 | Commutative/associative law for Hilbert space operator sum that swaps the second and third terms. (Contributed by NM, 24-Aug-2006.) (New usage is discouraged.) |
โข ((๐ : โโถ โ โง ๐: โโถ โ โง ๐: โโถ โ) โ ((๐ +op ๐) +op ๐) = ((๐ +op ๐) +op ๐)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |