Home | Metamath
Proof Explorer Theorem List (p. 282 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ifchhv 28101 | Prove (common case). (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
Theorem | helsh 28102 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Theorem | shsspwh 28103 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
Theorem | chsspwh 28104 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
Theorem | hsn0elch 28105 | The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
Theorem | norm1 28106 | From any nonzero Hilbert space vector, construct a vector whose norm is 1. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
Theorem | norm1exi 28107* | A normalized vector exists in a subspace iff the subspace has a nonzero vector. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
Theorem | norm1hex 28108 | A normalized vector can exist only iff the Hilbert space has a nonzero vector. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.) |
Definition | df-oc 28109* | Define orthogonal complement of a subset (usually a subspace) of Hilbert space. The orthogonal complement is the set of all vectors orthogonal to all vectors in the subset. See ocval 28139 and chocvali 28158 for its value. Textbooks usually denote this unary operation with the symbol as a small superscript, although Mittelstaedt uses the symbol as a prefix operation. Here we define a function (prefix operation) rather than introducing a new syntactic form. This lets us take advantage of the theorems about functions that we already have proved under set theory. Definition of [Mittelstaedt] p. 9. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
Definition | df-ch0 28110 | Define the zero for closed subspaces of Hilbert space. See h0elch 28112 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
Theorem | elch0 28111 | Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.) |
Theorem | h0elch 28112 | The zero subspace is a closed subspace. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
Theorem | h0elsh 28113 | The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Theorem | hhssva 28114 | The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
Theorem | hhsssm 28115 | The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssnm 28116 | The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
CV | ||
Theorem | issubgoilem 28117* | Lemma for hhssabloilem 28118. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
Theorem | hhssabloilem 28118 | Lemma for hhssabloi 28119. Formerly part of proof for hhssabloi 28119 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.) |
Theorem | hhssabloi 28119 | 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.) |
Theorem | hhssablo 28120 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssnv 28121 | Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.) |
Theorem | hhssnvt 28122 | Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
Theorem | hhsst 28123 | A member of is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
Theorem | hhshsslem1 28124 | Lemma for hhsssh 28126. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhshsslem2 28125 | Lemma for hhsssh 28126. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
Theorem | hhsssh 28126 | The predicate " is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.) |
Theorem | hhsssh2 28127 | The predicate " is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssba 28128 | The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssvs 28129 | The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssvsf 28130 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssph 28131 | Inner product space property of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssims 28132 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssims2 28133 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssmet 28134 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhssmetdval 28135 | Value of the distance function of the metric space of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhsscms 28136 | 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.) |
Theorem | hhssbn 28137 | Banach space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | hhsshl 28138 | Hilbert space property of a closed subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
Theorem | ocval 28139* | 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.) |
Theorem | ocel 28140* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
Theorem | shocel 28141* | Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.) |
Theorem | ocsh 28142 | 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.) |
Theorem | shocsh 28143 | 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.) |
Theorem | ocss 28144 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
Theorem | shocss 28145 | An orthogonal complement is a subset of Hilbert space. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
Theorem | occon 28146 | Contraposition law for orthogonal complement. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
Theorem | occon2 28147 | Double contraposition for orthogonal complement. (Contributed by NM, 22-Jul-2001.) (New usage is discouraged.) |
Theorem | occon2i 28148 | Double contraposition for orthogonal complement. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
Theorem | oc0 28149 | The zero vector belongs to an orthogonal complement of a Hilbert subspace. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
Theorem | ocorth 28150 | Members of a subset and its complement are orthogonal. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
Theorem | shocorth 28151 | Members of a subspace and its complement are orthogonal. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
Theorem | ococss 28152 | 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 28153 | Inclusion in complement of complement. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 10-Oct-1999.) (New usage is discouraged.) |
Theorem | shorth 28154 | Members of orthogonal subspaces are orthogonal. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
Theorem | ocin 28155 | 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.) |
Theorem | occon3 28156 | Hilbert lattice contraposition law. (Contributed by Mario Carneiro, 18-May-2014.) (New usage is discouraged.) |
Theorem | ocnel 28157 | 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.) |
Theorem | chocvali 28158* | 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.) |
Theorem | shuni 28159 | 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.) |
Theorem | chocunii 28160 | 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.) |
Theorem | pjhthmo 28161* | 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.) |
Theorem | occllem 28162 | Lemma for occl 28163. (Contributed by NM, 7-Aug-2000.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
Theorem | occl 28163 | 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.) |
Theorem | shoccl 28164 | 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.) |
Theorem | choccl 28165 | 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.) |
Theorem | choccli 28166 | Closure of orthocomplement. (Contributed by NM, 29-Jul-1999.) (New usage is discouraged.) |
Definition | df-shs 28167* | Define subspace sum in . See shsval 28171, shsval2i 28246, and shsval3i 28247 for its value. (Contributed by NM, 16-Oct-1999.) (New usage is discouraged.) |
Definition | df-span 28168* | Define the linear span of a subset of Hilbert space. Definition of span in [Schechter] p. 276. See spanval 28192 for its value. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Definition | df-chj 28169* | Define Hilbert lattice join. See chjval 28211 for its value and chjcl 28216 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 ; see sshjcl 28214. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
Definition | df-chsup 28170 | Define the supremum of a set of Hilbert lattice elements. See chsupval2 28269 for its value. We actually define the supremum for an arbitrary collection of Hilbert space subsets, not just elements of the Hilbert lattice , to allow more general theorems. Even for general subsets the supremum still a Hilbert lattice element; see hsupcl 28198. (Contributed by NM, 9-Dec-2003.) (New usage is discouraged.) |
Theorem | shsval 28171 | 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.) |
Theorem | shsss 28172 | The subspace sum is a subset of Hilbert space. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | shsel 28173* | 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.) |
Theorem | shsel3 28174* | Membership in the subspace sum of two Hilbert subspaces, using vector subtraction. (Contributed by NM, 20-Jan-2007.) (New usage is discouraged.) |
Theorem | shseli 28175* | Membership in subspace sum. (Contributed by NM, 4-May-2000.) (New usage is discouraged.) |
Theorem | shscli 28176 | Closure of subspace sum. (Contributed by NM, 15-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | shscl 28177 | Closure of subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | shscom 28178 | Commutative law for subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | shsva 28179 | Vector sum belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | shsel1 28180 | A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | shsel2 28181 | A subspace sum contains a member of one of its subspaces. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | shsvs 28182 | Vector subtraction belongs to subspace sum. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
Theorem | shsub1 28183 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
Theorem | shsub2 28184 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
Theorem | choc0 28185 | The orthocomplement of the zero subspace is the unit subspace. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
Theorem | choc1 28186 | 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.) |
Theorem | chocnul 28187 | Orthogonal complement of the empty set. (Contributed by NM, 31-Oct-2000.) (New usage is discouraged.) |
Theorem | shintcli 28188 | Closure of intersection of a nonempty subset of . (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
Theorem | shintcl 28189 | The intersection of a nonempty set of subspaces is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Theorem | chintcli 28190 | The intersection of a nonempty set of closed subspaces is a closed subspace. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
Theorem | chintcl 28191 | The intersection (infimum) of a nonempty subset of belongs to . 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.) |
Theorem | spanval 28192* | 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.) |
Theorem | hsupval 28193 | Value of supremum of set of subsets of Hilbert space. For an alternate version of the value, see hsupval2 28268. (Contributed by NM, 9-Dec-2003.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
Theorem | chsupval 28194 | The value of the supremum of a set of closed subspaces of Hilbert space. For an alternate version of the value, see chsupval2 28269. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
Theorem | spancl 28195 | The span of a subset of Hilbert space is a subspace. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
Theorem | elspancl 28196 | A member of a span is a vector. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
Theorem | shsupcl 28197 | Closure of the subspace supremum of set of subsets of Hilbert space. (Contributed by NM, 26-Nov-2004.) (New usage is discouraged.) |
Theorem | hsupcl 28198 | Closure of supremum of set of subsets of Hilbert space. Note that the supremum belongs to even if the subsets do not. (Contributed by NM, 10-Nov-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
Theorem | chsupcl 28199 | Closure of supremum of subset of . Definition of supremum in Proposition 1 of [Kalmbach] p. 65. Shows that 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.) |
Theorem | hsupss 28200 | 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.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |