HomeTheorem List (p. 278 of 424)
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. 278 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | chsleji 27701 | 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 27702* | Membership in subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
| Theorem | chincli 27703 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ Cℋ | ||
| Theorem | chsscon3i 27704 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴)) | ||
| Theorem | chsscon1i 27705 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴) | ||
| Theorem | chsscon2i 27706 | Hilbert lattice contraposition law. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴)) | ||
| Theorem | chcon2i 27707 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = (⊥‘𝐵) ↔ 𝐵 = (⊥‘𝐴)) | ||
| Theorem | chcon1i 27708 | Hilbert lattice contraposition law. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ ((⊥‘𝐴) = 𝐵 ↔ (⊥‘𝐵) = 𝐴) | ||
| Theorem | chcon3i 27709 | Hilbert lattice contraposition law. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 = 𝐵 ↔ (⊥‘𝐵) = (⊥‘𝐴)) | ||
| Theorem | chunssji 27710 | Union is smaller than Cℋ join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chjcomi 27711 | Commutative law for join in Cℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
| Theorem | chub1i 27712 | Cℋ join is an upper bound of two elements. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chub2i 27713 | Cℋ join is an upper bound of two elements. (Contributed by NM, 5-Nov-2000.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ 𝐴 ⊆ (𝐵 ∨ℋ 𝐴) | ||
| Theorem | chlubi 27714 | 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 27715 | Hilbert lattice join is the least upper bound of two elements (one direction of chlubi 27714). (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ⊆ 𝐶 ∧ 𝐵 ⊆ 𝐶) → (𝐴 ∨ℋ 𝐵) ⊆ 𝐶) | ||
| Theorem | chlej1i 27716 | 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 27717 | 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 27718 | 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 27719 | Hilbert lattice ordering in terms of join. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 ↔ (𝐴 ∨ℋ 𝐵) = 𝐵) | ||
| Theorem | chdmm1i 27720 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵)) | ||
| Theorem | chdmm2i 27721 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵)) | ||
| Theorem | chdmm3i 27722 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵) | ||
| Theorem | chdmm4i 27723 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵) | ||
| Theorem | chdmj1i 27724 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵)) | ||
| Theorem | chdmj2i 27725 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵)) | ||
| Theorem | chdmj3i 27726 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵) | ||
| Theorem | chdmj4i 27727 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵) | ||
| Theorem | chnlei 27728 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chjassi 27729 | 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 27730 | 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 27731 | The join of a closed subspace and its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ | ||
| Theorem | chj1i 27732 | Join with Hilbert lattice unit. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ ℋ) = ℋ | ||
| Theorem | chm0i 27733 | Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 0ℋ) = 0ℋ | ||
| Theorem | chm0 27734 | Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∩ 0ℋ) = 0ℋ) | ||
| Theorem | shjshsi 27735 | Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 +ℋ 𝐵))) | ||
| Theorem | shjshseli 27736 | 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 27737* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ)) | ||
| Theorem | chocin 27738 | 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 27739 | A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ⊆ (⊥‘𝐴) ↔ 𝐴 = 0ℋ)) | ||
| Theorem | chj0 27740 | Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 0ℋ) = 𝐴) | ||
| Theorem | chslej 27741 | 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 27742 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∩ 𝐵) ∈ Cℋ ) | ||
| Theorem | chsscon3 27743 | Hilbert lattice contraposition law. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
| Theorem | chsscon1 27744 | Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴)) | ||
| Theorem | chsscon2 27745 | Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
| Theorem | chpsscon3 27746 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊊ 𝐵 ↔ (⊥‘𝐵) ⊊ (⊥‘𝐴))) | ||
| Theorem | chpsscon1 27747 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((⊥‘𝐴) ⊊ 𝐵 ↔ (⊥‘𝐵) ⊊ 𝐴)) | ||
| Theorem | chpsscon2 27748 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊊ (⊥‘𝐵) ↔ 𝐵 ⊊ (⊥‘𝐴))) | ||
| Theorem | chjcom 27749 | Commutative law for Hilbert lattice join. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)) | ||
| Theorem | chub1 27750 | 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 27751 | 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 27752 | 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 27753 | Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chlej2 27754 | Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
| Theorem | chlejb1 27755 | Hilbert lattice ordering in terms of join. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∨ℋ 𝐵) = 𝐵)) | ||
| Theorem | chlejb2 27756 | Hilbert lattice ordering in terms of join. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐵 ∨ℋ 𝐴) = 𝐵)) | ||
| Theorem | chnle 27757 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | chjo 27758 | 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 27759 | 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 27760 | 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 27761 | 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 27762 | 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 27763 | Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 𝐴) = 𝐴) | ||
| Theorem | chjidmi 27764 | Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 | ||
| Theorem | chj12i 27765 | A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶)) | ||
| Theorem | chj4i 27766 | 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 27767 | Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chdmm1 27768 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) | ||
| Theorem | chdmm2 27769 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵))) | ||
| Theorem | chdmm3 27770 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵)) | ||
| Theorem | chdmm4 27771 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chdmj1 27772 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵))) | ||
| Theorem | chdmj2 27773 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵))) | ||
| Theorem | chdmj3 27774 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵)) | ||
| Theorem | chdmj4 27775 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵)) | ||
| Theorem | chjass 27776 | 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 | chj12 27777 | A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶))) | ||
| Theorem | chj4 27778 | Rearrangement of the join of 4 Hilbert lattice elements. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) ∧ (𝐶 ∈ Cℋ ∧ 𝐷 ∈ Cℋ )) → ((𝐴 ∨ℋ 𝐵) ∨ℋ (𝐶 ∨ℋ 𝐷)) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐷))) | ||
| Theorem | ledii 27779 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | lediri 27780 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐶) ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ 𝐶) | ||
| Theorem | lejdii 27781 | An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ (𝐴 ∨ℋ 𝐶)) | ||
| Theorem | lejdiri 27782 | An ortholattice is distributive in one ordering direction (join version). (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ∨ℋ 𝐶) ⊆ ((𝐴 ∨ℋ 𝐶) ∩ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | ledi 27783 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) | ||
| Theorem | spansn0 27784 | The span of the singleton of the zero vector is the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
| ⊢ (span‘{0ℎ}) = 0ℋ | ||
| Theorem | span0 27785 | The span of the empty set is the zero subspace. Remark 11.6.e of [Schechter] p. 276. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ (span‘∅) = 0ℋ | ||
| Theorem | elspani 27786* | Membership in the span of a subset of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ V ⇒ ⊢ (𝐴 ⊆ ℋ → (𝐵 ∈ (span‘𝐴) ↔ ∀𝑥 ∈ Sℋ (𝐴 ⊆ 𝑥 → 𝐵 ∈ 𝑥))) | ||
| Theorem | spanuni 27787 | The span of a union is the subspace sum of spans. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (span‘(𝐴 ∪ 𝐵)) = ((span‘𝐴) +ℋ (span‘𝐵)) | ||
| Theorem | spanun 27788 | The span of a union is the subspace sum of spans. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (span‘(𝐴 ∪ 𝐵)) = ((span‘𝐴) +ℋ (span‘𝐵))) | ||
| Theorem | sshhococi 27789 | The join of two Hilbert space subsets (not necessarily closed subspaces) equals the join of their closures (double orthocomplements). (Contributed by NM, 1-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = ((⊥‘(⊥‘𝐴)) ∨ℋ (⊥‘(⊥‘𝐵))) | ||
| Theorem | hne0 27790 | Hilbert space has a nonzero vector iff it is not trivial. (Contributed by NM, 24-Feb-2006.) (New usage is discouraged.) |
| ⊢ ( ℋ ≠ 0ℋ ↔ ∃𝑥 ∈ ℋ 𝑥 ≠ 0ℎ) | ||
| Theorem | chsup0 27791 | The supremum of the empty set. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
| ⊢ ( ∨ℋ ‘∅) = 0ℋ | ||
| Theorem | h1deoi 27792 | Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘{𝐵}) ↔ (𝐴 ∈ ℋ ∧ (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | h1dei 27793* | Membership in 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ ℋ ((𝐵 ·ih 𝑥) = 0 → (𝐴 ·ih 𝑥) = 0))) | ||
| Theorem | h1did 27794 | A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (⊥‘(⊥‘{𝐴}))) | ||
| Theorem | h1dn0 27795 | A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ≠ 0ℋ) | ||
| Theorem | h1de2i 27796 | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 17-Jul-2001.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) → ((𝐵 ·ih 𝐵) ·ℎ 𝐴) = ((𝐴 ·ih 𝐵) ·ℎ 𝐵)) | ||
| Theorem | h1de2bi 27797 | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐵 ≠ 0ℎ → (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ 𝐴 = (((𝐴 ·ih 𝐵) / (𝐵 ·ih 𝐵)) ·ℎ 𝐵))) | ||
| Theorem | h1de2ctlem 27798* | Lemma for h1de2ci 27799. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵)) | ||
| Theorem | h1de2ci 27799* | Membership in 1-dimensional subspace. All members are collinear with the generating vector. (Contributed by NM, 21-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵)) | ||
| Theorem | spansni 27800 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (span‘{𝐴}) = (⊥‘(⊥‘{𝐴})) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |