![]() |
Metamath
Proof Explorer Theorem List (p. 314 of 491) | < 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: | ![]() (1-30946) |
![]() (30947-32469) |
![]() (32470-49035) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hhssvsf 31301 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ ( −ℎ ↾ (𝐻 × 𝐻)):(𝐻 × 𝐻)⟶𝐻 | ||
Theorem | hhssims 31302 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Sℋ & ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) ⇒ ⊢ 𝐷 = (IndMet‘𝑊) | ||
Theorem | hhssims2 31303 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 = ((normℎ ∘ −ℎ ) ↾ (𝐻 × 𝐻)) | ||
Theorem | hhssmet 31304 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐷 = (IndMet‘𝑊) & ⊢ 𝐻 ∈ Sℋ ⇒ ⊢ 𝐷 ∈ (Met‘𝐻) | ||
Theorem | hhssmetdval 31305 | 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 31306 | 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 | hhssbnOLD 31307 | Obsolete version of cssbn 25422: Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝑊 = 〈〈( +ℎ ↾ (𝐻 × 𝐻)), ( ·ℎ ↾ (ℂ × 𝐻))〉, (normℎ ↾ 𝐻)〉 & ⊢ 𝐻 ∈ Cℋ ⇒ ⊢ 𝑊 ∈ CBan | ||
Theorem | ocval 31308* | 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 31309* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐻 ⊆ ℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
Theorem | shocel 31310* | Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → (𝐴 ∈ (⊥‘𝐻) ↔ (𝐴 ∈ ℋ ∧ ∀𝑥 ∈ 𝐻 (𝐴 ·ih 𝑥) = 0))) | ||
Theorem | ocsh 31311 | 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 31312 | 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 31313 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → (⊥‘𝐴) ⊆ ℋ) | ||
Theorem | shocss 31314 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (⊥‘𝐴) ⊆ ℋ) | ||
Theorem | occon 31315 | Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘𝐵) ⊆ (⊥‘𝐴))) | ||
Theorem | occon2 31316 | Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵)))) | ||
Theorem | occon2i 31317 | Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐴 ⊆ ℋ & ⊢ 𝐵 ⊆ ℋ ⇒ ⊢ (𝐴 ⊆ 𝐵 → (⊥‘(⊥‘𝐴)) ⊆ (⊥‘(⊥‘𝐵))) | ||
Theorem | oc0 31318 | 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 31319 | Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ (𝐻 ⊆ ℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
Theorem | shocorth 31320 | Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → ((𝐴 ∈ 𝐻 ∧ 𝐵 ∈ (⊥‘𝐻)) → (𝐴 ·ih 𝐵) = 0)) | ||
Theorem | ococss 31321 | 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 31322 | 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 31323 | Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐻 ∈ Sℋ → (𝐺 ⊆ (⊥‘𝐻) → ((𝐴 ∈ 𝐺 ∧ 𝐵 ∈ 𝐻) → (𝐴 ·ih 𝐵) = 0))) | ||
Theorem | ocin 31324 | 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 31325 | Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ⊆ (⊥‘𝐵) ↔ 𝐵 ⊆ (⊥‘𝐴))) | ||
Theorem | ocnel 31326 | 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 31327* | 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 31328 | 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 31329 | 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 31330* | 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 31331 | Lemma for occl 31332. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
⊢ (𝜑 → 𝐴 ⊆ ℋ) & ⊢ (𝜑 → 𝐹 ∈ Cauchy) & ⊢ (𝜑 → 𝐹:ℕ⟶(⊥‘𝐴)) & ⊢ (𝜑 → 𝐵 ∈ 𝐴) ⇒ ⊢ (𝜑 → (( ⇝𝑣 ‘𝐹) ·ih 𝐵) = 0) | ||
Theorem | occl 31332 | 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 31333 | 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 31334 | 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 31335 | Closure of Cℋ orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ ⇒ ⊢ (⊥‘𝐴) ∈ Cℋ | ||
Definition | df-shs 31336* | Define subspace sum in Sℋ. See shsval 31340, shsval2i 31415, and shsval3i 31416 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
⊢ +ℋ = (𝑥 ∈ Sℋ , 𝑦 ∈ Sℋ ↦ ( +ℎ “ (𝑥 × 𝑦))) | ||
Definition | df-span 31337* | Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 31361 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ span = (𝑥 ∈ 𝒫 ℋ ↦ ∩ {𝑦 ∈ Sℋ ∣ 𝑥 ⊆ 𝑦}) | ||
Definition | df-chj 31338* | Define Hilbert lattice join. See chjval 31380 for its value and chjcl 31385 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 31383. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
⊢ ∨ℋ = (𝑥 ∈ 𝒫 ℋ, 𝑦 ∈ 𝒫 ℋ ↦ (⊥‘(⊥‘(𝑥 ∪ 𝑦)))) | ||
Definition | df-chsup 31339 | Define the supremum of a set of Hilbert lattice elements. See chsupval2 31438 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 31367. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.) |
⊢ ∨ℋ = (𝑥 ∈ 𝒫 𝒫 ℋ ↦ (⊥‘(⊥‘∪ 𝑥))) | ||
Theorem | shsval 31340 | 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 31341 | The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ⊆ ℋ) | ||
Theorem | shsel 31342* | 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 31343* | 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 31344* | Membership in subspace sum. (Contributed by NM, 4-May-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐶 ∈ (𝐴 +ℋ 𝐵) ↔ ∃𝑥 ∈ 𝐴 ∃𝑦 ∈ 𝐵 𝐶 = (𝑥 +ℎ 𝑦)) | ||
Theorem | shscli 31345 | 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 31346 | Closure of subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) ∈ Sℋ ) | ||
Theorem | shscom 31347 | Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴)) | ||
Theorem | shsva 31348 | Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))) | ||
Theorem | shsel1 31349 | 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 31350 | 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 31351 | Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵))) | ||
Theorem | shsub1 31352 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐴 +ℋ 𝐵)) | ||
Theorem | shsub2 31353 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → 𝐴 ⊆ (𝐵 +ℋ 𝐴)) | ||
Theorem | choc0 31354 | The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
⊢ (⊥‘0ℋ) = ℋ | ||
Theorem | choc1 31355 | 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 31356 | Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.) |
⊢ (⊥‘∅) = ℋ | ||
Theorem | shintcli 31357 | Closure of intersection of a nonempty subset of Sℋ. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Sℋ ∧ 𝐴 ≠ ∅) ⇒ ⊢ ∩ 𝐴 ∈ Sℋ | ||
Theorem | shintcl 31358 | 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 31359 | 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 31360 | 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 31361* | 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 31362 | Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 31437. (Contributed by NM, 9-Dec-2003.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ 𝒫 ℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴))) | ||
Theorem | chsupval 31363 | The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 31438. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ Cℋ → ( ∨ℋ ‘𝐴) = (⊥‘(⊥‘∪ 𝐴))) | ||
Theorem | spancl 31364 | 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 31365 | A member of a span is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ∈ (span‘𝐴)) → 𝐵 ∈ ℋ) | ||
Theorem | shsupcl 31366 | 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 31367 | 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 31368 | 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 31369 | 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 31370 | Subset relation for supremum of subset of Cℋ. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ Cℋ ∧ 𝐵 ⊆ Cℋ ) → (𝐴 ⊆ 𝐵 → ( ∨ℋ ‘𝐴) ⊆ ( ∨ℋ ‘𝐵))) | ||
Theorem | hsupunss 31371 | 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 31372 | 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 31373 | A subset of Hilbert space is included in its span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ⊆ ℋ → 𝐴 ⊆ (span‘𝐴)) | ||
Theorem | shsupunss 31374 | 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 31375 | A subspace of Hilbert space is its own span. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ (𝐴 ∈ Sℋ → (span‘𝐴) = 𝐴) | ||
Theorem | spanss 31376 | Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐵 ⊆ ℋ ∧ 𝐴 ⊆ 𝐵) → (span‘𝐴) ⊆ (span‘𝐵)) | ||
Theorem | spanssoc 31377 | 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 31378 | 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 31379 | Value of join in Sℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))) | ||
Theorem | chjval 31380 | Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵)))) | ||
Theorem | chjvali 31381 | Value of join in Cℋ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Cℋ & ⊢ 𝐵 ∈ Cℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (⊥‘(⊥‘(𝐴 ∪ 𝐵))) | ||
Theorem | sshjval3 31382 | 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 31383 | Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
⊢ ((𝐴 ⊆ ℋ ∧ 𝐵 ⊆ ℋ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ ) | ||
Theorem | shjcl 31384 | Closure of join in Sℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ ) | ||
Theorem | chjcl 31385 | Closure of join in Cℋ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Cℋ ∧ 𝐵 ∈ Cℋ ) → (𝐴 ∨ℋ 𝐵) ∈ Cℋ ) | ||
Theorem | shjcom 31386 | Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ ((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ) → (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴)) | ||
Theorem | shless 31387 | Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 +ℋ 𝐶) ⊆ (𝐵 +ℋ 𝐶)) | ||
Theorem | shlej1 31388 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐴 ∨ℋ 𝐶) ⊆ (𝐵 ∨ℋ 𝐶)) | ||
Theorem | shlej2 31389 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
⊢ (((𝐴 ∈ Sℋ ∧ 𝐵 ∈ Sℋ ∧ 𝐶 ∈ Sℋ ) ∧ 𝐴 ⊆ 𝐵) → (𝐶 ∨ℋ 𝐴) ⊆ (𝐶 ∨ℋ 𝐵)) | ||
Theorem | shincli 31390 | Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∩ 𝐵) ∈ Sℋ | ||
Theorem | shscomi 31391 | Commutative law for subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) = (𝐵 +ℋ 𝐴) | ||
Theorem | shsvai 31392 | Vector sum belongs to subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 +ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)) | ||
Theorem | shsel1i 31393 | A subspace sum contains a member of one of its subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐶 ∈ 𝐴 → 𝐶 ∈ (𝐴 +ℋ 𝐵)) | ||
Theorem | shsel2i 31394 | A subspace sum contains a member of one of its subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐶 ∈ 𝐵 → 𝐶 ∈ (𝐴 +ℋ 𝐵)) | ||
Theorem | shsvsi 31395 | Vector subtraction belongs to subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ ((𝐶 ∈ 𝐴 ∧ 𝐷 ∈ 𝐵) → (𝐶 −ℎ 𝐷) ∈ (𝐴 +ℋ 𝐵)) | ||
Theorem | shunssi 31396 | Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 +ℋ 𝐵) | ||
Theorem | shunssji 31397 | Union is smaller than Hilbert lattice join. (Contributed by NM, 11-Jun-2004.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∪ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | shsleji 31398 | Subspace sum is smaller than Hilbert lattice join. Remark in [Kalmbach] p. 65. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 +ℋ 𝐵) ⊆ (𝐴 ∨ℋ 𝐵) | ||
Theorem | shjcomi 31399 | Commutative law for join in Sℋ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ (𝐴 ∨ℋ 𝐵) = (𝐵 ∨ℋ 𝐴) | ||
Theorem | shsub1i 31400 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
⊢ 𝐴 ∈ Sℋ & ⊢ 𝐵 ∈ Sℋ ⇒ ⊢ 𝐴 ⊆ (𝐴 +ℋ 𝐵) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |