![]() |
Metamath
Proof Explorer Theorem List (p. 316 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 | pjs14i 31501 | 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 31502* | 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 31503* | 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 31504* | 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 31505* | 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 31506 | [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 31507 | 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 31508 | Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
โข ((๐ โ CHStates โง ๐ด โ Cโ ) โ (๐โ๐ด) โ โ) | ||
Theorem | hst1a 31509 | Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
โข (๐ โ CHStates โ (normโโ(๐โ โ)) = 1) | ||
Theorem | hstel2 31510 | Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
โข (((๐ โ CHStates โง ๐ด โ Cโ ) โง (๐ต โ Cโ โง ๐ด โ (โฅโ๐ต))) โ (((๐โ๐ด) ยทih (๐โ๐ต)) = 0 โง (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต)))) | ||
Theorem | hstorth 31511 | 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 31512 | Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
โข (((๐ โ CHStates โง ๐ด โ Cโ ) โง (๐ต โ Cโ โง ๐ด โ (โฅโ๐ต))) โ (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) +โ (๐โ๐ต))) | ||
Theorem | hstoc 31513 | 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 31514 | 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 31515 | 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 31516 | 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 31517 | 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 31518 | 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 31519 | 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 31520 | 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 31521 | 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 31522 | 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 31523 | 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 31524 | 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 31525 | The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ States โ (๐โ โ) = 1) | ||
Theorem | stj 31526 | The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ States โ (((๐ด โ Cโ โง ๐ต โ Cโ ) โง ๐ด โ (โฅโ๐ต)) โ (๐โ(๐ด โจโ ๐ต)) = ((๐โ๐ด) + (๐โ๐ต)))) | ||
Theorem | sto1i 31527 | 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 31528 | The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ โ โข (๐ โ States โ (๐โ(โฅโ๐ด)) = (1 โ (๐โ๐ด))) | ||
Theorem | stge1i 31529 | 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 31530 | 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 31531 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ States โ (๐ด โ ๐ต โ (๐โ๐ด) โค (๐โ๐ต))) | ||
Theorem | stlesi 31532 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ States โ (๐ด โ ๐ต โ ((๐โ๐ด) = 1 โ (๐โ๐ต) = 1))) | ||
Theorem | stji1i 31533 | Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ States โ (๐โ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต))) = ((๐โ(โฅโ๐ด)) + (๐โ(๐ด โฉ ๐ต)))) | ||
Theorem | stm1i 31534 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ States โ ((๐โ(๐ด โฉ ๐ต)) = 1 โ (๐โ๐ด) = 1)) | ||
Theorem | stm1ri 31535 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ States โ ((๐โ(๐ด โฉ ๐ต)) = 1 โ (๐โ๐ต) = 1)) | ||
Theorem | stm1addi 31536 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ States โ ((๐โ(๐ด โฉ ๐ต)) = 1 โ ((๐โ๐ด) + (๐โ๐ต)) = 2)) | ||
Theorem | staddi 31537 | 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 31538 | 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 31539 | 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 31540 | The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ States โ (๐โ0โ) = 0) | ||
Theorem | strlem1 31541* | 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 31542* | 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 31543* | 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 31544* | 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 31545* | 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 31546* | 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 31547* | 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 31548* | 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 31549* | Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (โ๐ โ States ((๐โ๐ด) = 1 โ (๐โ๐ต) = 1) โ ๐ด โ ๐ต) | ||
Theorem | hstrlem2 31550* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
โข ๐ = (๐ฅ โ Cโ โฆ ((projโโ๐ฅ)โ๐ข)) โ โข (๐ถ โ Cโ โ (๐โ๐ถ) = ((projโโ๐ถ)โ๐ข)) | ||
Theorem | hstrlem3a 31551* | 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 31552* | 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 31553* | 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 31554* | 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 31555* | 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 31556* | 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 31557* | 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 31558* | 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 31559 | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
โข ๐ด โ Cโ โ โข ((๐ข โ โ โง (normโโ๐ข) = 1) โ (๐ข โ ๐ด โ ((normโโ((projโโ๐ด)โ๐ข))โ2) = 1)) | ||
Theorem | jplem2 31560* | 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 31561* | 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 31543 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 31562 | Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ & โข ๐ถ โ Cโ & โข ๐น = ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต)) & โข ๐บ = ((โฅโ๐ต) โจโ (๐ต โฉ ๐ถ)) & โข ๐ป = ((โฅโ๐ถ) โจโ (๐ถ โฉ ๐ด)) & โข ๐ท = ((โฅโ๐ต) โจโ (๐ต โฉ ๐ด)) & โข ๐ = ((โฅโ๐ถ) โจโ (๐ถ โฉ ๐ต)) & โข ๐ = ((โฅโ๐ด) โจโ (๐ด โฉ ๐ถ)) โ โข (๐ โ States โ (((๐โ๐น) + (๐โ๐บ)) + (๐โ๐ป)) = (((๐โ๐ท) + (๐โ๐ )) + (๐โ๐))) | ||
Theorem | golem2 31563 | Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ & โข ๐ถ โ Cโ & โข ๐น = ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต)) & โข ๐บ = ((โฅโ๐ต) โจโ (๐ต โฉ ๐ถ)) & โข ๐ป = ((โฅโ๐ถ) โจโ (๐ถ โฉ ๐ด)) & โข ๐ท = ((โฅโ๐ต) โจโ (๐ต โฉ ๐ด)) & โข ๐ = ((โฅโ๐ถ) โจโ (๐ถ โฉ ๐ต)) & โข ๐ = ((โฅโ๐ด) โจโ (๐ด โฉ ๐ถ)) โ โข (๐ โ States โ ((๐โ((๐น โฉ ๐บ) โฉ ๐ป)) = 1 โ (๐โ๐ท) = 1)) | ||
Theorem | goeqi 31564 | Godowski's equation, shown here as a variant equivalent to Equation SF of [Godowski] p. 730. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ & โข ๐ถ โ Cโ & โข ๐น = ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต)) & โข ๐บ = ((โฅโ๐ต) โจโ (๐ต โฉ ๐ถ)) & โข ๐ป = ((โฅโ๐ถ) โจโ (๐ถ โฉ ๐ด)) & โข ๐ท = ((โฅโ๐ต) โจโ (๐ต โฉ ๐ด)) โ โข ((๐น โฉ ๐บ) โฉ ๐ป) โ ๐ท | ||
Theorem | stcltr1i 31565* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ (๐ โ States โง โ๐ฅ โ Cโ โ๐ฆ โ Cโ (((๐โ๐ฅ) = 1 โ (๐โ๐ฆ) = 1) โ ๐ฅ โ ๐ฆ))) & โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ (((๐โ๐ด) = 1 โ (๐โ๐ต) = 1) โ ๐ด โ ๐ต)) | ||
Theorem | stcltr2i 31566* | Property of a strong classical state. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ (๐ โ States โง โ๐ฅ โ Cโ โ๐ฆ โ Cโ (((๐โ๐ฅ) = 1 โ (๐โ๐ฆ) = 1) โ ๐ฅ โ ๐ฆ))) & โข ๐ด โ Cโ โ โข (๐ โ ((๐โ๐ด) = 1 โ ๐ด = โ)) | ||
Theorem | stcltrlem1 31567* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ (๐ โ States โง โ๐ฅ โ Cโ โ๐ฆ โ Cโ (((๐โ๐ฅ) = 1 โ (๐โ๐ฆ) = 1) โ ๐ฅ โ ๐ฆ))) & โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ ((๐โ๐ต) = 1 โ (๐โ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต))) = 1)) | ||
Theorem | stcltrlem2 31568* | Lemma for strong classical state theorem. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข (๐ โ (๐ โ States โง โ๐ฅ โ Cโ โ๐ฆ โ Cโ (((๐โ๐ฅ) = 1 โ (๐โ๐ฆ) = 1) โ ๐ฅ โ ๐ฆ))) & โข ๐ด โ Cโ & โข ๐ต โ Cโ โ โข (๐ โ ๐ต โ ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต))) | ||
Theorem | stcltrthi 31569* | Theorem for classically strong set of states. If there exists a "classically strong set of states" on lattice Cโ (or actually any ortholattice, which would have an identical proof), then any two elements of the lattice commute, i.e., the lattice is distributive. (Proof due to Mladen Pavicic.) Theorem 3.3 of [MegPav2000] p. 2344. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
โข ๐ด โ Cโ & โข ๐ต โ Cโ & โข โ๐ โ States โ๐ฅ โ Cโ โ๐ฆ โ Cโ (((๐ โ๐ฅ) = 1 โ (๐ โ๐ฆ) = 1) โ ๐ฅ โ ๐ฆ) โ โข ๐ต โ ((โฅโ๐ด) โจโ (๐ด โฉ ๐ต)) | ||
Definition | df-cv 31570* | Define the covers relation (on the Hilbert lattice). Definition 3.2.18 of [PtakPulmannova] p. 68, whose notation we use. Ptak/Pulmannova's notation ๐ด โโ ๐ต is read "๐ต covers ๐ด " or "๐ด is covered by ๐ต " , and it means that ๐ต is larger than ๐ด and there is nothing in between. See cvbr 31573 and cvbr2 31574 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
โข โโ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Cโ โง ๐ฆ โ Cโ ) โง (๐ฅ โ ๐ฆ โง ยฌ โ๐ง โ Cโ (๐ฅ โ ๐ง โง ๐ง โ ๐ฆ)))} | ||
Definition | df-md 31571* | Define the modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M for "the ordered pair <x,y> is a modular pair." See mdbr 31585 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
โข ๐โ = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Cโ โง ๐ฆ โ Cโ ) โง โ๐ง โ Cโ (๐ง โ ๐ฆ โ ((๐ง โจโ ๐ฅ) โฉ ๐ฆ) = (๐ง โจโ (๐ฅ โฉ ๐ฆ))))} | ||
Definition | df-dmd 31572* | Define the dual modular pair relation (on the Hilbert lattice). Definition 1.1 of [MaedaMaeda] p. 1, who use the notation (x,y)M* for "the ordered pair <x,y> is a dual modular pair." See dmdbr 31590 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
โข ๐โ* = {โจ๐ฅ, ๐ฆโฉ โฃ ((๐ฅ โ Cโ โง ๐ฆ โ Cโ ) โง โ๐ง โ Cโ (๐ฆ โ ๐ง โ ((๐ง โฉ ๐ฅ) โจโ ๐ฆ) = (๐ง โฉ (๐ฅ โจโ ๐ฆ))))} | ||
Theorem | cvbr 31573* | Binary relation expressing ๐ต covers ๐ด, which means that ๐ต is larger than ๐ด and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด โโ ๐ต โ (๐ด โ ๐ต โง ยฌ โ๐ฅ โ Cโ (๐ด โ ๐ฅ โง ๐ฅ โ ๐ต)))) | ||
Theorem | cvbr2 31574* | Binary relation expressing ๐ต covers ๐ด. Definition of covers in [Kalmbach] p. 15. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด โโ ๐ต โ (๐ด โ ๐ต โง โ๐ฅ โ Cโ ((๐ด โ ๐ฅ โง ๐ฅ โ ๐ต) โ ๐ฅ = ๐ต)))) | ||
Theorem | cvcon3 31575 | Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด โโ ๐ต โ (โฅโ๐ต) โโ (โฅโ๐ด))) | ||
Theorem | cvpss 31576 | The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด โโ ๐ต โ ๐ด โ ๐ต)) | ||
Theorem | cvnbtwn 31577 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โ (๐ด โโ ๐ต โ ยฌ (๐ด โ ๐ถ โง ๐ถ โ ๐ต))) | ||
Theorem | cvnbtwn2 31578 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โ (๐ด โโ ๐ต โ ((๐ด โ ๐ถ โง ๐ถ โ ๐ต) โ ๐ถ = ๐ต))) | ||
Theorem | cvnbtwn3 31579 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โ (๐ด โโ ๐ต โ ((๐ด โ ๐ถ โง ๐ถ โ ๐ต) โ ๐ถ = ๐ด))) | ||
Theorem | cvnbtwn4 31580 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โ (๐ด โโ ๐ต โ ((๐ด โ ๐ถ โง ๐ถ โ ๐ต) โ (๐ถ = ๐ด โจ ๐ถ = ๐ต)))) | ||
Theorem | cvnsym 31581 | The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด โโ ๐ต โ ยฌ ๐ต โโ ๐ด)) | ||
Theorem | cvnref 31582 | The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
โข (๐ด โ Cโ โ ยฌ ๐ด โโ ๐ด) | ||
Theorem | cvntr 31583 | The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โ ((๐ด โโ ๐ต โง ๐ต โโ ๐ถ) โ ยฌ ๐ด โโ ๐ถ)) | ||
Theorem | spansncv2 31584 | Hilbert space has the covering property (using spans of singletons to represent atoms). Proposition 1(ii) of [Kalmbach] p. 153. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ โ) โ (ยฌ (spanโ{๐ต}) โ ๐ด โ ๐ด โโ (๐ด โจโ (spanโ{๐ต})))) | ||
Theorem | mdbr 31585* | Binary relation expressing โจ๐ด, ๐ตโฉ is a modular pair. Definition 1.1 of [MaedaMaeda] p. 1. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ ๐ต โ โ๐ฅ โ Cโ (๐ฅ โ ๐ต โ ((๐ฅ โจโ ๐ด) โฉ ๐ต) = (๐ฅ โจโ (๐ด โฉ ๐ต))))) | ||
Theorem | mdi 31586 | Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
โข (((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โง (๐ด ๐โ ๐ต โง ๐ถ โ ๐ต)) โ ((๐ถ โจโ ๐ด) โฉ ๐ต) = (๐ถ โจโ (๐ด โฉ ๐ต))) | ||
Theorem | mdbr2 31587* | Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 31585. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ ๐ต โ โ๐ฅ โ Cโ (๐ฅ โ ๐ต โ ((๐ฅ โจโ ๐ด) โฉ ๐ต) โ (๐ฅ โจโ (๐ด โฉ ๐ต))))) | ||
Theorem | mdbr3 31588* | Binary relation expressing the modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ ๐ต โ โ๐ฅ โ Cโ (((๐ฅ โฉ ๐ต) โจโ ๐ด) โฉ ๐ต) = ((๐ฅ โฉ ๐ต) โจโ (๐ด โฉ ๐ต)))) | ||
Theorem | mdbr4 31589* | Binary relation expressing the modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ ๐ต โ โ๐ฅ โ Cโ (((๐ฅ โฉ ๐ต) โจโ ๐ด) โฉ ๐ต) โ ((๐ฅ โฉ ๐ต) โจโ (๐ด โฉ ๐ต)))) | ||
Theorem | dmdbr 31590* | Binary relation expressing the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ* ๐ต โ โ๐ฅ โ Cโ (๐ต โ ๐ฅ โ ((๐ฅ โฉ ๐ด) โจโ ๐ต) = (๐ฅ โฉ (๐ด โจโ ๐ต))))) | ||
Theorem | dmdmd 31591 | The dual modular pair property expressed in terms of the modular pair property, that hold in Hilbert lattices. Remark 29.6 of [MaedaMaeda] p. 130. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ* ๐ต โ (โฅโ๐ด) ๐โ (โฅโ๐ต))) | ||
Theorem | mddmd 31592 | The modular pair property expressed in terms of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ ๐ต โ (โฅโ๐ด) ๐โ* (โฅโ๐ต))) | ||
Theorem | dmdi 31593 | Consequence of the dual modular pair property. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
โข (((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โง (๐ด ๐โ* ๐ต โง ๐ต โ ๐ถ)) โ ((๐ถ โฉ ๐ด) โจโ ๐ต) = (๐ถ โฉ (๐ด โจโ ๐ต))) | ||
Theorem | dmdbr2 31594* | Binary relation expressing the dual modular pair property. This version has a weaker constraint than dmdbr 31590. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ* ๐ต โ โ๐ฅ โ Cโ (๐ต โ ๐ฅ โ (๐ฅ โฉ (๐ด โจโ ๐ต)) โ ((๐ฅ โฉ ๐ด) โจโ ๐ต)))) | ||
Theorem | dmdi2 31595 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
โข (((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โง (๐ด ๐โ* ๐ต โง ๐ต โ ๐ถ)) โ (๐ถ โฉ (๐ด โจโ ๐ต)) โ ((๐ถ โฉ ๐ด) โจโ ๐ต)) | ||
Theorem | dmdbr3 31596* | Binary relation expressing the dual modular pair property. This version quantifies an equality instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ* ๐ต โ โ๐ฅ โ Cโ (((๐ฅ โจโ ๐ต) โฉ ๐ด) โจโ ๐ต) = ((๐ฅ โจโ ๐ต) โฉ (๐ด โจโ ๐ต)))) | ||
Theorem | dmdbr4 31597* | Binary relation expressing the dual modular pair property. This version quantifies an ordering instead of an inference. (Contributed by NM, 6-Jul-2004.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ* ๐ต โ โ๐ฅ โ Cโ ((๐ฅ โจโ ๐ต) โฉ (๐ด โจโ ๐ต)) โ (((๐ฅ โจโ ๐ต) โฉ ๐ด) โจโ ๐ต))) | ||
Theorem | dmdi4 31598 | Consequence of the dual modular pair property. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ โง ๐ถ โ Cโ ) โ (๐ด ๐โ* ๐ต โ ((๐ถ โจโ ๐ต) โฉ (๐ด โจโ ๐ต)) โ (((๐ถ โจโ ๐ต) โฉ ๐ด) โจโ ๐ต))) | ||
Theorem | dmdbr5 31599* | Binary relation expressing the dual modular pair property. (Contributed by NM, 15-Jan-2005.) (New usage is discouraged.) |
โข ((๐ด โ Cโ โง ๐ต โ Cโ ) โ (๐ด ๐โ* ๐ต โ โ๐ฅ โ Cโ (๐ฅ โ (๐ด โจโ ๐ต) โ ๐ฅ โ (((๐ฅ โจโ ๐ต) โฉ ๐ด) โจโ ๐ต)))) | ||
Theorem | mddmd2 31600* | Relationship between modular pairs and dual-modular pairs. Lemma 1.2 of [MaedaMaeda] p. 1. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
โข (๐ด โ Cโ โ (โ๐ฅ โ Cโ ๐ด ๐โ ๐ฅ โ โ๐ฅ โ Cโ ๐ด ๐โ* ๐ฅ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |