HomeTheorem List (p. 311 of 480)
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. 311 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: | Metamath Proof Explorer
(1-30438) |
Hilbert Space Explorer
(30439-31961) |
Users' Mathboxes
(31962-47939) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | chdmj1i 31001 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵)) | ||
| Theorem | chdmj2i 31002 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵)) | ||
| Theorem | chdmj3i 31003 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵) | ||
| Theorem | chdmj4i 31004 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵) | ||
| Theorem | chnlei 31005 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chjassi 31006 | 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 31007 | 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 31008 | The join of a closed subspace and its orthocomplement. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (⊥‘𝐴)) = ℋ | ||
| Theorem | chj1i 31009 | Join with Hilbert lattice one. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ ℋ) = ℋ | ||
| Theorem | chm0i 31010 | Meet with Hilbert lattice zero. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∩ 0ℋ) = 0ℋ | ||
| Theorem | chm0 31011 | Meet with Hilbert lattice zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∩ 0ℋ) = 0ℋ) | ||
| Theorem | shjshsi 31012 | Hilbert lattice join equals the double orthocomplement of subspace sum. (Contributed by NM, 27-Nov-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 +ℋ 𝐵))) | ||
| Theorem | shjshseli 31013 | 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 31014* | A nonzero closed subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ≠ 0ℋ ↔ ∃𝑥 ∈ 𝐴 𝑥 ≠ 0ℎ)) | ||
| Theorem | chocin 31015 | 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 31016 | A closed subspace less than its orthocomplement is zero. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ⊆ (⊥‘𝐴) ↔ 𝐴 = 0ℋ)) | ||
| Theorem | chj0 31017 | Join with Hilbert lattice zero. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 0ℋ) = 𝐴) | ||
| Theorem | chslej 31018 | 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 31019 | Closure of Hilbert lattice intersection. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∩ 𝐵) ∈ Cℋ ) | ||
| Theorem | chsscon3 31020 | Hilbert lattice contraposition law. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
| Theorem | chsscon1 31021 | Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((⊥‘𝐴) ⊆ 𝐵 ↔ (⊥‘𝐵) ⊆ 𝐴)) | ||
| Theorem | chsscon2 31022 | Hilbert lattice contraposition law. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
| Theorem | chpsscon3 31023 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊊ 𝐵 ↔ (⊥‘𝐵) ⊊ (⊥‘𝐴))) | ||
| Theorem | chpsscon1 31024 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → ((⊥‘𝐴) ⊊ 𝐵 ↔ (⊥‘𝐵) ⊊ 𝐴)) | ||
| Theorem | chpsscon2 31025 | Hilbert lattice contraposition law for strict ordering. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊊ (⊥‘𝐵) ↔ 𝐵 ⊊ (⊥‘𝐴))) | ||
| Theorem | chjcom 31026 | Commutative law for Hilbert lattice join. (Contributed by NM, 12-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)) | ||
| Theorem | chub1 31027 | 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 31028 | 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 31029 | 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 31030 | Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chlej2 31031 | Add join to both sides of Hilbert lattice ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
| Theorem | chlejb1 31032 | Hilbert lattice ordering in terms of join. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐴 ∨ℋ 𝐵) = 𝐵)) | ||
| Theorem | chlejb2 31033 | Hilbert lattice ordering in terms of join. (Contributed by NM, 2-Jul-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ⊆ 𝐵 ↔ (𝐵 ∨ℋ 𝐴) = 𝐵)) | ||
| Theorem | chnle 31034 | Equivalent expressions for "not less than" in the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (¬ 𝐵 ⊆ 𝐴 ↔ 𝐴 ⊊ (𝐴 ∨ℋ 𝐵))) | ||
| Theorem | chjo 31035 | 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 31036 | 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 31037 | 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 31038 | 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 31039 | 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 31040 | Idempotent law for Hilbert lattice join. (Contributed by NM, 26-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Cℋ → (𝐴 ∨ℋ 𝐴) = 𝐴) | ||
| Theorem | chjidmi 31041 | Idempotent law for Hilbert lattice join. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐴) = 𝐴 | ||
| Theorem | chj12i 31042 | A rearrangement of Hilbert lattice join. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶)) | ||
| Theorem | chj4i 31043 | 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 31044 | Hilbert lattice join distributes over itself. (Contributed by NM, 29-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∨ℋ 𝐵) ∨ℋ 𝐶) = ((𝐴 ∨ℋ 𝐶) ∨ℋ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | chdmm1 31045 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ 𝐵)) = ((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) | ||
| Theorem | chdmm2 31046 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ 𝐵)) = (𝐴 ∨ℋ (⊥‘𝐵))) | ||
| Theorem | chdmm3 31047 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∩ (⊥‘𝐵))) = ((⊥‘𝐴) ∨ℋ 𝐵)) | ||
| Theorem | chdmm4 31048 | De Morgan's law for meet in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∩ (⊥‘𝐵))) = (𝐴 ∨ℋ 𝐵)) | ||
| Theorem | chdmj1 31049 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ 𝐵)) = ((⊥‘𝐴) ∩ (⊥‘𝐵))) | ||
| Theorem | chdmj2 31050 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ 𝐵)) = (𝐴 ∩ (⊥‘𝐵))) | ||
| Theorem | chdmj3 31051 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘(𝐴 ∨ℋ (⊥‘𝐵))) = ((⊥‘𝐴) ∩ 𝐵)) | ||
| Theorem | chdmj4 31052 | De Morgan's law for join in a Hilbert lattice. (Contributed by NM, 21-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (⊥‘((⊥‘𝐴) ∨ℋ (⊥‘𝐵))) = (𝐴 ∩ 𝐵)) | ||
| Theorem | chjass 31053 | 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 31054 | A rearrangement of Hilbert lattice join. (Contributed by NM, 15-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → (𝐴 ∨ℋ (𝐵 ∨ℋ 𝐶)) = (𝐵 ∨ℋ (𝐴 ∨ℋ 𝐶))) | ||
| Theorem | chj4 31055 | 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 31056 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 6-Aug-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶)) | ||
| Theorem | lediri 31057 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 27-Apr-2006.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ & ⊢ 𝐶 ∈ Cℋ ⇒ ⊢ ((𝐴 ∩ 𝐶) ∨ℋ (𝐵 ∩ 𝐶)) ⊆ ((𝐴 ∨ℋ 𝐵) ∩ 𝐶) | ||
| Theorem | lejdii 31058 | 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 31059 | 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 31060 | An ortholattice is distributive in one ordering direction. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ∧ 𝐶 ∈ Cℋ ) → ((𝐴 ∩ 𝐵) ∨ℋ (𝐴 ∩ 𝐶)) ⊆ (𝐴 ∩ (𝐵 ∨ℋ 𝐶))) | ||
| Theorem | spansn0 31061 | 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 31062 | 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 31063* | 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 31064 | 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 31065 | 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 31066 | 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 31067 | 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 31068 | The supremum of the empty set. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
| ⊢ ( ∨ℋ ‘∅) = 0ℋ | ||
| Theorem | h1deoi 31069 | Membership in orthocomplement of 1-dimensional subspace. (Contributed by NM, 7-Jul-2001.) (New usage is discouraged.) |
| ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘{𝐵}) ↔ (𝐴 ∈ ℋ ∧ (𝐴 ·ih 𝐵) = 0)) | ||
| Theorem | h1dei 31070* | 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 31071 | A generating vector belongs to the 1-dimensional subspace it generates. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (⊥‘(⊥‘{𝐴}))) | ||
| Theorem | h1dn0 31072 | A nonzero vector generates a (nonzero) 1-dimensional subspace. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (⊥‘(⊥‘{𝐴})) ≠ 0ℋ) | ||
| Theorem | h1de2i 31073 | 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 31074 | 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 31075* | Lemma for h1de2ci 31076. (Contributed by NM, 19-Jul-2001.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (𝐴 ∈ (⊥‘(⊥‘{𝐵})) ↔ ∃𝑥 ∈ ℂ 𝐴 = (𝑥 ·ℎ 𝐵)) | ||
| Theorem | h1de2ci 31076* | 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 31077 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (span‘{𝐴}) = (⊥‘(⊥‘{𝐴})) | ||
| Theorem | elspansni 31078* | Membership in the span of a singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴)) | ||
| Theorem | spansn 31079 | The span of a singleton in Hilbert space equals its closure. (Contributed by NM, 4-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) = (⊥‘(⊥‘{𝐴}))) | ||
| Theorem | spansnch 31080 | The span of a Hilbert space singleton belongs to the Hilbert lattice. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Cℋ ) | ||
| Theorem | spansnsh 31081 | The span of a Hilbert space singleton is a subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (span‘{𝐴}) ∈ Sℋ ) | ||
| Theorem | spansnchi 31082 | The span of a singleton in Hilbert space is a closed subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ ℋ ⇒ ⊢ (span‘{𝐴}) ∈ Cℋ | ||
| Theorem | spansnid 31083 | A vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → 𝐴 ∈ (span‘{𝐴})) | ||
| Theorem | spansnmul 31084 | A scalar product with a vector belongs to the span of its singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ) → (𝐵 ·ℎ 𝐴) ∈ (span‘{𝐴})) | ||
| Theorem | elspansncl 31085 | A member of a span of a singleton is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ (span‘{𝐴})) → 𝐵 ∈ ℋ) | ||
| Theorem | elspansn 31086* | Membership in the span of a singleton. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → (𝐵 ∈ (span‘{𝐴}) ↔ ∃𝑥 ∈ ℂ 𝐵 = (𝑥 ·ℎ 𝐴))) | ||
| Theorem | elspansn2 31087 | Membership in the span of a singleton. All members are collinear with the generating vector. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) ↔ 𝐴 = (((𝐴 ·ih 𝐵) / (𝐵 ·ih 𝐵)) ·ℎ 𝐵))) | ||
| Theorem | spansncol 31088 | The singletons of collinear vectors have the same span. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℂ ∧ 𝐵 ≠ 0) → (span‘{(𝐵 ·ℎ 𝐴)}) = (span‘{𝐴})) | ||
| Theorem | spansneleqi 31089 | Membership relation implied by equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ ℋ → ((span‘{𝐴}) = (span‘{𝐵}) → 𝐴 ∈ (span‘{𝐵}))) | ||
| Theorem | spansneleq 31090 | Membership relation that implies equality of spans. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → (𝐴 ∈ (span‘{𝐵}) → (span‘{𝐴}) = (span‘{𝐵}))) | ||
| Theorem | spansnss 31091 | The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 5-Jun-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴) → (span‘{𝐵}) ⊆ 𝐴) | ||
| Theorem | elspansn3 31092 | A member of the span of the singleton of a vector is a member of a subspace containing the vector. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ 𝐴 ∧ 𝐶 ∈ (span‘{𝐵})) → 𝐶 ∈ 𝐴) | ||
| Theorem | elspansn4 31093 | A span membership condition implying two vectors belong to the same subspace. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
| ⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ) ∧ (𝐶 ∈ (span‘{𝐵}) ∧ 𝐶 ≠ 0ℎ)) → (𝐵 ∈ 𝐴 ↔ 𝐶 ∈ 𝐴)) | ||
| Theorem | elspansn5 31094 | A vector belonging to both a subspace and the span of the singleton of a vector not in it must be zero. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
| ⊢ (𝐴 ∈ Sℋ → (((𝐵 ∈ ℋ ∧ ¬ 𝐵 ∈ 𝐴) ∧ (𝐶 ∈ (span‘{𝐵}) ∧ 𝐶 ∈ 𝐴)) → 𝐶 = 0ℎ)) | ||
| Theorem | spansnss2 31095 | The span of the singleton of an element of a subspace is included in the subspace. (Contributed by NM, 16-Dec-2004.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ ℋ) → (𝐵 ∈ 𝐴 ↔ (span‘{𝐵}) ⊆ 𝐴)) | ||
| Theorem | normcan 31096 | Cancellation-type law that "extracts" a vector 𝐴 from its inner product with a proportional vector 𝐵. (Contributed by NM, 18-Mar-2006.) (New usage is discouraged.) |
| ⊢ ((𝐵 ∈ ℋ ∧ 𝐵 ≠ 0ℎ ∧ 𝐴 ∈ (span‘{𝐵})) → (((𝐴 ·ih 𝐵) / ((normℎ‘𝐵)↑2)) ·ℎ 𝐵) = 𝐴) | ||
| Theorem | pjspansn 31097 | A projection on the span of a singleton. (The proof ws shortened by Mario Carneiro, 15-Dec-2013.) (Contributed by NM, 28-May-2006.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ ∧ 𝐴 ≠ 0ℎ) → ((projℎ‘(span‘{𝐴}))‘𝐵) = (((𝐵 ·ih 𝐴) / ((normℎ‘𝐴)↑2)) ·ℎ 𝐴)) | ||
| Theorem | spansnpji 31098 | A subset of Hilbert space is orthogonal to the span of the singleton of a projection onto its orthocomplement. (Contributed by NM, 4-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
| ⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ 𝐴 ⊆ (⊥‘(span‘{((projℎ‘(⊥‘𝐴))‘𝐵)})) | ||
| Theorem | spanunsni 31099 | The span of the union of a closed subspace with a singleton equals the span of its union with an orthogonal singleton. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
| ⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ ℋ ⇒ ⊢ (span‘(𝐴 ∪ {𝐵})) = (span‘(𝐴 ∪ {((projℎ‘(⊥‘𝐴))‘𝐵)})) | ||
| Theorem | spanpr 31100 | The span of a pair of vectors. (Contributed by NM, 9-Jun-2006.) (New usage is discouraged.) |
| ⊢ ((𝐴 ∈ ℋ ∧ 𝐵 ∈ ℋ) → (span‘{(𝐴 +ℎ 𝐵)}) ⊆ (span‘{𝐴, 𝐵})) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |