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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pjadjcoi 30901 | Adjoint of composition of projections. Special case of Theorem 3.11(viii) of [Beran] p. 106. (Contributed by NM, 6-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ ((π΄ β β β§ π΅ β β) β ((((projββπΊ) β (projββπ»))βπ΄) Β·ih π΅) = (π΄ Β·ih (((projββπ») β (projββπΊ))βπ΅))) | ||
Theorem | pjcofni 30902 | Functionality of composition of projections. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ ((projββπΊ) β (projββπ»)) Fn β | ||
Theorem | pjss1coi 30903 | Subset relationship for projections. Theorem 4.5(i)<->(iii) of [Beran] p. 112. (Contributed by NM, 1-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») β (projββπΊ)) = (projββπΊ)) | ||
Theorem | pjss2coi 30904 | Subset relationship for projections. Theorem 4.5(i)<->(ii) of [Beran] p. 112. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπΊ) β (projββπ»)) = (projββπΊ)) | ||
Theorem | pjssmi 30905 | Projection meet property. Remark in [Kalmbach] p. 66. Also Theorem 4.5(i)->(iv) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (π» β πΊ β (((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) = ((projββ(πΊ β© (β₯βπ»)))βπ΄))) | ||
Theorem | pjssge0i 30906 | Theorem 4.5(iv)->(v) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β ((((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) = ((projββ(πΊ β© (β₯βπ»)))βπ΄) β 0 β€ ((((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) Β·ih π΄))) | ||
Theorem | pjdifnormi 30907 | Theorem 4.5(v)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β (0 β€ ((((projββπΊ)βπ΄) ββ ((projββπ»)βπ΄)) Β·ih π΄) β (normββ((projββπ»)βπ΄)) β€ (normββ((projββπΊ)βπ΄)))) | ||
Theorem | pjnormssi 30908* | Theorem 4.5(i)<->(vi) of [Beran] p. 112. (Contributed by NM, 26-Sep-2001.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β βπ₯ β β (normββ((projββπΊ)βπ₯)) β€ (normββ((projββπ»)βπ₯))) | ||
Theorem | pjorthcoi 30909 | Composition of projections of orthogonal subspaces. Part (i)->(iia) of Theorem 27.4 of [Halmos] p. 45. (Contributed by NM, 6-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β (β₯βπ») β ((projββπΊ) β (projββπ»)) = 0hop ) | ||
Theorem | pjscji 30910 | The projection of orthogonal subspaces is the sum of the projections. (Contributed by NM, 11-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β (β₯βπ») β (projββ(πΊ β¨β π»)) = ((projββπΊ) +op (projββπ»))) | ||
Theorem | pjssumi 30911 | 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ββπΊ) +op (projββπ»))) | ||
Theorem | pjssposi 30912* | Projector ordering can be expressed by the subset relationship between their projection subspaces. (i)<->(iii) of Theorem 29.2 of [Halmos] p. 48. (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (βπ₯ β β 0 β€ ((((projββπ») βop (projββπΊ))βπ₯) Β·ih π₯) β πΊ β π») | ||
Theorem | pjordi 30913* | 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 30912). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (βπ₯ β β 0 β€ ((((projββπ») βop (projββπΊ))βπ₯) Β·ih π₯) β ((projββπΊ) β β) β ((projββπ») β β)) | ||
Theorem | pjssdif2i 30914 | The projection subspace of the difference between two projectors. Part 2 of Theorem 29.3 of [Halmos] p. 48 (shortened with pjssposi 30912). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) = (projββ(π» β© (β₯βπΊ)))) | ||
Theorem | pjssdif1i 30915 | 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 30912). (Contributed by NM, 2-Jun-2006.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ β π» β ((projββπ») βop (projββπΊ)) β ran projβ) | ||
Theorem | pjimai 30916 | 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 30917 | 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 30918 | 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 30919 | 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 30920 | 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 30921 | 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 30922 | Definition of projection operator in [Hughes] p. 47, except that we do not need linearity to be explicit by virtue of hmoplin 30682. (Contributed by NM, 24-Apr-2006.) (Revised by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ (π β ran projβ β (π β HrmOp β§ (π β π) = π)) | ||
Theorem | pjhmopidm 30923 | 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 30924 | 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 30925 | 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 30926 | A projector is a positive operator. (Contributed by NM, 27-Sep-2008.) (New usage is discouraged.) |
β’ (π β ran projβ β 0hop β€op π) | ||
Theorem | pjadj2 30927 | 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 30928 | 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 30929 | 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 30930* | 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 30931 | 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 30932 | 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 30933 | 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 30934 | 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 30935 | Lemma for projection commutation theorem. (Contributed by NM, 16-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = (projββ(πΊ β© π»))) | ||
Theorem | pjclem2 30936 | Lemma for projection commutation theorem. (Contributed by NM, 17-Nov-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (πΊ πΆβ π» β ((projββπΊ) β (projββπ»)) = ((projββπ») β (projββπΊ))) | ||
Theorem | pjclem3 30937 | 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 30938 | Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β (πΊ β© π») β (((projββπΊ) β (projββπ»))βπ΄) = π΄) | ||
Theorem | pjclem4 30939 | 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 30940 | 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 30941 | 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 30942 | 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 30943 | Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π: ββΆ β β β’ (π΄ β β β (((projββπ») β π)βπ΄) β π») | ||
Theorem | pjadj2coi 30944 | 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 30945 | Closure of double composition of projections. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β β β ((((projββπΉ) β (projββπΊ)) β (projββπ»))βπ΄) β πΉ) | ||
Theorem | pj3lem1 30946 | Lemma for projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
β’ πΉ β Cβ & β’ πΊ β Cβ & β’ π» β Cβ β β’ (π΄ β ((πΉ β© πΊ) β© π») β ((((projββπΉ) β (projββπΊ)) β (projββπ»))βπ΄) = π΄) | ||
Theorem | pj3si 30947 | 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 30948 | 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 30949 | 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 30950 | 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 30951* | 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 30952* | 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 30953* | 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 30954* | 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 30955 | [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 30956 | 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 30957 | Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ ((π β CHStates β§ π΄ β Cβ ) β (πβπ΄) β β) | ||
Theorem | hst1a 30958 | Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (π β CHStates β (normββ(πβ β)) = 1) | ||
Theorem | hstel2 30959 | Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β (β₯βπ΅))) β (((πβπ΄) Β·ih (πβπ΅)) = 0 β§ (πβ(π΄ β¨β π΅)) = ((πβπ΄) +β (πβπ΅)))) | ||
Theorem | hstorth 30960 | 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 30961 | Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
β’ (((π β CHStates β§ π΄ β Cβ ) β§ (π΅ β Cβ β§ π΄ β (β₯βπ΅))) β (πβ(π΄ β¨β π΅)) = ((πβπ΄) +β (πβπ΅))) | ||
Theorem | hstoc 30962 | 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 30963 | 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 30964 | 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 30965 | 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 30966 | 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 30967 | 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 30968 | 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 30969 | 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 30970 | 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 30971 | 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 30972 | 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 30973 | 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 30974 | The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ (π β States β (πβ β) = 1) | ||
Theorem | stj 30975 | The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ (π β States β (((π΄ β Cβ β§ π΅ β Cβ ) β§ π΄ β (β₯βπ΅)) β (πβ(π΄ β¨β π΅)) = ((πβπ΄) + (πβπ΅)))) | ||
Theorem | sto1i 30976 | 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 30977 | The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (π β States β (πβ(β₯βπ΄)) = (1 β (πβπ΄))) | ||
Theorem | stge1i 30978 | 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 30979 | 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 30980 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (π΄ β π΅ β (πβπ΄) β€ (πβπ΅))) | ||
Theorem | stlesi 30981 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (π΄ β π΅ β ((πβπ΄) = 1 β (πβπ΅) = 1))) | ||
Theorem | stji1i 30982 | Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β (πβ((β₯βπ΄) β¨β (π΄ β© π΅))) = ((πβ(β₯βπ΄)) + (πβ(π΄ β© π΅)))) | ||
Theorem | stm1i 30983 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β ((πβ(π΄ β© π΅)) = 1 β (πβπ΄) = 1)) | ||
Theorem | stm1ri 30984 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β ((πβ(π΄ β© π΅)) = 1 β (πβπ΅) = 1)) | ||
Theorem | stm1addi 30985 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π β States β ((πβ(π΄ β© π΅)) = 1 β ((πβπ΄) + (πβπ΅)) = 2)) | ||
Theorem | staddi 30986 | 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 30987 | 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 30988 | 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 30989 | The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
β’ (π β States β (πβ0β) = 0) | ||
Theorem | strlem1 30990* | 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 30991* | 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 30992* | 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 30993* | 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 30994* | 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 30995* | 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 30996* | 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 30997* | 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 30998* | Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (βπ β States ((πβπ΄) = 1 β (πβπ΅) = 1) β π΄ β π΅) | ||
Theorem | hstrlem2 30999* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
β’ π = (π₯ β Cβ β¦ ((projββπ₯)βπ’)) β β’ (πΆ β Cβ β (πβπΆ) = ((projββπΆ)βπ’)) | ||
Theorem | hstrlem3a 31000* | 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) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |