![]() |
Metamath
Proof Explorer Theorem List (p. 308 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: | ![]() (1-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hcau 30701* | Member of the set of Cauchy sequences on a Hilbert space. Definition for Cauchy sequence in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (πΉ β Cauchy β (πΉ:ββΆ β β§ βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ¦) ββ (πΉβπ§))) < π₯)) | ||
Theorem | hcauseq 30702 | A Cauchy sequences on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (πΉ β Cauchy β πΉ:ββΆ β) | ||
Theorem | hcaucvg 30703* | A Cauchy sequence on a Hilbert space converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ ((πΉ β Cauchy β§ π΄ β β+) β βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ¦) ββ (πΉβπ§))) < π΄) | ||
Theorem | seq1hcau 30704* | A sequence on a Hilbert space is a Cauchy sequence if it converges. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (πΉ:ββΆ β β (πΉ β Cauchy β βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ¦) ββ (πΉβπ§))) < π₯)) | ||
Theorem | hlimi 30705* | Express the predicate: The limit of vector sequence πΉ in a Hilbert space is π΄, i.e. πΉ converges to π΄. This means that for any real π₯, no matter how small, there always exists an integer π¦ such that the norm of any later vector in the sequence minus the limit is less than π₯. Definition of converge in [Beran] p. 96. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ π΄ β V β β’ (πΉ βπ£ π΄ β ((πΉ:ββΆ β β§ π΄ β β) β§ βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ§) ββ π΄)) < π₯)) | ||
Theorem | hlimseqi 30706 | A sequence with a limit on a Hilbert space is a sequence. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β V β β’ (πΉ βπ£ π΄ β πΉ:ββΆ β) | ||
Theorem | hlimveci 30707 | Closure of the limit of a sequence on Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ π΄ β V β β’ (πΉ βπ£ π΄ β π΄ β β) | ||
Theorem | hlimconvi 30708* | Convergence of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ π΄ β V β β’ ((πΉ βπ£ π΄ β§ π΅ β β+) β βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ§) ββ π΄)) < π΅) | ||
Theorem | hlim2 30709* | The limit of a sequence on a Hilbert space. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ ((πΉ:ββΆ β β§ π΄ β β) β (πΉ βπ£ π΄ β βπ₯ β β+ βπ¦ β β βπ§ β (β€β₯βπ¦)(normββ((πΉβπ§) ββ π΄)) < π₯)) | ||
Theorem | hlimadd 30710* | Limit of the sum of two sequences in a Hilbert vector space. (Contributed by Mario Carneiro, 19-May-2014.) (New usage is discouraged.) |
β’ (π β πΉ:ββΆ β) & β’ (π β πΊ:ββΆ β) & β’ (π β πΉ βπ£ π΄) & β’ (π β πΊ βπ£ π΅) & β’ π» = (π β β β¦ ((πΉβπ) +β (πΊβπ))) β β’ (π β π» βπ£ (π΄ +β π΅)) | ||
Theorem | hilmet 30711 | The Hilbert space norm determines a metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ π· β (Metβ β) | ||
Theorem | hilxmet 30712 | The Hilbert space norm determines a metric space. (Contributed by Mario Carneiro, 10-Sep-2015.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ π· β (βMetβ β) | ||
Theorem | hilmetdval 30713 | Value of the distance function of the metric space of Hilbert space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ ((π΄ β β β§ π΅ β β) β (π΄π·π΅) = (normββ(π΄ ββ π΅))) | ||
Theorem | hilims 30714 | Hilbert space distance metric. (Contributed by NM, 13-Sep-2007.) (New usage is discouraged.) |
β’ β = (BaseSetβπ) & β’ +β = ( +π£ βπ) & β’ Β·β = ( Β·π OLD βπ) & β’ Β·ih = (Β·πOLDβπ) & β’ π· = (IndMetβπ) & β’ π β NrmCVec β β’ π· = (normβ β ββ ) | ||
Theorem | hhcau 30715 | The Cauchy sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ Cauchy = ((Cauβπ·) β© ( β βm β)) | ||
Theorem | hhlm 30716 | The limit sequences of Hilbert space. (Contributed by NM, 19-Nov-2007.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) β β’ βπ£ = ((βπ‘βπ½) βΎ ( β βm β)) | ||
Theorem | hhcmpl 30717* | Lemma used for derivation of the completeness axiom ax-hcompl 30719 from ZFC Hilbert space theory. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ (πΉ β (Cauβπ·) β βπ₯ β β πΉ(βπ‘βπ½)π₯) β β’ (πΉ β Cauchy β βπ₯ β β πΉ βπ£ π₯) | ||
Theorem | hilcompl 30718* | Lemma used for derivation of the completeness axiom ax-hcompl 30719 from ZFC Hilbert space theory. The first five hypotheses would be satisfied by the definitions described in ax-hilex 30516; the 6th would be satisfied by eqid 2731; the 7th by a given fixed Hilbert space; and the last by Theorem hlcompl 30432. (Contributed by NM, 13-Sep-2007.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ β = (BaseSetβπ) & β’ +β = ( +π£ βπ) & β’ Β·β = ( Β·π OLD βπ) & β’ Β·ih = (Β·πOLDβπ) & β’ π· = (IndMetβπ) & β’ π½ = (MetOpenβπ·) & β’ π β CHilOLD & β’ (πΉ β (Cauβπ·) β βπ₯ β β πΉ(βπ‘βπ½)π₯) β β’ (πΉ β Cauchy β βπ₯ β β πΉ βπ£ π₯) | ||
Axiom | ax-hcompl 30719* | Completeness of a Hilbert space. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
β’ (πΉ β Cauchy β βπ₯ β β πΉ βπ£ π₯) | ||
Theorem | hhcms 30720 | The Hilbert space induced metric determines a complete metric space. (Contributed by NM, 10-Apr-2008.) (Proof shortened by Mario Carneiro, 14-May-2014.) (Proof shortened by Peter Mazsa, 2-Oct-2022.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π· = (IndMetβπ) β β’ π· β (CMetβ β) | ||
Theorem | hhhl 30721 | The Hilbert space structure is a complex Hilbert space. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© β β’ π β CHilOLD | ||
Theorem | hilcms 30722 | The Hilbert space norm determines a complete metric space. (Contributed by NM, 17-Apr-2007.) (New usage is discouraged.) |
β’ π· = (normβ β ββ ) β β’ π· β (CMetβ β) | ||
Theorem | hilhl 30723 | The Hilbert space of the Hilbert Space Explorer is a complex Hilbert space. (Contributed by Steve Rodriguez, 29-Apr-2007.) (New usage is discouraged.) |
β’ β¨β¨ +β , Β·β β©, normββ© β CHilOLD | ||
Definition | df-sh 30724 | Define the set of subspaces of a Hilbert space. See issh 30725 for its membership relation. Basically, a subspace is a subset of a Hilbert space that acts like a vector space. From Definition of [Beran] p. 95. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ Sβ = {β β π« β β£ (0β β β β§ ( +β β (β Γ β)) β β β§ ( Β·β β (β Γ β)) β β)} | ||
Theorem | issh 30725 | Subspace π» of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. (Contributed by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Sβ β ((π» β β β§ 0β β π») β§ (( +β β (π» Γ π»)) β π» β§ ( Β·β β (β Γ π»)) β π»))) | ||
Theorem | issh2 30726* | Subspace π» of a Hilbert space. A subspace is a subset of Hilbert space which contains the zero vector and is closed under vector addition and scalar multiplication. Definition of [Beran] p. 95. (Contributed by NM, 16-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Sβ β ((π» β β β§ 0β β π») β§ (βπ₯ β π» βπ¦ β π» (π₯ +β π¦) β π» β§ βπ₯ β β βπ¦ β π» (π₯ Β·β π¦) β π»))) | ||
Theorem | shss 30727 | A subspace is a subset of Hilbert space. (Contributed by NM, 9-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Sβ β π» β β) | ||
Theorem | shel 30728 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 14-Dec-2004.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β π») β π΄ β β) | ||
Theorem | shex 30729 | The set of subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ Sβ β V | ||
Theorem | shssii 30730 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Sβ β β’ π» β β | ||
Theorem | sheli 30731 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Sβ β β’ (π΄ β π» β π΄ β β) | ||
Theorem | shelii 30732 | A member of a subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Sβ & β’ π΄ β π» β β’ π΄ β β | ||
Theorem | sh0 30733 | The zero vector belongs to any subspace of a Hilbert space. (Contributed by NM, 11-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Sβ β 0β β π») | ||
Theorem | shaddcl 30734 | Closure of vector addition in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β π» β§ π΅ β π») β (π΄ +β π΅) β π») | ||
Theorem | shmulcl 30735 | Closure of vector scalar multiplication in a subspace of a Hilbert space. (Contributed by NM, 13-Sep-1999.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β β β§ π΅ β π») β (π΄ Β·β π΅) β π») | ||
Theorem | issh3 30736* | Subspace π» of a Hilbert space. (Contributed by NM, 16-Aug-1999.) (New usage is discouraged.) |
β’ (π» β β β (π» β Sβ β (0β β π» β§ (βπ₯ β π» βπ¦ β π» (π₯ +β π¦) β π» β§ βπ₯ β β βπ¦ β π» (π₯ Β·β π¦) β π»)))) | ||
Theorem | shsubcl 30737 | Closure of vector subtraction in a subspace of a Hilbert space. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ ((π» β Sβ β§ π΄ β π» β§ π΅ β π») β (π΄ ββ π΅) β π») | ||
Definition | df-ch 30738 | Define the set of closed subspaces of a Hilbert space. A closed subspace is one in which the limit of every convergent sequence in the subspace belongs to the subspace. For its membership relation, see isch 30739. From Definition of [Beran] p. 107. Alternate definitions are given by isch2 30740 and isch3 30758. (Contributed by NM, 17-Aug-1999.) (New usage is discouraged.) |
β’ Cβ = {β β Sβ β£ ( βπ£ β (β βm β)) β β} | ||
Theorem | isch 30739 | Closed subspace π» of a Hilbert space. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Cβ β (π» β Sβ β§ ( βπ£ β (π» βm β)) β π»)) | ||
Theorem | isch2 30740* | Closed subspace π» of a Hilbert space. Definition of [Beran] p. 107. (Contributed by NM, 17-Aug-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Cβ β (π» β Sβ β§ βπβπ₯((π:ββΆπ» β§ π βπ£ π₯) β π₯ β π»))) | ||
Theorem | chsh 30741 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Cβ β π» β Sβ ) | ||
Theorem | chsssh 30742 | Closed subspaces are subspaces in a Hilbert space. (Contributed by NM, 29-May-1999.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ Cβ β Sβ | ||
Theorem | chex 30743 | The set of closed subspaces of a Hilbert space exists (is a set). (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ Cβ β V | ||
Theorem | chshii 30744 | A closed subspace is a subspace. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ π» β Sβ | ||
Theorem | ch0 30745 | The zero vector belongs to any closed subspace of a Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.) |
β’ (π» β Cβ β 0β β π») | ||
Theorem | chss 30746 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 24-Aug-1999.) (New usage is discouraged.) |
β’ (π» β Cβ β π» β β) | ||
Theorem | chel 30747 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 15-Dec-2004.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β π») β π΄ β β) | ||
Theorem | chssii 30748 | A closed subspace of a Hilbert space is a subset of Hilbert space. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ π» β β | ||
Theorem | cheli 30749 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π΄ β π» β π΄ β β) | ||
Theorem | chelii 30750 | A member of a closed subspace of a Hilbert space is a vector. (Contributed by NM, 6-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β π» β β’ π΄ β β | ||
Theorem | chlimi 30751 | The limit property of a closed subspace of a Hilbert space. (Contributed by NM, 14-Sep-1999.) (New usage is discouraged.) |
β’ π΄ β V β β’ ((π» β Cβ β§ πΉ:ββΆπ» β§ πΉ βπ£ π΄) β π΄ β π») | ||
Theorem | hlim0 30752 | The zero sequence in Hilbert space converges to the zero vector. (Contributed by NM, 17-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (β Γ {0β}) βπ£ 0β | ||
Theorem | hlimcaui 30753 | If a sequence in Hilbert space subset converges to a limit, it is a Cauchy sequence. (Contributed by NM, 17-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (πΉ βπ£ π΄ β πΉ β Cauchy) | ||
Theorem | hlimf 30754 | Function-like behavior of the convergence relation. (Contributed by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ βπ£ :dom βπ£ βΆ β | ||
Theorem | hlimuni 30755 | A Hilbert space sequence converges to at most one limit. (Contributed by NM, 19-Aug-1999.) (Revised by Mario Carneiro, 2-May-2015.) (New usage is discouraged.) |
β’ ((πΉ βπ£ π΄ β§ πΉ βπ£ π΅) β π΄ = π΅) | ||
Theorem | hlimreui 30756* | The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (βπ₯ β π» πΉ βπ£ π₯ β β!π₯ β π» πΉ βπ£ π₯) | ||
Theorem | hlimeui 30757* | The limit of a Hilbert space sequence is unique. (Contributed by NM, 19-Aug-1999.) (Proof shortened by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (βπ₯ πΉ βπ£ π₯ β β!π₯ πΉ βπ£ π₯) | ||
Theorem | isch3 30758* | A Hilbert subspace is closed iff it is complete. A complete subspace is one in which every Cauchy sequence of vectors in the subspace converges to a member of the subspace (Definition of complete subspace in [Beran] p. 96). Remark 3.12 of [Beran] p. 107. (Contributed by NM, 24-Dec-2001.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (π» β Cβ β (π» β Sβ β§ βπ β Cauchy (π:ββΆπ» β βπ₯ β π» π βπ£ π₯))) | ||
Theorem | chcompl 30759* | Completeness of a closed subspace of Hilbert space. (Contributed by NM, 4-Oct-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ πΉ β Cauchy β§ πΉ:ββΆπ») β βπ₯ β π» πΉ βπ£ π₯) | ||
Theorem | helch 30760 | The Hilbert lattice one (which is all of Hilbert space) belongs to the Hilbert lattice. Part of Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 6-Sep-1999.) (New usage is discouraged.) |
β’ β β Cβ | ||
Theorem | ifchhv 30761 | Prove if(π΄ β Cβ , π΄, β) β Cβ. (Contributed by David A. Wheeler, 8-Dec-2018.) (New usage is discouraged.) |
β’ if(π΄ β Cβ , π΄, β) β Cβ | ||
Theorem | helsh 30762 | Hilbert space is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
β’ β β Sβ | ||
Theorem | shsspwh 30763 | Subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
β’ Sβ β π« β | ||
Theorem | chsspwh 30764 | Closed subspaces are subsets of Hilbert space. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
β’ Cβ β π« β | ||
Theorem | hsn0elch 30765 | The zero subspace belongs to the set of closed subspaces of Hilbert space. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
β’ {0β} β Cβ | ||
Theorem | norm1 30766 | From any nonzero Hilbert space vector, construct a vector whose norm is 1. (Contributed by NM, 7-Feb-2006.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΄ β 0β) β (normββ((1 / (normββπ΄)) Β·β π΄)) = 1) | ||
Theorem | norm1exi 30767* | A normalized vector exists in a subspace iff the subspace has a nonzero vector. (Contributed by NM, 9-Apr-2006.) (New usage is discouraged.) |
β’ π» β Sβ β β’ (βπ₯ β π» π₯ β 0β β βπ¦ β π» (normββπ¦) = 1) | ||
Theorem | norm1hex 30768 | A normalized vector can exist only iff the Hilbert space has a nonzero vector. (Contributed by NM, 21-Jan-2006.) (New usage is discouraged.) |
β’ (βπ₯ β β π₯ β 0β β βπ¦ β β (normββπ¦) = 1) | ||
Definition | df-oc 30769* | 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 30797 and chocvali 30816 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.) |
β’ β₯ = (π₯ β π« β β¦ {π¦ β β β£ βπ§ β π₯ (π¦ Β·ih π§) = 0}) | ||
Definition | df-ch0 30770 | Define the zero for closed subspaces of Hilbert space. See h0elch 30772 for closure law. (Contributed by NM, 30-May-1999.) (New usage is discouraged.) |
β’ 0β = {0β} | ||
Theorem | elch0 30771 | Membership in zero for closed subspaces of Hilbert space. (Contributed by NM, 6-Apr-2001.) (New usage is discouraged.) |
β’ (π΄ β 0β β π΄ = 0β) | ||
Theorem | h0elch 30772 | 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.) |
β’ 0β β Cβ | ||
Theorem | h0elsh 30773 | The zero subspace is a subspace of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
β’ 0β β Sβ | ||
Theorem | hhssva 30774 | The vector addition operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ ( +β βΎ (π» Γ π»)) = ( +π£ βπ) | ||
Theorem | hhsssm 30775 | The scalar multiplication operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ ( Β·β βΎ (β Γ π»)) = ( Β·π OLD βπ) | ||
Theorem | hhssnm 30776 | The norm operation on a subspace. (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ (normβ βΎ π») = (normCVβπ) | ||
Theorem | issubgoilem 30777* | Lemma for hhssabloilem 30778. (Contributed by Paul Chapman, 25-Feb-2008.) (New usage is discouraged.) |
β’ ((π₯ β π β§ π¦ β π) β (π₯π»π¦) = (π₯πΊπ¦)) β β’ ((π΄ β π β§ π΅ β π) β (π΄π»π΅) = (π΄πΊπ΅)) | ||
Theorem | hhssabloilem 30778 | Lemma for hhssabloi 30779. Formerly part of proof for hhssabloi 30779 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 30779 | 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 30780 | Abelian group property of subspace addition. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
β’ (π» β Sβ β ( +β βΎ (π» Γ π»)) β AbelOp) | ||
Theorem | hhssnv 30781 | Normed complex vector space property of a subspace. (Contributed by NM, 26-Mar-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π» β Sβ β β’ π β NrmCVec | ||
Theorem | hhssnvt 30782 | Normed complex vector space property of a subspace. (Contributed by NM, 9-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ (π» β Sβ β π β NrmCVec) | ||
Theorem | hhsst 30783 | A member of Sβ is a subspace. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ (π» β Sβ β π β (SubSpβπ)) | ||
Theorem | hhshsslem1 30784 | Lemma for hhsssh 30786. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π β (SubSpβπ) & β’ π» β β β β’ π» = (BaseSetβπ) | ||
Theorem | hhshsslem2 30785 | Lemma for hhsssh 30786. (Contributed by NM, 6-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π β (SubSpβπ) & β’ π» β β β β’ π» β Sβ | ||
Theorem | hhsssh 30786 | The predicate "π» is a subspace of Hilbert space." (Contributed by NM, 25-Mar-2008.) (New usage is discouraged.) |
β’ π = β¨β¨ +β , Β·β β©, normββ© & β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ (π» β Sβ β (π β (SubSpβπ) β§ π» β β)) | ||
Theorem | hhsssh2 30787 | The predicate "π» is a subspace of Hilbert space." (Contributed by NM, 8-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© β β’ (π» β Sβ β (π β NrmCVec β§ π» β β)) | ||
Theorem | hhssba 30788 | The base set of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π» β Sβ β β’ π» = (BaseSetβπ) | ||
Theorem | hhssvs 30789 | The vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π» β Sβ β β’ ( ββ βΎ (π» Γ π»)) = ( βπ£ βπ) | ||
Theorem | hhssvsf 30790 | Mapping of the vector subtraction operation on a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π» β Sβ β β’ ( ββ βΎ (π» Γ π»)):(π» Γ π»)βΆπ» | ||
Theorem | hhssims 30791 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π» β Sβ & β’ π· = ((normβ β ββ ) βΎ (π» Γ π»)) β β’ π· = (IndMetβπ) | ||
Theorem | hhssims2 30792 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π· = (IndMetβπ) & β’ π» β Sβ β β’ π· = ((normβ β ββ ) βΎ (π» Γ π»)) | ||
Theorem | hhssmet 30793 | Induced metric of a subspace. (Contributed by NM, 10-Apr-2008.) (New usage is discouraged.) |
β’ π = β¨β¨( +β βΎ (π» Γ π»)), ( Β·β βΎ (β Γ π»))β©, (normβ βΎ π»)β© & β’ π· = (IndMetβπ) & β’ π» β Sβ β β’ π· β (Metβπ») | ||
Theorem | hhssmetdval 30794 | 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 30795 | 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 30796 | Obsolete version of cssbn 25124: 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 30797* | 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 30798* | Membership in orthogonal complement of H subset. (Contributed by NM, 7-Aug-2000.) (New usage is discouraged.) |
β’ (π» β β β (π΄ β (β₯βπ») β (π΄ β β β§ βπ₯ β π» (π΄ Β·ih π₯) = 0))) | ||
Theorem | shocel 30799* | Membership in orthogonal complement of H subspace. (Contributed by NM, 9-Oct-1999.) (New usage is discouraged.) |
β’ (π» β Sβ β (π΄ β (β₯βπ») β (π΄ β β β§ βπ₯ β π» (π΄ Β·ih π₯) = 0))) | ||
Theorem | ocsh 30800 | 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β ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |