![]() |
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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | spanss 30601 | Ordering relationship for the spans of subsets of Hilbert space. (Contributed by NM, 2-Jun-2004.) (New usage is discouraged.) |
β’ ((π΅ β β β§ π΄ β π΅) β (spanβπ΄) β (spanβπ΅)) | ||
Theorem | spanssoc 30602 | 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 30603 | 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 30604 | Value of join in Sβ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β¨β π΅) = (β₯β(β₯β(π΄ βͺ π΅)))) | ||
Theorem | chjval 30605 | Value of join in Cβ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
β’ ((π΄ β Cβ β§ π΅ β Cβ ) β (π΄ β¨β π΅) = (β₯β(β₯β(π΄ βͺ π΅)))) | ||
Theorem | chjvali 30606 | Value of join in Cβ. (Contributed by NM, 9-Aug-2000.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Cβ β β’ (π΄ β¨β π΅) = (β₯β(β₯β(π΄ βͺ π΅))) | ||
Theorem | sshjval3 30607 | 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 30608 | Closure of join for subsets of Hilbert space. (Contributed by NM, 1-Nov-2000.) (New usage is discouraged.) |
β’ ((π΄ β β β§ π΅ β β) β (π΄ β¨β π΅) β Cβ ) | ||
Theorem | shjcl 30609 | Closure of join in Sβ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β¨β π΅) β Cβ ) | ||
Theorem | chjcl 30610 | Closure of join in Cβ. (Contributed by NM, 2-Nov-1999.) (New usage is discouraged.) |
β’ ((π΄ β Cβ β§ π΅ β Cβ ) β (π΄ β¨β π΅) β Cβ ) | ||
Theorem | shjcom 30611 | Commutative law for Hilbert lattice join of subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β¨β π΅) = (π΅ β¨β π΄)) | ||
Theorem | shless 30612 | Subset implies subset of subspace sum. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (((π΄ β Sβ β§ π΅ β Sβ β§ πΆ β Sβ ) β§ π΄ β π΅) β (π΄ +β πΆ) β (π΅ +β πΆ)) | ||
Theorem | shlej1 30613 | 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 30614 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ (((π΄ β Sβ β§ π΅ β Sβ β§ πΆ β Sβ ) β§ π΄ β π΅) β (πΆ β¨β π΄) β (πΆ β¨β π΅)) | ||
Theorem | shincli 30615 | Closure of intersection of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β© π΅) β Sβ | ||
Theorem | shscomi 30616 | Commutative law for subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ +β π΅) = (π΅ +β π΄) | ||
Theorem | shsvai 30617 | Vector sum belongs to subspace sum. (Contributed by NM, 17-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ ((πΆ β π΄ β§ π· β π΅) β (πΆ +β π·) β (π΄ +β π΅)) | ||
Theorem | shsel1i 30618 | 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 30619 | 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 30620 | Vector subtraction belongs to subspace sum. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ ((πΆ β π΄ β§ π· β π΅) β (πΆ ββ π·) β (π΄ +β π΅)) | ||
Theorem | shunssi 30621 | Union is smaller than subspace sum. (Contributed by NM, 18-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ βͺ π΅) β (π΄ +β π΅) | ||
Theorem | shunssji 30622 | 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 30623 | 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 30624 | Commutative law for join in Sβ. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β¨β π΅) = (π΅ β¨β π΄) | ||
Theorem | shsub1i 30625 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ π΄ β (π΄ +β π΅) | ||
Theorem | shsub2i 30626 | Subspace sum is an upper bound of its arguments. (Contributed by NM, 17-Dec-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ π΄ β (π΅ +β π΄) | ||
Theorem | shub1i 30627 | Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ π΄ β (π΄ β¨β π΅) | ||
Theorem | shjcli 30628 | Closure of Cβ join. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β¨β π΅) β Cβ | ||
Theorem | shjshcli 30629 | Sβ closure of join. (Contributed by NM, 5-May-2000.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β¨β π΅) β Sβ | ||
Theorem | shlessi 30630 | Subset implies subset of subspace sum. (Contributed by NM, 18-Nov-2000.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (π΄ β π΅ β (π΄ +β πΆ) β (π΅ +β πΆ)) | ||
Theorem | shlej1i 30631 | 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 30632 | Add disjunct to both sides of Hilbert subspace ordering. (Contributed by NM, 19-Oct-1999.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ (π΄ β π΅ β (πΆ β¨β π΄) β (πΆ β¨β π΅)) | ||
Theorem | shslej 30633 | 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 30634 | Closure of intersection of two subspaces. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β© π΅) β Sβ ) | ||
Theorem | shub1 30635 | Hilbert lattice join is an upper bound of two subspaces. (Contributed by NM, 22-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β π΄ β (π΄ β¨β π΅)) | ||
Theorem | shub2 30636 | 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 30637 | Idempotent law for Hilbert subspace sum. (Contributed by NM, 6-Jun-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ β β’ (π΄ +β π΄) = π΄ | ||
Theorem | shslubi 30638 | The least upper bound law for Hilbert subspace sum. (Contributed by NM, 15-Jun-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ & β’ πΆ β Sβ β β’ ((π΄ β πΆ β§ π΅ β πΆ) β (π΄ +β π΅) β πΆ) | ||
Theorem | shlesb1i 30639 | Hilbert lattice ordering in terms of subspace sum. (Contributed by NM, 23-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ β π΅ β (π΄ +β π΅) = π΅) | ||
Theorem | shsval2i 30640* | An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ +β π΅) = β© {π₯ β Sβ β£ (π΄ βͺ π΅) β π₯} | ||
Theorem | shsval3i 30641 | An alternate way to express subspace sum. (Contributed by NM, 25-Nov-2004.) (New usage is discouraged.) |
β’ π΄ β Sβ & β’ π΅ β Sβ β β’ (π΄ +β π΅) = (spanβ(π΄ βͺ π΅)) | ||
Theorem | shmodsi 30642 | 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 30643 | 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 30644* | Lemma for pjhth 30646. (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 30645* | Lemma for pjhth 30646. (Contributed by NM, 10-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ π» β Cβ & β’ (π β π΄ β β) β β’ (π β βπ₯ β π» βπ¦ β (β₯βπ»)π΄ = (π₯ +β π¦)) | ||
Theorem | pjhth 30646 | 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 30647* | 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 30669 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 30648* | 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 30649* | 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 30650* | 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 30651* | Equality with a projection. This version of pjeq 30652 does not assume the Axiom of Choice via pjhth 30646. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β (π» +β (β₯βπ»))) β (((projββπ»)βπ΄) = π΅ β (π΅ β π» β§ βπ₯ β (β₯βπ»)π΄ = (π΅ +β π₯)))) | ||
Theorem | pjeq 30652* | 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 30653 | Closure of a projection in its subspace. If we consider this together with axpjpj 30673 to be axioms, the need for the ax-hcompl 30455 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 30688.) (Contributed by NM, 23-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) β π») | ||
Theorem | pjhcl 30654 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) β β) | ||
Theorem | omlsilem 30655 | Lemma for orthomodular law in the Hilbert lattice. (Contributed by NM, 14-Oct-1999.) (New usage is discouraged.) |
β’ πΊ β Sβ & β’ π» β Sβ & β’ πΊ β π» & β’ (π» β© (β₯βπΊ)) = 0β & β’ π΄ β π» & β’ π΅ β πΊ & β’ πΆ β (β₯βπΊ) β β’ (π΄ = (π΅ +β πΆ) β π΄ β πΊ) | ||
Theorem | omlsii 30656 | 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 30657 | 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 30658 | 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 30659 | 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 30660 | 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 30661* | 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 30662* | 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 30663* | 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 30664* | 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 30665* | A subspace is the supremum of all smaller subspaces. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β ( β¨β β{π₯ β Cβ β£ π₯ β π΄}) = π΄) | ||
Theorem | chsupsn 30666 | Value of supremum of subset of Cβ on a singleton. (Contributed by NM, 13-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β ( β¨β β{π΄}) = π΄) | ||
Theorem | shlub 30667 | 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 30668 | 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 30669* | 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 30670 | Closure of a projection in its subspace. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π΄ β β β ((projββπ»)βπ΄) β π») | ||
Theorem | pjhcli 30671 | Closure of a projection in Hilbert space. (Contributed by NM, 7-Oct-2000.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (π΄ β β β ((projββπ»)βπ΄) β β) | ||
Theorem | pjpjpre 30672 | Decomposition of a vector into projections. This formulation of axpjpj 30673 avoids pjhth 30646. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (π β π» β Cβ ) & β’ (π β π΄ β (π» +β (β₯βπ»))) β β’ (π β π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄))) | ||
Theorem | axpjpj 30673 | Decomposition of a vector into projections. See comment in axpjcl 30653. (Contributed by NM, 26-Oct-1999.) (Revised by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄))) | ||
Theorem | pjclii 30674 | Closure of a projection in its subspace. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββπ»)βπ΄) β π» | ||
Theorem | pjhclii 30675 | Closure of a projection in Hilbert space. (Contributed by NM, 30-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββπ»)βπ΄) β β | ||
Theorem | pjpj0i 30676 | 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 30677 | Decomposition of a vector into projections. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ π΄ = (((projββπ»)βπ΄) +β ((projββ(β₯βπ»))βπ΄)) | ||
Theorem | pjpjhth 30678* | 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 30679* | 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 30680 | Orthocomplement projection in terms of projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββ(β₯βπ»))βπ΄) = (π΄ ββ ((projββπ»)βπ΄))) | ||
Theorem | pjpo 30681 | Projection in terms of orthocomplement projection. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
β’ ((π» β Cβ β§ π΄ β β) β ((projββπ»)βπ΄) = (π΄ ββ ((projββ(β₯βπ»))βπ΄))) | ||
Theorem | pjopi 30682 | Orthocomplement projection in terms of projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββ(β₯βπ»))βπ΄) = (π΄ ββ ((projββπ»)βπ΄)) | ||
Theorem | pjpoi 30683 | Projection in terms of orthocomplement projection. (Contributed by NM, 31-Oct-1999.) (New usage is discouraged.) |
β’ π» β Cβ & β’ π΄ β β β β’ ((projββπ»)βπ΄) = (π΄ ββ ((projββ(β₯βπ»))βπ΄)) | ||
Theorem | pjoc1i 30684 | 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 30685 | 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 30686 | 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 30687 | 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 30688 | 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 30657. (Contributed by NM, 6-Nov-1999.) (New usage is discouraged.) |
β’ π΄ β Cβ & β’ π΅ β Sβ β β’ ((π΄ β π΅ β§ (π΅ β© (β₯βπ΄)) = 0β) β π΄ = π΅) | ||
Theorem | pjoml 30689 | 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 30657. (Contributed by NM, 14-Jun-2006.) (New usage is discouraged.) |
β’ (((π΄ β Cβ β§ π΅ β Sβ ) β§ (π΄ β π΅ β§ (π΅ β© (β₯βπ΄)) = 0β)) β π΄ = π΅) | ||
Theorem | pjococi 30690 | Proof of orthocomplement theorem using projections. Compare ococ 30659. (Contributed by NM, 5-Nov-1999.) (New usage is discouraged.) |
β’ π» β Cβ β β’ (β₯β(β₯βπ»)) = π» | ||
Theorem | pjoc2i 30691 | 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 30692 | 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 30693 | The zero subspace is the smallest subspace. (Contributed by NM, 3-Jun-2004.) (New usage is discouraged.) |
β’ (π΄ β Sβ β 0β β π΄) | ||
Theorem | ch0le 30694 | The zero subspace is the smallest member of Cβ. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β 0β β π΄) | ||
Theorem | shle0 30695 | No subspace is smaller than the zero subspace. (Contributed by NM, 24-Nov-2004.) (New usage is discouraged.) |
β’ (π΄ β Sβ β (π΄ β 0β β π΄ = 0β)) | ||
Theorem | chle0 30696 | No Hilbert lattice element is smaller than zero. (Contributed by NM, 14-Aug-2002.) (New usage is discouraged.) |
β’ (π΄ β Cβ β (π΄ β 0β β π΄ = 0β)) | ||
Theorem | chnlen0 30697 | 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 30698 | 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 30699 | The intersection of orthogonal subspaces is the zero subspace. (Contributed by NM, 24-Jun-2004.) (New usage is discouraged.) |
β’ ((π΄ β Sβ β§ π΅ β Sβ ) β (π΄ β (β₯βπ΅) β (π΄ β© π΅) = 0β)) | ||
Theorem | ssjo 30700 | The lattice join of a subset with its orthocomplement is the whole space. (Contributed by Mario Carneiro, 15-May-2014.) (New usage is discouraged.) |
β’ (π΄ β β β (π΄ β¨β (β₯βπ΄)) = β) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |