Home | Metamath
Proof Explorer Theorem List (p. 276 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 | issubgoilem 27501* | Lemma for hhssabloilem 27502. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
⊢ ((𝑥 ∈ 𝑌 ∧ 𝑦 ∈ 𝑌) → (𝑥𝐻𝑦) = (𝑥𝐺𝑦)) ⇒ ⊢ ((𝐴 ∈ 𝑌 ∧ 𝐵 ∈ 𝑌) → (𝐴𝐻𝐵) = (𝐴𝐺𝐵)) | ||
Theorem | hhssabloilem 27502 | Lemma for hhssabloi 27503. Formerly part of proof for hhssabloi 27503 which was based on the deprecated definition "SubGrpOp" for subgroups. (Contributed by NM, 9-Apr-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (Revised by AV, 27-Aug-2021.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( +ℎ ∈ GrpOp ∧ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ GrpOp ∧ ( +ℎ ↾ (𝐻 × 𝐻)) ⊆ +ℎ ) | ||
Theorem | hhssabloi 27503 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (Revised by Mario Carneiro, 23-Dec-2013.) (Proof shortened by AV, 27-Aug-2021.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp | ||
Theorem | hhssablo 27504 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → ( +ℎ ↾ (𝐻 × 𝐻)) ∈ AbelOp) | ||
Theorem | hhssnv 27505 | Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝑊 ∈ NrmCVec | ||
Theorem | hhssnvt 27506 | Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ NrmCVec) | ||
Theorem | hhsst 27507 | A member of Sℋ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ → 𝑊 ∈ (SubSp‘𝑈)) | ||
Theorem | hhshsslem1 27508 | Lemma for hhsssh 27510. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
Theorem | hhshsslem2 27509 | Lemma for hhsssh 27510. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝑊 ∈ (SubSp‘𝑈) & ⊢ 𝐻 ⊆ ℋ ⇒ ⊢ 𝐻 ∈ Sℋ | ||
Theorem | hhsssh 27510 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.) |
⊢ 𝑈 = 〈〈 +ℎ , ·ℎ 〉, normℎ〉 & ⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ (SubSp‘𝑈) ∧ 𝐻 ⊆ ℋ)) | ||
Theorem | hhsssh2 27511 | The predicate "𝐻 is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 ⇒ ⊢ (𝐻 ∈ Sℋ ↔ (𝑊 ∈ NrmCVec ∧ 𝐻 ⊆ ℋ)) | ||
Theorem | hhssba 27512 | The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐻 = (BaseSet‘𝑊) | ||
Theorem | hhssvs 27513 | The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)) = ( −𝑣 ‘𝑊) | ||
Theorem | hhssvsf 27514 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 | ||
Theorem | hhssph 27515 | Inner product space property of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝑊 ∈ CPreHilOLD | ||
Theorem | hhssims 27516 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) ⇒ ⊢ 𝐷 = (IndMet‘𝑊) | ||
Theorem | hhssims2 27517 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) | ||
Theorem | hhssmet 27518 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 ∈ (Met‘𝐻) | ||
Theorem | hhssmetdval 27519 | Value of the distance function of the metric space of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ 𝐻) → (𝐴𝐷𝐵) = (normℎ‘(𝐴 −ℎ 𝐵))) | ||
Theorem | hhsscms 27520 | The induced metric of a closed subspace is complete. (Contributed by NM, 10-Apr-2008.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝐷 ∈ (CMet‘𝐻) | ||
Theorem | hhssbn 27521 | Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝑊 ∈ CBan | ||
Theorem | hhsshl 27522 | Hilbert space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝑊 ∈ CHilOLD | ||
Theorem | ocval 27523* | Value of orthogonal complement of a subset of Hilbert space. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ (𝐻 ⊆ ℋ → (⊥‘𝐻) = {𝑥 ∈ ℋ ∣ ∀𝑦 ∈ 𝐻 (𝑥 ·ih 𝑦) = 0}) | ||
Theorem | ocel 27524* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
Theorem | shocel 27525* | Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
Theorem | ocsh 27526 | The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ∈ Sℋ ) | ||
Theorem | shocsh 27527 | The orthogonal complement of a subspace is a subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ∈ Sℋ ) | ||
Theorem | ocss 27528 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ) | ||
Theorem | shocss 27529 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ) | ||
Theorem | occon 27530 | Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
Theorem | occon2 27531 | Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))) | ||
Theorem | occon2i 27532 | Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))) | ||
Theorem | oc0 27533 | The zero vector belongs to an orthogonal complement of a Hilbert subspace. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → 0ℎ ∈ (⊥‘𝐻)) | ||
Theorem | ocorth 27534 | Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
Theorem | shocorth 27535 | Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
Theorem | ococss 27536 | Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (⊥‘(⊥‘𝐴))) | ||
Theorem | shococss 27537 | Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → 𝐴 ⊆ (⊥‘(⊥‘𝐴))) | ||
Theorem | shorth 27538 | Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0))) | ||
Theorem | ocin 27539 | Intersection of a Hilbert subspace and its complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (𝐴 ∩ (⊥‘𝐴)) = 0ℋ) | ||
Theorem | occon3 27540 | Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
Theorem | ocnel 27541 | A nonzero vector in the complement of a subspace does not belong to the subspace. (Contributed by NM, 10-Apr-2006.) (New usage is discouraged.) |
⊢ ((𝐻 ∈ Sℋ ∧ 𝐴 ∈ (⊥‘𝐻) ∧ 𝐴 ≠ 0ℎ) → ¬ 𝐴 ∈ 𝐻) | ||
Theorem | chocvali 27542* | Value of the orthogonal complement of a Hilbert lattice element. The orthogonal complement of 𝐴 is the set of vectors that are orthogonal to all vectors in 𝐴. (Contributed by NM, 8-Aug-2004.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) = {𝑥 ∈ ℋ ∣ ∀𝑦 ∈ 𝐴 (𝑥 ·ih 𝑦) = 0} | ||
Theorem | shuni 27543 | Two subspaces with trivial intersection have a unique decomposition of the elements of the subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐻 ∈ Sℋ ) & ⊢ (𝜑 → 𝐾 ∈ Sℋ ) & ⊢ (𝜑 → (𝐻 ∩ 𝐾) = 0ℋ) & ⊢ (𝜑 → 𝐴 ∈ 𝐻) & ⊢ (𝜑 → 𝐵 ∈ 𝐾) & ⊢ (𝜑 → 𝐶 ∈ 𝐻) & ⊢ (𝜑 → 𝐷 ∈ 𝐾) & ⊢ (𝜑 → (𝐴 +ℎ 𝐵) = (𝐶 +ℎ 𝐷)) ⇒ ⊢ (𝜑 → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷)) | ||
Theorem | chocunii 27544 | Lemma for uniqueness part of Projection Theorem. Theorem 3.7(i) of [Beran] p. 102 (uniqueness part). (Contributed by NM, 23-Oct-1999.) (Proof shortened by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐻 ∈ Cℋ ⇒ ⊢ (((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) ∧ (𝐶 ∈ 𝐻 ∧ 𝐷 ∈ (⊥‘𝐻))) → ((𝑅 = (𝐴 +ℎ 𝐵) ∧ 𝑅 = (𝐶 +ℎ 𝐷)) → (𝐴 = 𝐶 ∧ 𝐵 = 𝐷))) | ||
Theorem | pjhthmo 27545* | Projection Theorem, uniqueness part. Any two disjoint subspaces yield a unique decomposition of vectors into each subspace. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ (𝐴 ∩ 𝐵) = 0ℋ) → ∃*𝑥(𝑥 ∈ 𝐴 ∧ ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))) | ||
Theorem | occllem 27546 | Lemma for occl 27547. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ⊆ ℋ) & ⊢ (𝜑 → 𝐹 ∈ Cauchy) & ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0) | ||
Theorem | occl 27547 | Closure of complement of Hilbert subset. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 8-Aug-2000.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ∈ Cℋ ) | ||
Theorem | shoccl 27548 | Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 13-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ∈ Cℋ ) | ||
Theorem | choccl 27549 | Closure of complement of Hilbert subspace. Part of Remark 3.12 of [Beran] p. 107. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Cℋ → (⊥‘𝐴) ∈ Cℋ ) | ||
Theorem | choccli 27550 | Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) ∈ Cℋ | ||
Definition | df-shs 27551* | Define subspace sum in Sℋ. See shsval 27555, shsval2i 27630, and shsval3i 27631 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) | ||
Definition | df-span 27552* | Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 27576 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦}) | ||
Definition | df-chj 27553* | Define Hilbert lattice join. See chjval 27595 for its value and chjcl 27600 for its closure law. Note that we define it over all Hilbert space subsets to allow proving more general theorems. Even for general subsets the join belongs to Cℋ; see sshjcl 27598. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) | ||
Definition | df-chsup 27554 | Define the supremum of a set of Hilbert lattice elements. See chsupval2 27653 for its value. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice Cℋ, to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupcl 27582. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.) |
⊢ ∨ℋ = (𝑥 ∈ 𝒫 𝒫 ℋ ↦ (⊥‘(⊥‘∪ 𝑥))) | ||
Theorem | shsval 27555 | Value of subspace sum of two Hilbert space subspaces. Definition of subspace sum in [Kalmbach] p. 65. (Contributed by NM, 16-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = ( +ℎ “ (𝐴 × 𝐵))) | ||
Theorem | shsss 27556 | The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ ℋ) | ||
Theorem | shsel 27557* | Membership in the subspace sum of two Hilbert subspaces. (Contributed by NM, 14-Dec-2004.) (Revised by Mario Carneiro, 29-Jan-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦))) | ||
Theorem | shsel3 27558* | Membership in the subspace sum of two Hilbert subspaces, using vector subtraction. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 −ℎ 𝑦))) | ||
Theorem | shseli 27559* | Membership in subspace sum. (Contributed by NM, 4-May-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
Theorem | shscli 27560 | Closure of subspace sum. (Contributed by NM, 15-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) ∈ Sℋ | ||
Theorem | shscl 27561 | Closure of subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ∈ Sℋ ) | ||
Theorem | shscom 27562 | Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) | ||
Theorem | shsva 27563 | Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))) | ||
Theorem | shsel1 27564 | A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ 𝐴 → 𝐶 ∈ (𝐴 +ℋ 𝐵))) | ||
Theorem | shsel2 27565 | A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐶 ∈ 𝐵 → 𝐶 ∈ (𝐴 +ℋ 𝐵))) | ||
Theorem | shsvs 27566 | Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))) | ||
Theorem | shsub1 27567 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 +ℋ 𝐵)) | ||
Theorem | shsub2 27568 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐵 +ℋ 𝐴)) | ||
Theorem | choc0 27569 | The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ (⊥‘0ℋ) = ℋ | ||
Theorem | choc1 27570 | The orthocomplement of the unit subspace is the zero subspace. Does not require Axiom of Choice. (Contributed by NM, 24-Oct-1999.) (New usage is discouraged.) |
⊢ (⊥‘ ℋ) = 0ℋ | ||
Theorem | chocnul 27571 | Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.) |
⊢ (⊥‘∅) = ℋ | ||
Theorem | shintcli 27572 | Closure of intersection of a nonempty subset of Sℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅) ⇒ ⊢ ∩ 𝐴 ∈ Sℋ | ||
Theorem | shintcl 27573 | The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Sℋ ) | ||
Theorem | chintcli 27574 | The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅) ⇒ ⊢ ∩ 𝐴 ∈ Cℋ | ||
Theorem | chintcl 27575 | The intersection (infimum) of a nonempty subset of Cℋ belongs to Cℋ. Part of Theorem 3.13 of [Beran] p. 108. Also part of Definition 3.4-1 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐴 ≠ ∅) → ∩ 𝐴 ∈ Cℋ ) | ||
Theorem | spanval 27576* | Value of the linear span of a subset of Hilbert space. The span is the intersection of all subspaces constraining the subset. Definition of span in [Schechter] p. 276. (Contributed by NM, 2-Jun-2004.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) = ∩ {𝑥 ∈ Sℋ ∣ 𝐴 ⊆ 𝑥}) | ||
Theorem | hsupval 27577 | Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 27652. (Contributed by NM, 9-Dec-2003.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴))) | ||
Theorem | chsupval 27578 | The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 27653. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴))) | ||
Theorem | spancl 27579 | The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) ∈ Sℋ ) | ||
Theorem | elspancl 27580 | A member of a span is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ∈ (span‘𝐴)) → 𝐵 ∈ ℋ) | ||
Theorem | shsupcl 27581 | Closure of the subspace supremum of set of subsets of Hilbert space. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 ℋ → (span‘∪ 𝐴) ∈ Sℋ ) | ||
Theorem | hsupcl 27582 | Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to Cℋ even if the subsets do not. (Contributed by NM, 10-Nov-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) ∈ Cℋ ) | ||
Theorem | chsupcl 27583 | Closure of supremum of subset of Cℋ. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that Cℋ is a complete lattice. Also part of Definition 3.4-1 in [MegPav2000] p. 2345 (PDF p. 8). (Contributed by NM, 10-Nov-1999.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) ∈ Cℋ ) | ||
Theorem | hsupss 27584 | Subset relation for supremum of Hilbert space subsets. (Contributed by NM, 24-Nov-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ 𝒫 ℋ ∧ 𝐵 ⊆ 𝒫 ℋ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵))) | ||
Theorem | chsupss 27585 | Subset relation for supremum of subset of Cℋ. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐵 ⊆ Cℋ ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵))) | ||
Theorem | hsupunss 27586 | The union of a set of Hilbert space subsets is smaller than its supremum. (Contributed by NM, 24-Nov-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 ℋ → ∪ 𝐴 ⊆ ( ∨ℋ ‘𝐴)) | ||
Theorem | chsupunss 27587 | The union of a set of closed subspaces is smaller than its supremum. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Cℋ → ∪ 𝐴 ⊆ ( ∨ℋ ‘𝐴)) | ||
Theorem | spanss2 27588 | A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (span‘𝐴)) | ||
Theorem | shsupunss 27589 | The union of a set of subspaces is smaller than its supremum. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Sℋ → ∪ 𝐴 ⊆ (span‘∪ 𝐴)) | ||
Theorem | spanid 27590 | A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (span‘𝐴) = 𝐴) | ||
Theorem | spanss 27591 | Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵) → (span‘𝐴) ⊆ (span‘𝐵)) | ||
Theorem | spanssoc 27592 | The span of a subset of Hilbert space is less than or equal to its closure (double orthogonal complement). (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (span‘𝐴) ⊆ (⊥‘(⊥‘𝐴))) | ||
Theorem | sshjval 27593 | Value of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))) | ||
Theorem | shjval 27594 | Value of join in Sℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))) | ||
Theorem | chjval 27595 | Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))) | ||
Theorem | chjvali 27596 | Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))) | ||
Theorem | sshjval3 27597 | Value of join for subsets of Hilbert space in terms of supremum: the join is the supremum of its two arguments. Based on the definition of join in [Beran] p. 3. For later convenience we prove a general version that works for any subset of Hilbert space, not just the elements of the lattice Cℋ. (Contributed by NM, 2-Mar-2004.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) = ( ∨ℋ ‘{𝐴, 𝐵})) | ||
Theorem | sshjcl 27598 | Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ ) | ||
Theorem | shjcl 27599 | Closure of join in Sℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ ) | ||
Theorem | chjcl 27600 | Closure of join in Cℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |