HomeTheorem List (p. 315 of 499)
GIF version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 315 of 499) | < 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-30893) |
Hilbert Space Explorer
(30894-32416) |
Users' Mathboxes
(32417-49836) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pjpjhthi 31401* | Projection Theorem: Any Hilbert space vector 𝐴 can be decomposed into a member 𝑥 of a closed subspace 𝐻 and a member 𝑦 of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ ∃𝑥 ∈ 𝐻 ∃𝑦 ∈ (⊥‘𝐻)𝐴 = (𝑥 +ℎ 𝑦) | ||
| Theorem | pjop 31402 | Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴))) | ||
| Theorem | pjpo 31403 | Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴))) | ||
| Theorem | pjopi 31404 | Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘(⊥‘𝐻))‘𝐴) = (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)) | ||
| Theorem | pjpoi 31405 | Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ ((projℎ‘𝐻)‘𝐴) = (𝐴 −ℎ ((projℎ‘(⊥‘𝐻))‘𝐴)) | ||
| Theorem | pjoc1i 31406 | Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 ∈ 𝐻 ↔ ((projℎ‘(⊥‘𝐻))‘𝐴) = 0ℎ) | ||
| Theorem | pjchi 31407 | Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 ∈ 𝐻 ↔ ((projℎ‘𝐻)‘𝐴) = 𝐴) | ||
| Theorem | pjoccl 31408 | The part of a vector that belongs to the orthocomplemented space. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 −ℎ ((projℎ‘𝐻)‘𝐴)) ∈ (⊥‘𝐻)) | ||
| Theorem | pjoc1 31409 | Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ 𝐻 ↔ ((projℎ‘(⊥‘𝐻))‘𝐴) = 0ℎ)) | ||
| Theorem | pjomli 31410 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omlsi 31379. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ) → 𝐴 = 𝐵) | ||
| Theorem | pjoml 31411 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omlsi 31379. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Sℋ ) ∧ (𝐴 ⊆ 𝐵 ∧ (𝐵 ∩ (⊥‘𝐴)) = 0ℋ)) → 𝐴 = 𝐵) | ||
| Theorem | pjococi 31412 | Proof of orthocomplement theorem using projections. Compare ococ 31381. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (⊥‘(⊥‘𝐻)) = 𝐻 | ||
| Theorem | pjoc2i 31413 | Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐻 ∈ Cℋ & ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘𝐻) ↔ ((projℎ‘𝐻)‘𝐴) = 0ℎ) | ||
| Theorem | pjoc2 31414 | Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
| ⊢ ((𝐻 ∈ Cℋ ∧ 𝐴 ∈ ℋ) → (𝐴 ∈ (⊥‘𝐻) ↔ ((projℎ‘𝐻)‘𝐴) = 0ℎ)) | ||
| Theorem | sh0le 31415 | The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Sℋ → 0ℋ ⊆ 𝐴) | ||
| Theorem | ch0le 31416 | The zero subspace is the smallest member of Cℋ. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → 0ℋ ⊆ 𝐴) | ||
| Theorem | shle0 31417 | No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Sℋ → (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ)) | ||
| Theorem | chle0 31418 | No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ)) | ||
| Theorem | chnlen0 31419 | A Hilbert lattice element that is not a subset of another is nonzero. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐵 ∈ Cℋ → (¬ 𝐴 ⊆ 𝐵 → ¬ 𝐴 = 0ℋ)) | ||
| Theorem | ch0pss 31420 | The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (0ℋ ⊊ 𝐴 ↔ 𝐴 ≠ 0ℋ)) | ||
| Theorem | orthin 31421 | The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ⊆ (⊥‘𝐵) → (𝐴 ∩ 𝐵) = 0ℋ)) | ||
| Theorem | ssjo 31422 | The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ (𝐴 ⊆ ℋ → (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ) | ||
| Theorem | shne0i 31423* | A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ) | ||
| Theorem | shs0i 31424 | Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 0ℋ) = 𝐴 | ||
| Theorem | shs00i 31425 | Two subspaces are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 = 0ℋ ∧ 𝐵 = 0ℋ) ↔ (𝐴 +ℋ 𝐵) = 0ℋ) | ||
| Theorem | ch0lei 31426 | The closed subspace zero is the smallest member of Cℋ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ 0ℋ ⊆ 𝐴 | ||
| Theorem | chle0i 31427 | No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 0ℋ ↔ 𝐴 = 0ℋ) | ||
| Theorem | chne0i 31428* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ) | ||
| Theorem | chocini 31429 | Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ (⊥‘𝐴)) = 0ℋ | ||
| Theorem | chj0i 31430 | Join with lattice zero in Cℋ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 0ℋ) = 𝐴 | ||
| Theorem | chm1i 31431 | Meet with lattice one in Cℋ. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ ℋ) = 𝐴 | ||
| Theorem | chjcli 31432 | Closure of Cℋ join. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) ∈ Cℋ | ||
| Theorem | chsleji 31433 | Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chseli 31434* | Membership in subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
| Theorem | chincli 31435 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ | ||
| Theorem | chsscon3i 31436 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴)) | ||
| Theorem | chsscon1i 31437 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴) | ||
| Theorem | chsscon2i 31438 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)) | ||
| Theorem | chcon2i 31439 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = (⊥‘𝐵) ↔ 𝐵 = (⊥‘𝐴)) | ||
| Theorem | chcon1i 31440 | Hilbert lattice contraposition law. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) = 𝐵 ↔ (⊥‘𝐵) = 𝐴) | ||
| Theorem | chcon3i 31441 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = 𝐵 ↔ (⊥‘𝐵) = (⊥‘𝐴)) | ||
| Theorem | chunssji 31442 | Union is smaller than Cℋ join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chjcomi 31443 | Commutative law for join in Cℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
| Theorem | chub1i 31444 | Cℋ join is an upper bound of two elements. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chub2i 31445 | Cℋ join is an upper bound of two elements. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐵 ∨ℋ 𝐴) | ||
| Theorem | chlubi 31446 | Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶) | ||
| Theorem | chlubii 31447 | Hilbert lattice join is the least upper bound of two elements (one direction of chlubi 31446). (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ∨ℋ 𝐵) ⊆ 𝐶) | ||
| Theorem | chlej1i 31448 | Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chlej2i 31449 | Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
| Theorem | chlej12i 31450 | Add join to both sides of a Hilbert lattice ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐵 ∧ 𝐶 ⊆ 𝐷) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐷)) | ||
| Theorem | chlejb1i 31451 | Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∨ℋ 𝐵) = 𝐵) | ||
| Theorem | chdmm1i 31452 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)) | ||
| Theorem | chdmm2i 31453 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵)) | ||
| Theorem | chdmm3i 31454 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵) | ||
| Theorem | chdmm4i 31455 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chdmj1i 31456 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵)) | ||
| Theorem | chdmj2i 31457 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵)) | ||
| Theorem | chdmj3i 31458 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵) | ||
| Theorem | chdmj4i 31459 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵) | ||
| Theorem | chnlei 31460 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chjassi 31461 | Associative law for Hilbert lattice join. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chj00i 31462 | Two Hilbert lattice elements are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((𝐴 = 0ℋ ∧ 𝐵 = 0ℋ) ↔ (𝐴 ∨ℋ 𝐵) = 0ℋ) | ||
| Theorem | chjoi 31463 | The join of a closed subspace and its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ | ||
| Theorem | chj1i 31464 | Join with Hilbert lattice one. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ ℋ) = ℋ | ||
| Theorem | chm0i 31465 | Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 0ℋ) = 0ℋ | ||
| Theorem | chm0 31466 | Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∩ 0ℋ) = 0ℋ) | ||
| Theorem | shjshsi 31467 | Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 +ℋ 𝐵))) | ||
| Theorem | shjshseli 31468 | A closed subspace sum equals Hilbert lattice join. Part of Lemma 31.1.5 of [MaedaMaeda] p. 136. (Contributed by NM, 30-Nov-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐴 +ℋ 𝐵) ∈ Cℋ ↔ (𝐴 +ℋ 𝐵) = (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chne0 31469* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ)) | ||
| Theorem | chocin 31470 | Intersection of a closed subspace and its orthocomplement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 13-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) | ||
| Theorem | chssoc 31471 | A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ⊆ (⊥‘𝐴) ↔ 𝐴 = 0ℋ)) | ||
| Theorem | chj0 31472 | Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 0ℋ) = 𝐴) | ||
| Theorem | chslej 31473 | Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chincl 31474 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∩ 𝐵) ∈ Cℋ ) | ||
| Theorem | chsscon3 31475 | Hilbert lattice contraposition law. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
| Theorem | chsscon1 31476 | Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴)) | ||
| Theorem | chsscon2 31477 | Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
| Theorem | chpsscon3 31478 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊊ 𝐵 ↔ (⊥‘𝐵) ⊊ (⊥‘𝐴))) | ||
| Theorem | chpsscon1 31479 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((⊥‘𝐴) ⊊ 𝐵 ↔ (⊥‘𝐵) ⊊ 𝐴)) | ||
| Theorem | chpsscon2 31480 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊊ (⊥‘𝐵) ↔ 𝐵 ⊊ (⊥‘𝐴))) | ||
| Theorem | chjcom 31481 | Commutative law for Hilbert lattice join. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)) | ||
| Theorem | chub1 31482 | Hilbert lattice join is greater than or equal to its first argument. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ⊆ (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chub2 31483 | Hilbert lattice join is greater than or equal to its second argument. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → 𝐴 ⊆ (𝐵 ∨ℋ 𝐴)) | ||
| Theorem | chlub 31484 | Hilbert lattice join is the least upper bound of two elements. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) ↔ (𝐴 ∨ℋ 𝐵) ⊆ 𝐶)) | ||
| Theorem | chlej1 31485 | Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chlej2 31486 | Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
| Theorem | chlejb1 31487 | Hilbert lattice ordering in terms of join. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∨ℋ 𝐵) = 𝐵)) | ||
| Theorem | chlejb2 31488 | Hilbert lattice ordering in terms of join. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐵 ∨ℋ 𝐴) = 𝐵)) | ||
| Theorem | chnle 31489 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | chjo 31490 | The join of a closed subspace and its orthocomplement is all of Hilbert space. (Contributed by NM, 31-Oct-2005.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ) | ||
| Theorem | chabs1 31491 | Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ (𝐴 ∩ 𝐵)) = 𝐴) | ||
| Theorem | chabs2 31492 | Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴) | ||
| Theorem | chabs1i 31493 | Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 10-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐴 ∩ 𝐵)) = 𝐴 | ||
| Theorem | chabs2i 31494 | Hilbert lattice absorption law. From definition of lattice in [Kalmbach] p. 14. (Contributed by NM, 16-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ (𝐴 ∨ℋ 𝐵)) = 𝐴 | ||
| Theorem | chjidm 31495 | Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 𝐴) = 𝐴) | ||
| Theorem | chjidmi 31496 | Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 | ||
| Theorem | chj12i 31497 | A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶)) | ||
| Theorem | chj4i 31498 | Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ & ⊢ 𝐷 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ (𝐶 ∨ℋ 𝐷)) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐷)) | ||
| Theorem | chjjdiri 31499 | Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chdmm1 31500 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |