Home | Metamath
Proof Explorer Theorem List (p. 310 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pjordi 30901* | The definition of projector ordering in [Halmos] p. 42 is equivalent to the definition of projector ordering in [Beran] p. 110. (We will usually express projector ordering with the even simpler equivalent πΊ β π»; see pjssposi 30900). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (βπ₯ β β 0 β€ ((((projββπ») βop (projββπΊ))βπ₯) Β·ih π₯) β ((projββπΊ) β β) β ((projββπ») β β)) | ||
Theorem | pjssdif2i 30902 | The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 30900). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) = (projββ(π» β© (β₯βπΊ)))) | ||
Theorem | pjssdif1i 30903 | A necessary and sufficient condition for the difference between two projectors to be a projector. Part 1 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 30900). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) β ran projβ) | ||
Theorem | pjimai 30904 | The image of a projection. Lemma 5 in Daniel Lehmann, "A presentation of Quantum Logic based on an and then connective", https://doi.org/10.48550/arXiv.quant-ph/0701113. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Cβ β β’ ((projββπ΅) β π΄) = ((π΄ +β (β₯βπ΅)) β© π΅) | ||
Theorem | pjidmcoi 30905 | A projection is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») β (projββπ»)) = (projββπ») | ||
Theorem | pjoccoi 30906 | Composition of projections of a subspace and its orthocomplement. (Contributed by NM, 14-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») β (projββ(β₯βπ»))) = 0hop | ||
Theorem | pjtoi 30907 | Subspace sum of projection and projection of orthocomplement. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββπ») +op (projββ(β₯βπ»))) = (projββ β) | ||
Theorem | pjoci 30908 | Projection of orthocomplement. First part of Theorem 27.3 of [Halmos] p. 45. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ ((projββ β) βop (projββπ»)) = (projββ(β₯βπ»)) | ||
Theorem | pjidmco 30909 | A projection operator is idempotent. Property (ii) of [Beran] p. 109. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β ((projββπ») β (projββπ»)) = (projββπ»)) | ||
Theorem | dfpjop 30910 | Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 30670. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ (π β ran projβ β (π β HrmOp β§ (π β π) = π)) | ||
Theorem | pjhmopidm 30911 | Two ways to express the set of all projection operators. (Contributed by NM, 24-Apr-2006.) (Proof shortened by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ ran projβ = {π‘ β HrmOp β£ (π‘ β π‘) = π‘} | ||
Theorem | elpjidm 30912 | A projection operator is idempotent. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β (π β π) = π) | ||
Theorem | elpjhmop 30913 | A projection operator is Hermitian. Part of Theorem 26.1 of [Halmos] p. 43. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β π β HrmOp) | ||
Theorem | 0leopj 30914 | A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.) |
β’ (π β ran projβ β 0hop β€op π) | ||
Theorem | pjadj2 30915 | A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β (adjββπ) = π) | ||
Theorem | pjadj3 30916 | A projector is self-adjoint. Property (i) of [Beran] p. 109. (Contributed by NM, 20-Feb-2006.) (New usage is discouraged.) |
β’ (π» β Cβ β (adjββ(projββπ»)) = (projββπ»)) | ||
Theorem | elpjch 30917 | Reconstruction of the subspace of a projection operator. Part of Theorem 26.2 of [Halmos] p. 44. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ (π β ran projβ β (ran π β Cβ β§ π = (projββran π))) | ||
Theorem | elpjrn 30918* | Reconstruction of the subspace of a projection operator. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ (π β ran projβ β ran π = {π₯ β β β£ (πβπ₯) = π₯}) | ||
Theorem | pjinvari 30919 | A closed subspace π» with projection π is invariant under an operator π iff ππ = πππ. Theorem 27.1 of [Halmos] p. 45. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ π: ββΆ β & β’ π» β Cβ & β’ π = (projββπ») β β’ ((π β π): ββΆπ» β (π β π) = (π β (π β π))) | ||
Theorem | pjin1i 30920 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (projββ(πΊ β© π»)) = ((projββπΊ) β (projββ(πΊ β© π»))) | ||
Theorem | pjin2i 30921 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) = ((projββπΊ) β (projββπ»)) β§ (projββπ») = ((projββπ») β (projββπΊ))) β (projββπΊ) = (projββπ»)) | ||
Theorem | pjin3i 30922 | Lemma for Theorem 1.22 of Mittelstaedt, p. 20. (Contributed by NM, 22-Apr-2001.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΉ) = ((projββπΉ) β (projββπΊ)) β§ (projββπΉ) = ((projββπΉ) β (projββπ»))) β (projββπΉ) = ((projββπΉ) β (projββ(πΊ β© π»)))) | ||
Theorem | pjclem1 30923 | Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjclem2 30924 | Lemma for projection commutation theorem. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ))) | ||
Theorem | pjclem3 30925 | Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββ(β₯βπ»))) = ((projββ(β₯βπ»)) β (projββπΊ))) | ||
Theorem | pjclem4a 30926 | Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β (πΊ β© π») β (((projββπΊ) β (projββπ»))βπ΄) = π΄) | ||
Theorem | pjclem4 30927 | Lemma for projection commutation theorem. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjci 30928 | Two subspaces commute iff their projections commute. Lemma 4 of [Kalmbach] p. 67. (Contributed by NM, 26-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ))) | ||
Theorem | pjcmul1i 30929 | A necessary and sufficient condition for the product of two projectors to be a projector is that the projectors commute. Part 1 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββπ»)) β ran projβ) | ||
Theorem | pjcmul2i 30930 | The projection subspace of the difference between two projectors. Part 2 of Theorem 1 of [AkhiezerGlazman] p. 65. (Contributed by NM, 3-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ)) β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjcohocli 30931 | Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π: ββΆ β β β’ (π΄ β β β (((projββπ») β π)βπ΄) β π») | ||
Theorem | pjadj2coi 30932 | Adjoint of double composition of projections. Generalization of special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 1-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ ((π΄ β β β§ π΅ β β) β (((((projββπΉ) β (projββπΊ)) β (projββπ»))βπ΄) Β·ih π΅) = (π΄ Β·ih ((((projββπ») β (projββπΊ)) β (projββπΉ))βπ΅))) | ||
Theorem | pj2cocli 30933 | Closure of double composition of projections. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β ((((projββπΉ) β (projββπΊ)) β (projββπ»))βπ΄) β πΉ) | ||
Theorem | pj3lem1 30934 | Lemma for projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β ((πΉ β© πΊ) β© π») β ((((projββπΉ) β (projββπΊ)) β (projββπ»))βπ΄) = π΄) | ||
Theorem | pj3si 30935 | Stronger projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (((((projββπΉ) β (projββπΊ)) β (projββπ»)) = (((projββπ») β (projββπΊ)) β (projββπΉ)) β§ ran (((projββπΉ) β (projββπΊ)) β (projββπ»)) β πΊ) β (((projββπΉ) β (projββπΊ)) β (projββπ»)) = (projββ((πΉ β© πΊ) β© π»))) | ||
Theorem | pj3i 30936 | Projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (((((projββπΉ) β (projββπΊ)) β (projββπ»)) = (((projββπ») β (projββπΊ)) β (projββπΉ)) β§ (((projββπΉ) β (projββπΊ)) β (projββπ»)) = (((projββπΊ) β (projββπΉ)) β (projββπ»))) β (((projββπΉ) β (projββπΊ)) β (projββπ»)) = (projββ((πΉ β© πΊ) β© π»))) | ||
Theorem | pj3cor1i 30937 | Projection triplet corollary. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (((((projββπΉ) β (projββπΊ)) β (projββπ»)) = (((projββπ») β (projββπΊ)) β (projββπΉ)) β§ (((projββπΉ) β (projββπΊ)) β (projββπ»)) = (((projββπΊ) β (projββπΉ)) β (projββπ»))) β (((projββπΉ) β (projββπΊ)) β (projββπ»)) = (((projββπ») β (projββπΉ)) β (projββπΊ))) | ||
Theorem | pjs14i 30938 | Theorem S-14 of Watanabe, p. 486. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (normββ(((projββπ») β (projββπΊ))βπ΄)) β€ (normββ((projββπΊ)βπ΄))) | ||
Definition | df-st 30939* | Define the set of states on a Hilbert lattice. Definition of [Kalmbach] p. 266. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ States = {π β ((0[,]1) βm Cβ ) β£ ((πβ β) = 1 β§ βπ₯ β Cβ βπ¦ β Cβ (π₯ β (β₯βπ¦) β (πβ(π₯ β¨β π¦)) = ((πβπ₯) + (πβπ¦))))} | ||
Definition | df-hst 30940* | Define the set of complex Hilbert-space-valued states on a Hilbert lattice. Definition of CH-states in [Mayet3] p. 9. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ CHStates = {π β ( β βm Cβ ) β£ ((normββ(πβ β)) = 1 β§ βπ₯ β Cβ βπ¦ β Cβ (π₯ β (β₯βπ¦) β (((πβπ₯) Β·ih (πβπ¦)) = 0 β§ (πβ(π₯ β¨β π¦)) = ((πβπ₯) +β (πβπ¦)))))} | ||
Theorem | isst 30941* | Property of a state. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π β States β (π: Cβ βΆ(0[,]1) β§ (πβ β) = 1 β§ βπ₯ β Cβ βπ¦ β Cβ (π₯ β (β₯βπ¦) β (πβ(π₯ β¨β π¦)) = ((πβπ₯) + (πβπ¦))))) | ||
Theorem | ishst 30942* | Property of a complex Hilbert-space-valued state. Definition of CH-states in [Mayet3] p. 9. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (π β CHStates β (π: Cβ βΆ β β§ (normββ(πβ β)) = 1 β§ βπ₯ β Cβ βπ¦ β Cβ (π₯ β (β₯βπ¦) β (((πβπ₯) Β·ih (πβπ¦)) = 0 β§ (πβ(π₯ β¨β π¦)) = ((πβπ₯) +β (πβπ¦)))))) | ||
Theorem | sticl 30943 | [0, 1] closure of the value of a state. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π β States β (π΄ β Cβ β (πβπ΄) β (0[,]1))) | ||
Theorem | stcl 30944 | Real closure of the value of a state. (Contributed by NM, 24-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π β States β (π΄ β Cβ β (πβπ΄) β β)) | ||
Theorem | hstcl 30945 | Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β (πβπ΄) β β) | ||
Theorem | hst1a 30946 | Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (π β CHStates β (normββ(πβ β)) = 1) | ||
Theorem | hstel2 30947 | Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β (β₯βπ΅))) β (((πβπ΄) Β·ih (πβπ΅)) = 0 β§ (πβ(π΄ β¨β π΅)) = ((πβπ΄) +β (πβπ΅)))) | ||
Theorem | hstorth 30948 | Orthogonality property of a Hilbert-space-valued state. This is a key feature distinguishing it from a real-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β (β₯βπ΅))) β ((πβπ΄) Β·ih (πβπ΅)) = 0) | ||
Theorem | hstosum 30949 | Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β (β₯βπ΅))) β (πβ(π΄ β¨β π΅)) = ((πβπ΄) +β (πβπ΅))) | ||
Theorem | hstoc 30950 | Sum of a Hilbert-space-valued state of a lattice element and its orthocomplement. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β ((πβπ΄) +β (πβ(β₯βπ΄))) = (πβ β)) | ||
Theorem | hstnmoc 30951 | Sum of norms of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β (((normββ(πβπ΄))β2) + ((normββ(πβ(β₯βπ΄)))β2)) = 1) | ||
Theorem | stge0 30952 | The value of a state is nonnegative. (Contributed by NM, 24-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π β States β (π΄ β Cβ β 0 β€ (πβπ΄))) | ||
Theorem | stle1 30953 | The value of a state is less than or equal to one. (Contributed by NM, 24-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π β States β (π΄ β Cβ β (πβπ΄) β€ 1)) | ||
Theorem | hstle1 30954 | The norm of the value of a Hilbert-space-valued state is less than or equal to one. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β (normββ(πβπ΄)) β€ 1) | ||
Theorem | hst1h 30955 | The norm of a Hilbert-space-valued state equals one iff the state value equals the state value of the lattice one. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β ((normββ(πβπ΄)) = 1 β (πβπ΄) = (πβ β))) | ||
Theorem | hst0h 30956 | The norm of a Hilbert-space-valued state equals zero iff the state value equals zero. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β ((normββ(πβπ΄)) = 0 β (πβπ΄) = 0β)) | ||
Theorem | hstpyth 30957 | Pythagorean property of a Hilbert-space-valued state for orthogonal vectors π΄ and π΅. (Contributed by NM, 26-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β (β₯βπ΅))) β ((normββ(πβ(π΄ β¨β π΅)))β2) = (((normββ(πβπ΄))β2) + ((normββ(πβπ΅))β2))) | ||
Theorem | hstle 30958 | Ordering property of a Hilbert-space-valued state. (Contributed by NM, 26-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β π΅)) β (normββ(πβπ΄)) β€ (normββ(πβπ΅))) | ||
Theorem | hstles 30959 | Ordering property of a Hilbert-space-valued state. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β π΅)) β ((normββ(πβπ΄)) = 1 β (normββ(πβπ΅)) = 1)) | ||
Theorem | hstoh 30960 | A Hilbert-space-valued state orthogonal to the state of the lattice one is zero. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ β§ ((πβπ΄) Β·ih (πβ β)) = 0) β (πβπ΄) = 0β) | ||
Theorem | hst0 30961 | A Hilbert-space-valued state is zero at the zero subspace. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ (π β CHStates β (πβ0β) = 0β) | ||
Theorem | sthil 30962 | The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ (π β States β (πβ β) = 1) | ||
Theorem | stj 30963 | The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ (π β States β (((π΄ β Cβ β§ π΅ β Cβ ) β§ π΄ β (β₯βπ΅)) β (πβ(π΄ β¨β π΅)) = ((πβπ΄) + (πβπ΅)))) | ||
Theorem | sto1i 30964 | The state of a subspace plus the state of its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (π β States β ((πβπ΄) + (πβ(β₯βπ΄))) = 1) | ||
Theorem | sto2i 30965 | The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (π β States β (πβ(β₯βπ΄)) = (1 β (πβπ΄))) | ||
Theorem | stge1i 30966 | If a state is greater than or equal to 1, it is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (π β States β (1 β€ (πβπ΄) β (πβπ΄) = 1)) | ||
Theorem | stle0i 30967 | If a state is less than or equal to 0, it is 0. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (π β States β ((πβπ΄) β€ 0 β (πβπ΄) = 0)) | ||
Theorem | stlei 30968 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (π΄ β π΅ β (πβπ΄) β€ (πβπ΅))) | ||
Theorem | stlesi 30969 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (π΄ β π΅ β ((πβπ΄) = 1 β (πβπ΅) = 1))) | ||
Theorem | stji1i 30970 | Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (πβ((β₯βπ΄) β¨β (π΄ β© π΅))) = ((πβ(β₯βπ΄)) + (πβ(π΄ β© π΅)))) | ||
Theorem | stm1i 30971 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β ((πβ(π΄ β© π΅)) = 1 β (πβπ΄) = 1)) | ||
Theorem | stm1ri 30972 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β ((πβ(π΄ β© π΅)) = 1 β (πβπ΅) = 1)) | ||
Theorem | stm1addi 30973 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β ((πβ(π΄ β© π΅)) = 1 β ((πβπ΄) + (πβπ΅)) = 2)) | ||
Theorem | staddi 30974 | If the sum of 2 states is 2, then each state is 1. (Contributed by NM, 12-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (((πβπ΄) + (πβπ΅)) = 2 β (πβπ΄) = 1)) | ||
Theorem | stm1add3i 30975 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ & β’ πΆ β Cβ β β’ (π β States β ((πβ((π΄ β© π΅) β© πΆ)) = 1 β (((πβπ΄) + (πβπ΅)) + (πβπΆ)) = 3)) | ||
Theorem | stadd3i 30976 | If the sum of 3 states is 3, then each state is 1. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ & β’ πΆ β Cβ β β’ (π β States β ((((πβπ΄) + (πβπ΅)) + (πβπΆ)) = 3 β (πβπ΄) = 1)) | ||
Theorem | st0 30977 | The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ (π β States β (πβ0β) = 0) | ||
Theorem | strlem1 30978* | Lemma for strong state theorem: if closed subspace π΄ is not contained in π΅, there is a unit vector π’ in their difference. (Contributed by NM, 25-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (Β¬ π΄ β π΅ β βπ’ β (π΄ β π΅)(normββπ’) = 1) | ||
Theorem | strlem2 30979* | Lemma for strong state theorem. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) β β’ (πΆ β Cβ β (πβπΆ) = ((normββ((projββπΆ)βπ’))β2)) | ||
Theorem | strlem3a 30980* | Lemma for strong state theorem: the function π, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) β β’ ((π’ β β β§ (normββπ’) = 1) β π β States) | ||
Theorem | strlem3 30981* | Lemma for strong state theorem: the function π, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 28-Oct-1999.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β π β States) | ||
Theorem | strlem4 30982* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β (πβπ΄) = 1) | ||
Theorem | strlem5 30983* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β (πβπ΅) < 1) | ||
Theorem | strlem6 30984* | Lemma for strong state theorem. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β Β¬ ((πβπ΄) = 1 β (πβπ΅) = 1)) | ||
Theorem | stri 30985* | Strong state theorem. The states on a Hilbert lattice define an ordering. Remark in [Mayet] p. 370. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (βπ β States ((πβπ΄) = 1 β (πβπ΅) = 1) β π΄ β π΅) | ||
Theorem | strb 30986* | Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (βπ β States ((πβπ΄) = 1 β (πβπ΅) = 1) β π΄ β π΅) | ||
Theorem | hstrlem2 30987* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) β β’ (πΆ β Cβ β (πβπΆ) = ((projββπΆ)βπ’)) | ||
Theorem | hstrlem3a 30988* | Lemma for strong set of CH states theorem: the function π, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) β β’ ((π’ β β β§ (normββπ’) = 1) β π β CHStates) | ||
Theorem | hstrlem3 30989* | Lemma for strong set of CH states theorem: the function π, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a state. This lemma restates the hypotheses in a more convenient form to work with. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β π β CHStates) | ||
Theorem | hstrlem4 30990* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β (normββ(πβπ΄)) = 1) | ||
Theorem | hstrlem5 30991* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β (normββ(πβπ΅)) < 1) | ||
Theorem | hstrlem6 30992* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) & β’ (π β (π’ β (π΄ β π΅) β§ (normββπ’) = 1)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β Β¬ ((normββ(πβπ΄)) = 1 β (normββ(πβπ΅)) = 1)) | ||
Theorem | hstri 30993* | Hilbert space admits a strong set of Hilbert-space-valued states (CH-states). Theorem in [Mayet3] p. 10. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (βπ β CHStates ((normββ(πβπ΄)) = 1 β (normββ(πβπ΅)) = 1) β π΄ β π΅) | ||
Theorem | hstrbi 30994* | Strong CH-state theorem (bidirectional version). Theorem in [Mayet3] p. 10 and its converse. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (βπ β CHStates ((normββ(πβπ΄)) = 1 β (normββ(πβπ΅)) = 1) β π΄ β π΅) | ||
Theorem | largei 30995* | A Hilbert lattice admits a largei set of states. Remark in [Mayet] p. 370. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (Β¬ π΄ = 0β β βπ β States (πβπ΄) = 1) | ||
Theorem | jplem1 30996 | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ ((π’ β β β§ (normββπ’) = 1) β (π’ β π΄ β ((normββ((projββπ΄)βπ’))β2) = 1)) | ||
Theorem | jplem2 30997* | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) & β’ π΄ β Cβ β β’ ((π’ β β β§ (normββπ’) = 1) β (π’ β π΄ β (πβπ΄) = 1)) | ||
Theorem | jpi 30998* | The function π, that maps a closed subspace to the square of the norm of its projection onto a unit vector, is a Jauch-Piron state. Remark in [Mayet] p. 370. (See strlem3a 30980 for the proof that π is a state.) (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((normββ((projββπ₯)βπ’))β2)) & β’ π΄ β Cβ & β’ π΅ β Cβ β β’ ((π’ β β β§ (normββπ’) = 1) β (((πβπ΄) = 1 β§ (πβπ΅) = 1) β (πβ(π΄ β© π΅)) = 1)) | ||
Theorem | golem1 30999 | Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ & β’ πΆ β Cβ & β’ πΉ = ((β₯βπ΄) β¨β (π΄ β© π΅)) & β’ πΊ = ((β₯βπ΅) β¨β (π΅ β© πΆ)) & β’ π» = ((β₯βπΆ) β¨β (πΆ β© π΄)) & β’ π· = ((β₯βπ΅) β¨β (π΅ β© π΄)) & β’ π = ((β₯βπΆ) β¨β (πΆ β© π΅)) & β’ π = ((β₯βπ΄) β¨β (π΄ β© πΆ)) β β’ (π β States β (((πβπΉ) + (πβπΊ)) + (πβπ»)) = (((πβπ·) + (πβπ )) + (πβπ))) | ||
Theorem | golem2 31000 | Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ & β’ πΆ β Cβ & β’ πΉ = ((β₯βπ΄) β¨β (π΄ β© π΅)) & β’ πΊ = ((β₯βπ΅) β¨β (π΅ β© πΆ)) & β’ π» = ((β₯βπΆ) β¨β (πΆ β© π΄)) & β’ π· = ((β₯βπ΅) β¨β (π΅ β© π΄)) & β’ π = ((β₯βπΆ) β¨β (πΆ β© π΅)) & β’ π = ((β₯βπ΄) β¨β (π΄ β© πΆ)) β β’ (π β States β ((πβ((πΉ β© πΊ) β© π»)) = 1 β (πβπ·) = 1)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |