Home | Metamath
Proof Explorer Theorem List (p. 300 of 449) | < 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-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pjclem3 29901 | 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 29902 | Lemma for projection commutation theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ (𝐺 ∩ 𝐻) → (((projℎ‘𝐺) ∘ (projℎ‘𝐻))‘𝐴) = 𝐴) | ||
Theorem | pjclem4 29903 | 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 29904 | 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 29905 | 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 29906 | 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 29907 | Closure of composition of projection and Hilbert space operator. (Contributed by NM, 3-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ & ⊢ 𝑇: ℋ⟶ ℋ ⇒ ⊢ (𝐴 ∈ ℋ → (((projℎ‘𝐻) ∘ 𝑇)‘𝐴) ∈ 𝐻) | ||
Theorem | pjadj2coi 29908 | 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 29909 | Closure of double composition of projections. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ℋ → ((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) ∈ 𝐹) | ||
Theorem | pj3lem1 29910 | Lemma for projection triplet theorem. (Contributed by NM, 2-Dec-2000.) (New usage is discouraged.) |
⊢ 𝐹 ∈ Cℋ & ⊢ 𝐺 ∈ Cℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (𝐴 ∈ ((𝐹 ∩ 𝐺) ∩ 𝐻) → ((((projℎ‘𝐹) ∘ (projℎ‘𝐺)) ∘ (projℎ‘𝐻))‘𝐴) = 𝐴) | ||
Theorem | pj3si 29911 | 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 29912 | 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 29913 | 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 29914 | 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 29915* | 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 29916* | 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 29917* | 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 29918* | 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 29919 | [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 29920 | 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 29921 | Closure of the value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → (𝑆‘𝐴) ∈ ℋ) | ||
Theorem | hst1a 29922 | Unit value of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
⊢ (𝑆 ∈ CHStates → (normℎ‘(𝑆‘ ℋ)) = 1) | ||
Theorem | hstel2 29923 | Properties of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → (((𝑆‘𝐴) ·ih (𝑆‘𝐵)) = 0 ∧ (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵)))) | ||
Theorem | hstorth 29924 | 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 29925 | Orthogonal sum property of a Hilbert-space-valued state. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
⊢ (((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) ∧ (𝐵 ∈ Cℋ ∧ 𝐴 ⊆ (⊥‘𝐵))) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) +ℎ (𝑆‘𝐵))) | ||
Theorem | hstoc 29926 | 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 29927 | 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 29928 | 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 29929 | 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 29930 | 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 29931 | The norm of a Hilbert-space-valued state equals one iff the state value equals the state value of the lattice unit. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ) → ((normℎ‘(𝑆‘𝐴)) = 1 ↔ (𝑆‘𝐴) = (𝑆‘ ℋ))) | ||
Theorem | hst0h 29932 | 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 29933 | 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 29934 | 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 29935 | 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 29936 | A Hilbert-space-valued state orthogonal to the state of the lattice unit is zero. (Contributed by NM, 25-Jun-2006.) (New usage is discouraged.) |
⊢ ((𝑆 ∈ CHStates ∧ 𝐴 ∈ Cℋ ∧ ((𝑆‘𝐴) ·ih (𝑆‘ ℋ)) = 0) → (𝑆‘𝐴) = 0ℎ) | ||
Theorem | hst0 29937 | 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 29938 | The value of a state at the full Hilbert space. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
⊢ (𝑆 ∈ States → (𝑆‘ ℋ) = 1) | ||
Theorem | stj 29939 | The value of a state on a join. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
⊢ (𝑆 ∈ States → (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ 𝐴 ⊆ (⊥‘𝐵)) → (𝑆‘(𝐴 ∨ℋ 𝐵)) = ((𝑆‘𝐴) + (𝑆‘𝐵)))) | ||
Theorem | sto1i 29940 | 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 29941 | The state of the orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → (𝑆‘(⊥‘𝐴)) = (1 − (𝑆‘𝐴))) | ||
Theorem | stge1i 29942 | 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 29943 | 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 29944 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → (𝑆‘𝐴) ≤ (𝑆‘𝐵))) | ||
Theorem | stlesi 29945 | Ordering law for states. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → (𝐴 ⊆ 𝐵 → ((𝑆‘𝐴) = 1 → (𝑆‘𝐵) = 1))) | ||
Theorem | stji1i 29946 | Join of components of Sasaki arrow ->1. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → (𝑆‘((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵))) = ((𝑆‘(⊥‘𝐴)) + (𝑆‘(𝐴 ∩ 𝐵)))) | ||
Theorem | stm1i 29947 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐴) = 1)) | ||
Theorem | stm1ri 29948 | State of component of unit meet. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → (𝑆‘𝐵) = 1)) | ||
Theorem | stm1addi 29949 | Sum of states whose meet is 1. (Contributed by NM, 11-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝑆 ∈ States → ((𝑆‘(𝐴 ∩ 𝐵)) = 1 → ((𝑆‘𝐴) + (𝑆‘𝐵)) = 2)) | ||
Theorem | staddi 29950 | 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 29951 | 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 29952 | 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 29953 | The state of the zero subspace. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (𝑆 ∈ States → (𝑆‘0ℋ) = 0) | ||
Theorem | strlem1 29954* | 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 29955* | 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 29956* | 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 29957* | 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 29958* | 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 29959* | 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 29960* | 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 29961* | 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 29962* | Strong state theorem (bidirectional version). (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (∀𝑓 ∈ States ((𝑓‘𝐴) = 1 → (𝑓‘𝐵) = 1) ↔ 𝐴 ⊆ 𝐵) | ||
Theorem | hstrlem2 29963* | Lemma for strong set of CH states theorem. (Contributed by NM, 30-Jun-2006.) (New usage is discouraged.) |
⊢ 𝑆 = (𝑥 ∈ Cℋ ↦ ((projℎ‘𝑥)‘𝑢)) ⇒ ⊢ (𝐶 ∈ Cℋ → (𝑆‘𝐶) = ((projℎ‘𝐶)‘𝑢)) | ||
Theorem | hstrlem3a 29964* | 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 29965* | 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 29966* | 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 29967* | 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 29968* | 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 29969* | 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 29970* | 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 29971* | 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 29972 | Lemma for Jauch-Piron theorem. (Contributed by NM, 8-Apr-2001.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ ((𝑢 ∈ ℋ ∧ (normℎ‘𝑢) = 1) → (𝑢 ∈ 𝐴 ↔ ((normℎ‘((projℎ‘𝐴)‘𝑢))↑2) = 1)) | ||
Theorem | jplem2 29973* | 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 29974* | 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 29956 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 29975 | Lemma for Godowski's equation. (Contributed by NM, 10-Nov-2002.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵)) & ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)) & ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)) & ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴)) & ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)) & ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶)) ⇒ ⊢ (𝑓 ∈ States → (((𝑓‘𝐹) + (𝑓‘𝐺)) + (𝑓‘𝐻)) = (((𝑓‘𝐷) + (𝑓‘𝑅)) + (𝑓‘𝑆))) | ||
Theorem | golem2 29976 | Lemma for Godowski's equation. (Contributed by NM, 13-Nov-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐹 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐵)) & ⊢ 𝐺 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐶)) & ⊢ 𝐻 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐴)) & ⊢ 𝐷 = ((⊥‘𝐵) ∨ℋ (𝐵 ∩ 𝐴)) & ⊢ 𝑅 = ((⊥‘𝐶) ∨ℋ (𝐶 ∩ 𝐵)) & ⊢ 𝑆 = ((⊥‘𝐴) ∨ℋ (𝐴 ∩ 𝐶)) ⇒ ⊢ (𝑓 ∈ States → ((𝑓‘((𝐹 ∩ 𝐺) ∩ 𝐻)) = 1 → (𝑓‘𝐷) = 1)) | ||
Theorem | goeqi 29977 | 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 29978* | 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 29979* | 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 29980* | 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 29981* | 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 29982* | 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 29983* | 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 29986 and cvbr2 29987 for membership relations. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
⊢ ⋖ℋ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ (𝑥 ⊊ 𝑦 ∧ ¬ ∃𝑧 ∈ Cℋ (𝑥 ⊊ 𝑧 ∧ 𝑧 ⊊ 𝑦)))} | ||
Definition | df-md 29984* | 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 29998 for membership relation. (Contributed by NM, 14-Jun-2004.) (New usage is discouraged.) |
⊢ 𝑀ℋ = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑧 ⊆ 𝑦 → ((𝑧 ∨ℋ 𝑥) ∩ 𝑦) = (𝑧 ∨ℋ (𝑥 ∩ 𝑦))))} | ||
Definition | df-dmd 29985* | 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 30003 for membership relation. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
⊢ 𝑀ℋ* = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ Cℋ ∧ 𝑦 ∈ Cℋ ) ∧ ∀𝑧 ∈ Cℋ (𝑦 ⊆ 𝑧 → ((𝑧 ∩ 𝑥) ∨ℋ 𝑦) = (𝑧 ∩ (𝑥 ∨ℋ 𝑦))))} | ||
Theorem | cvbr 29986* | 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 29987* | 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 29988 | Contraposition law for the covers relation. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 ↔ (⊥‘𝐵) ⋖ℋ (⊥‘𝐴))) | ||
Theorem | cvpss 29989 | The covers relation implies proper subset. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → 𝐴 ⊊ 𝐵)) | ||
Theorem | cvnbtwn 29990 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ (𝐴 ⊊ 𝐶 ∧ 𝐶 ⊊ 𝐵))) | ||
Theorem | cvnbtwn2 29991 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊊ 𝐶 ∧ 𝐶 ⊆ 𝐵) → 𝐶 = 𝐵))) | ||
Theorem | cvnbtwn3 29992 | The covers relation implies no in-betweenness. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ((𝐴 ⊆ 𝐶 ∧ 𝐶 ⊊ 𝐵) → 𝐶 = 𝐴))) | ||
Theorem | cvnbtwn4 29993 | 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 29994 | The covers relation is not symmetric. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⋖ℋ 𝐵 → ¬ 𝐵 ⋖ℋ 𝐴)) | ||
Theorem | cvnref 29995 | The covers relation is not reflexive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → ¬ 𝐴 ⋖ℋ 𝐴) | ||
Theorem | cvntr 29996 | The covers relation is not transitive. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⋖ℋ 𝐵 ∧ 𝐵 ⋖ℋ 𝐶) → ¬ 𝐴 ⋖ℋ 𝐶)) | ||
Theorem | spansncv2 29997 | 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 29998* | 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 29999 | Consequence of the modular pair property. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ (𝐴 𝑀ℋ 𝐵 ∧ 𝐶 ⊆ 𝐵)) → ((𝐶 ∨ℋ 𝐴) ∩ 𝐵) = (𝐶 ∨ℋ (𝐴 ∩ 𝐵))) | ||
Theorem | mdbr2 30000* | Binary relation expressing the modular pair property. This version has a weaker constraint than mdbr 29998. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 𝑀ℋ 𝐵 ↔ ∀𝑥 ∈ Cℋ (𝑥 ⊆ 𝐵 → ((𝑥 ∨ℋ 𝐴) ∩ 𝐵) ⊆ (𝑥 ∨ℋ (𝐴 ∩ 𝐵))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |