![]() |
Metamath
Proof Explorer Theorem List (p. 307 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | chjvali 30601 | Value of join in Cβ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ β¨β π΅) = (β₯β(β₯β(π΄ βͺ π΅))) | ||
Theorem | sshjval3 30602 | 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 30603 | Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β¨β π΅) β Cβ ) | ||
Theorem | shjcl 30604 | Closure of join in Sβ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β¨β π΅) β Cβ ) | ||
Theorem | chjcl 30605 | Closure of join in Cβ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β Cβ β§ π΅ β Cβ ) β (π΄ β¨β π΅) β Cβ ) | ||
Theorem | shjcom 30606 | Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β¨β π΅) = (π΅ β¨β π΄)) | ||
Theorem | shless 30607 | Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (((π΄ β Sβ β§ π΅ β Sβ β§ πΆ β Sβ ) β§ π΄ β π΅) β (π΄ +β πΆ) β (π΅ +β πΆ)) | ||
Theorem | shlej1 30608 | 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 30609 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ (((π΄ β Sβ β§ π΅ β Sβ β§ πΆ β Sβ ) β§ π΄ β π΅) β (πΆ β¨β π΄) β (πΆ β¨β π΅)) | ||
Theorem | shincli 30610 | Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β© π΅) β Sβ | ||
Theorem | shscomi 30611 | Commutative law for subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | shsvai 30612 | Vector sum belongs to subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ ((πΆ β π΄ β§ π· β π΅) β (πΆ +β π·) β (π΄ +β π΅)) | ||
Theorem | shsel1i 30613 | 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 30614 | 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 30615 | Vector subtraction belongs to subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ ((πΆ β π΄ β§ π· β π΅) β (πΆ ββ π·) β (π΄ +β π΅)) | ||
Theorem | shunssi 30616 | Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ βͺ π΅) β (π΄ +β π΅) | ||
Theorem | shunssji 30617 | 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 30618 | 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 30619 | Commutative law for join in Sβ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β¨β π΅) = (π΅ β¨β π΄) | ||
Theorem | shsub1i 30620 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ π΄ β (π΄ +β π΅) | ||
Theorem | shsub2i 30621 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ π΄ β (π΅ +β π΄) | ||
Theorem | shub1i 30622 | Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ π΄ β (π΄ β¨β π΅) | ||
Theorem | shjcli 30623 | Closure of Cβ join. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β¨β π΅) β Cβ | ||
Theorem | shjshcli 30624 | Sβ closure of join. (Contributed by NM, 5-May-2000.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β¨β π΅) β Sβ | ||
Theorem | shlessi 30625 | Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (π΄ β π΅ β (π΄ +β πΆ) β (π΅ +β πΆ)) | ||
Theorem | shlej1i 30626 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (π΄ β π΅ β (π΄ β¨β πΆ) β (π΅ β¨β πΆ)) | ||
Theorem | shlej2i 30627 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (π΄ β π΅ β (πΆ β¨β π΄) β (πΆ β¨β π΅)) | ||
Theorem | shslej 30628 | Subspace sum is smaller than subspace join. Remark in [Kalmbach] p. 65. (Contributed by NM, 12-Jul-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ +β π΅) β (π΄ β¨β π΅)) | ||
Theorem | shincl 30629 | Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β© π΅) β Sβ ) | ||
Theorem | shub1 30630 | Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β π΄ β (π΄ β¨β π΅)) | ||
Theorem | shub2 30631 | A subspace is a subset of its Hilbert lattice join with another. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β π΄ β (π΅ β¨β π΄)) | ||
Theorem | shsidmi 30632 | Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ β β’ (π΄ +β π΄) = π΄ | ||
Theorem | shslubi 30633 | The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ ((π΄ β πΆ β§ π΅ β πΆ) β (π΄ +β π΅) β πΆ) | ||
Theorem | shlesb1i 30634 | Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β π΅ β (π΄ +β π΅) = π΅) | ||
Theorem | shsval2i 30635* | An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ +β π΅) = β© {π₯ β Sβ β£ (π΄ βͺ π΅) β π₯} | ||
Theorem | shsval3i 30636 | An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ +β π΅) = (spanβ(π΄ βͺ π΅)) | ||
Theorem | shmodsi 30637 | The modular law holds for subspace sum. Similar to part of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (π΄ β πΆ β ((π΄ +β π΅) β© πΆ) β (π΄ +β (π΅ β© πΆ))) | ||
Theorem | shmodi 30638 | The modular law is implied by the closure of subspace sum. Part of proof of Theorem 16.9 of [MaedaMaeda] p. 70. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (((π΄ +β π΅) = (π΄ β¨β π΅) β§ π΄ β πΆ) β ((π΄ β¨β π΅) β© πΆ) β (π΄ β¨β (π΅ β© πΆ))) | ||
Theorem | pjhthlem1 30639* | Lemma for pjhth 30641. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (Proof shortened by AV, 10-Jul-2022.) (New usage is discouraged.) |
β’ π» β Cβ & β’ (π β π΄ β β) & β’ (π β π΅ β π») & β’ (π β πΆ β π») & β’ (π β βπ₯ β π» (normββ(π΄ ββ π΅)) β€ (normββ(π΄ ββ π₯))) & β’ π = (((π΄ ββ π΅) Β·ih πΆ) / ((πΆ Β·ih πΆ) + 1)) β β’ (π β ((π΄ ββ π΅) Β·ih πΆ) = 0) | ||
Theorem | pjhthlem2 30640* | Lemma for pjhth 30641. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ π» β Cβ & β’ (π β π΄ β β) β β’ (π β βπ₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) | ||
Theorem | pjhth 30641 | Projection Theorem: Any Hilbert space vector π΄ can be decomposed uniquely into a member π₯ of a closed subspace π» and a member π¦ of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ (π» β Cβ β (π» +β (β₯βπ»)) = β) | ||
Theorem | pjhtheu 30642* | Projection Theorem: Any Hilbert space vector π΄ can be decomposed uniquely into a member π₯ of a closed subspace π» and a member π¦ of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102. See pjhtheu2 30664 for the uniqueness of π¦. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 14-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β β!π₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) | ||
Definition | df-pjh 30643* | Define the projection function on a Hilbert space, as a mapping from the Hilbert lattice to a function on Hilbert space. Every closed subspace is associated with a unique projection function. Remark in [Kalmbach] p. 66, adopted as a definition. (projββπ»)βπ΄ is the projection of vector π΄ onto closed subspace π». Note that the range of projβ is the set of all projection operators, so π β ran projβ means that π is a projection operator. (Contributed by NM, 23-Oct-1999.) (New usage is discouraged.) |
β’ projβ = (β β Cβ β¦ (π₯ β β β¦ (β©π§ β β βπ¦ β (β₯ββ)π₯ = (π§ +β π¦)))) | ||
Theorem | pjhfval 30644* | The value of the projection map. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ (π» β Cβ β (projββπ») = (π₯ β β β¦ (β©π§ β π» βπ¦ β (β₯βπ»)π₯ = (π§ +β π¦)))) | ||
Theorem | pjhval 30645* | Value of a projection. (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-Dec-2013.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) = (β©π₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦))) | ||
Theorem | pjpreeq 30646* | Equality with a projection. This version of pjeq 30647 does not assume the Axiom of Choice via pjhth 30641. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β (π» +β (β₯βπ»))) β (((projββπ»)βπ΄) = π΅ β (π΅ β π» β§ βπ₯ β (β₯βπ»)π΄ = (π΅ +β π₯)))) | ||
Theorem | pjeq 30647* | Equality with a projection. (Contributed by NM, 20-Jan-2007.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β (((projββπ»)βπ΄) = π΅ β (π΅ β π» β§ βπ₯ β (β₯βπ»)π΄ = (π΅ +β π₯)))) | ||
Theorem | axpjcl 30648 | Closure of a projection in its subspace. If we consider this together with axpjpj 30668 to be axioms, the need for the ax-hcompl 30450 can often be avoided for the kinds of theorems we are interested in here. An interesting project is to see how far we can go by using them in place of it. In particular, we can prove the orthomodular law pjomli 30683.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) β π») | ||
Theorem | pjhcl 30649 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) β β) | ||
Theorem | omlsilem 30650 | Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
β’ πΊ β Sβ & β’ π» β Sβ & β’ πΊ β π» & β’ (π» β© (β₯βπΊ)) = 0β & β’ π΄ β π» & β’ π΅ β πΊ & β’ πΆ β (β₯βπΊ) β β’ (π΄ = (π΅ +β πΆ) β π΄ β πΊ) | ||
Theorem | omlsii 30651 | Subspace inference form of orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Sβ & β’ π΄ β π΅ & β’ (π΅ β© (β₯βπ΄)) = 0β β β’ π΄ = π΅ | ||
Theorem | omlsi 30652 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Sβ β β’ ((π΄ β π΅ β§ (π΅ β© (β₯βπ΄)) = 0β) β π΄ = π΅) | ||
Theorem | ococi 30653 | Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (β₯β(β₯βπ΄)) = π΄ | ||
Theorem | ococ 30654 | Complement of complement of a closed subspace of Hilbert space. Theorem 3.7(ii) of [Beran] p. 102. (Contributed by NM, 11-Oct-1999.) (New usage is discouraged.) |
β’ (π΄ β Cβ β (β₯β(β₯βπ΄)) = π΄) | ||
Theorem | dfch2 30655 | Alternate definition of the Hilbert lattice. (Contributed by NM, 8-Aug-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ Cβ = {π₯ β π« β β£ (β₯β(β₯βπ₯)) = π₯} | ||
Theorem | ococin 30656* | The double complement is the smallest closed subspace containing a subset of Hilbert space. Remark 3.12(B) of [Beran] p. 107. (Contributed by NM, 8-Aug-2000.) (New usage is discouraged.) |
β’ (π΄ β β β (β₯β(β₯βπ΄)) = β© {π₯ β Cβ β£ π΄ β π₯}) | ||
Theorem | hsupval2 30657* | Alternate definition of supremum of a subset of the Hilbert lattice. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. We actually define it on any collection of Hilbert space subsets, not just the Hilbert lattice Cβ, to allow more general theorems. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β π« β β ( β¨β βπ΄) = β© {π₯ β Cβ β£ βͺ π΄ β π₯}) | ||
Theorem | chsupval2 30658* | The value of the supremum of a set of closed subspaces of Hilbert space. Definition of supremum in Proposition 1 of [Kalmbach] p. 65. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β ( β¨β βπ΄) = β© {π₯ β Cβ β£ βͺ π΄ β π₯}) | ||
Theorem | sshjval2 30659* | Value of join in the set of closed subspaces of Hilbert space Cβ. (Contributed by NM, 1-Nov-2000.) (Revised by Mario Carneiro, 23-Dec-2013.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β¨β π΅) = β© {π₯ β Cβ β£ (π΄ βͺ π΅) β π₯}) | ||
Theorem | chsupid 30660* | A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β ( β¨β β{π₯ β Cβ β£ π₯ β π΄}) = π΄) | ||
Theorem | chsupsn 30661 | Value of supremum of subset of Cβ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β ( β¨β β{π΄}) = π΄) | ||
Theorem | shlub 30662 | Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ β§ πΆ β Cβ ) β ((π΄ β πΆ β§ π΅ β πΆ) β (π΄ β¨β π΅) β πΆ)) | ||
Theorem | shlubi 30663 | Hilbert lattice join is the least upper bound (among Hilbert lattice elements) of two subspaces. (Contributed by NM, 11-Jun-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Cβ β β’ ((π΄ β πΆ β§ π΅ β πΆ) β (π΄ β¨β π΅) β πΆ) | ||
Theorem | pjhtheu2 30664* | Uniqueness of π¦ for the projection theorem. (Contributed by NM, 6-Nov-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β β!π¦ β (β₯βπ»)βπ₯ β π» π΄ = (π₯ +β π¦)) | ||
Theorem | pjcli 30665 | Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π΄ β β β ((projββπ»)βπ΄) β π») | ||
Theorem | pjhcli 30666 | Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π΄ β β β ((projββπ»)βπ΄) β β) | ||
Theorem | pjpjpre 30667 | Decomposition of a vector into projections. This formulation of axpjpj 30668 avoids pjhth 30641. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (π β π» β Cβ ) & β’ (π β π΄ β (π» +β (β₯βπ»))) β β’ (π β π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄))) | ||
Theorem | axpjpj 30668 | Decomposition of a vector into projections. See comment in axpjcl 30648. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄))) | ||
Theorem | pjclii 30669 | Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββπ»)βπ΄) β π» | ||
Theorem | pjhclii 30670 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββπ»)βπ΄) β β | ||
Theorem | pjpj0i 30671 | Decomposition of a vector into projections. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄)) | ||
Theorem | pjpji 30672 | Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄)) | ||
Theorem | pjpjhth 30673* | Projection Theorem: Any Hilbert space vector π΄ can be decomposed into a member π₯ of a closed subspace π» and a member π¦ of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β βπ₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) | ||
Theorem | pjpjhthi 30674* | Projection Theorem: Any Hilbert space vector π΄ can be decomposed into a member π₯ of a closed subspace π» and a member π¦ of the complement of the subspace. Theorem 3.7(i) of [Beran] p. 102 (existence part). (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β β & β’ π» β Cβ β β’ βπ₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦) | ||
Theorem | pjop 30675 | Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββ(β₯βπ»))βπ΄) = (π΄ ββ ((projββπ»)βπ΄))) | ||
Theorem | pjpo 30676 | Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) = (π΄ ββ ((projββ(β₯βπ»))βπ΄))) | ||
Theorem | pjopi 30677 | Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββ(β₯βπ»))βπ΄) = (π΄ ββ ((projββπ»)βπ΄)) | ||
Theorem | pjpoi 30678 | Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββπ»)βπ΄) = (π΄ ββ ((projββ(β₯βπ»))βπ΄)) | ||
Theorem | pjoc1i 30679 | Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ (π΄ β π» β ((projββ(β₯βπ»))βπ΄) = 0β) | ||
Theorem | pjchi 30680 | Projection of a vector in the projection subspace. Lemma 4.4(ii) of [Beran] p. 111. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ (π΄ β π» β ((projββπ»)βπ΄) = π΄) | ||
Theorem | pjoccl 30681 | The part of a vector that belongs to the orthocomplemented space. (Contributed by NM, 11-Apr-2006.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β (π΄ ββ ((projββπ»)βπ΄)) β (β₯βπ»)) | ||
Theorem | pjoc1 30682 | Projection of a vector in the orthocomplement of the projection subspace. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β (π΄ β π» β ((projββ(β₯βπ»))βπ΄) = 0β)) | ||
Theorem | pjomli 30683 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omlsi 30652. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Sβ β β’ ((π΄ β π΅ β§ (π΅ β© (β₯βπ΄)) = 0β) β π΄ = π΅) | ||
Theorem | pjoml 30684 | Subspace form of orthomodular law in the Hilbert lattice. Compare the orthomodular law in Theorem 2(ii) of [Kalmbach] p. 22. Derived using projections; compare omlsi 30652. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
β’ (((π΄ β Cβ β§ π΅ β Sβ ) β§ (π΄ β π΅ β§ (π΅ β© (β₯βπ΄)) = 0β)) β π΄ = π΅) | ||
Theorem | pjococi 30685 | Proof of orthocomplement theorem using projections. Compare ococ 30654. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (β₯β(β₯βπ»)) = π» | ||
Theorem | pjoc2i 30686 | Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111. (Contributed by NM, 27-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ (π΄ β (β₯βπ») β ((projββπ»)βπ΄) = 0β) | ||
Theorem | pjoc2 30687 | Projection of a vector in the orthocomplement of the projection subspace. Lemma 4.4(iii) of [Beran] p. 111. (Contributed by NM, 24-Apr-2006.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β (π΄ β (β₯βπ») β ((projββπ»)βπ΄) = 0β)) | ||
Theorem | sh0le 30688 | The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β Sβ β 0β β π΄) | ||
Theorem | ch0le 30689 | The zero subspace is the smallest member of Cβ. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β 0β β π΄) | ||
Theorem | shle0 30690 | No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
β’ (π΄ β Sβ β (π΄ β 0β β π΄ = 0β)) | ||
Theorem | chle0 30691 | No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β (π΄ β 0β β π΄ = 0β)) | ||
Theorem | chnlen0 30692 | A Hilbert lattice element that is not a subset of another is nonzero. (Contributed by NM, 30-Jun-2004.) (New usage is discouraged.) |
β’ (π΅ β Cβ β (Β¬ π΄ β π΅ β Β¬ π΄ = 0β)) | ||
Theorem | ch0pss 30693 | The zero subspace is a proper subset of nonzero Hilbert lattice elements. (Contributed by NM, 9-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β Cβ β (0β β π΄ β π΄ β 0β)) | ||
Theorem | orthin 30694 | The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β (β₯βπ΅) β (π΄ β© π΅) = 0β)) | ||
Theorem | ssjo 30695 | The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ β¨β (β₯βπ΄)) = β) | ||
Theorem | shne0i 30696* | A nonzero subspace has a nonzero vector. (Contributed by NM, 25-Feb-2006.) (New usage is discouraged.) |
β’ π΄ β Sβ β β’ (π΄ β 0β β βπ₯ β π΄ π₯ β 0β) | ||
Theorem | shs0i 30697 | Hilbert subspace sum with the zero subspace. (Contributed by NM, 14-Jan-2005.) (New usage is discouraged.) |
β’ π΄ β Sβ β β’ (π΄ +β 0β) = π΄ | ||
Theorem | shs00i 30698 | Two subspaces are zero iff their join is zero. (Contributed by NM, 7-Aug-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ ((π΄ = 0β β§ π΅ = 0β) β (π΄ +β π΅) = 0β) | ||
Theorem | ch0lei 30699 | The closed subspace zero is the smallest member of Cβ. (Contributed by NM, 15-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ 0β β π΄ | ||
Theorem | chle0i 30700 | No Hilbert closed subspace is smaller than zero. (Contributed by NM, 7-Apr-2001.) (New usage is discouraged.) |
β’ π΄ β Cβ β β’ (π΄ β 0β β π΄ = 0β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |