Home | Metamath
Proof Explorer Theorem List (p. 383 of 470) | < 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: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | paddssw1 38201 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β π β§ π β π) β (π + π) β (π + π))) | ||
Theorem | paddssw2 38202 | Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π + π) β π β (π β π β§ π β π))) | ||
Theorem | paddss 38203 | Subset law for projective subspace sum. (unss 4142 analog.) (Contributed by NM, 7-Mar-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β π΅ β§ (π β π΄ β§ π β π΄ β§ π β π)) β ((π β π β§ π β π) β (π + π) β π)) | ||
Theorem | pmodlem1 38204* | Lemma for pmod1i 38206. (Contributed by NM, 9-Mar-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ π β π) β§ (π β π β§ π β π β§ π β€ (π β¨ π))) β π β (π + (π β© π))) | ||
Theorem | pmodlem2 38205 | Lemma for pmod1i 38206. (Contributed by NM, 9-Mar-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ π β π) β ((π + π) β© π) β (π + (π β© π))) | ||
Theorem | pmod1i 38206 | The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β (π β π β ((π + π) β© π) = (π + (π β© π)))) | ||
Theorem | pmod2iN 38207 | Dual of the modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄)) β (π β π β ((π β© π) + π) = (π β© (π + π)))) | ||
Theorem | pmodN 38208 | The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄)) β (π β© (π + (π β© π))) = ((π β© π) + (π β© π))) | ||
Theorem | pmodl42N 38209 | Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ π β π)) β (((π + π) + π) β© ((π + π) + π)) = ((π + π) + ((π + π) β© (π + π)))) | ||
Theorem | pmapjoin 38210 | The projective map of the join of two lattice elements. Part of Equation 15.5.3 of [MaedaMaeda] p. 63. (Contributed by NM, 27-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β ((πβπ) + (πβπ)) β (πβ(π β¨ π))) | ||
Theorem | pmapjat1 38211 | The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (πβ(π β¨ π)) = ((πβπ) + (πβπ))) | ||
Theorem | pmapjat2 38212 | The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (πβ(π β¨ π)) = ((πβπ) + (πβπ))) | ||
Theorem | pmapjlln1 38213 | The projective map of the join of a lattice element and a lattice line (expressed as the join π β¨ π of two atoms). (Contributed by NM, 16-Sep-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β (πβ(π β¨ (π β¨ π ))) = ((πβπ) + (πβ(π β¨ π )))) | ||
Theorem | hlmod1i 38214 | A version of the modular law pmod1i 38206 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ (πΉβ(π β¨ π)) = ((πΉβπ) + (πΉβπ))) β ((π β¨ π) β§ π) = (π β¨ (π β§ π)))) | ||
Theorem | atmod1i1 38215 | Version of modular law pmod1i 38206 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 11-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) | ||
Theorem | atmod1i1m 38216 | Version of modular law pmod1i 38206 that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄) β§ (π β π΅ β§ π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β ((π β§ π) β¨ (π β§ π)) = (((π β§ π) β¨ π) β§ π)) | ||
Theorem | atmod1i2 38217 | Version of modular law pmod1i 38206 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) | ||
Theorem | llnmod1i2 38218 | Version of modular law pmod1i 38206 that holds in a Hilbert lattice, when one element is a lattice line (expressed as the join π β¨ π). (Contributed by NM, 16-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ π β π΄) β§ π β€ π) β (π β¨ ((π β¨ π) β§ π)) = ((π β¨ (π β¨ π)) β§ π)) | ||
Theorem | atmod2i1 38219 | Version of modular law pmod2iN 38207 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β ((π β§ π) β¨ π) = (π β§ (π β¨ π))) | ||
Theorem | atmod2i2 38220 | Version of modular law pmod2iN 38207 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β ((π β§ π) β¨ π) = (π β§ (π β¨ π))) | ||
Theorem | llnmod2i2 38221 | Version of modular law pmod1i 38206 that holds in a Hilbert lattice, when one element is a lattice line (expressed as the join π β¨ π). (Contributed by NM, 16-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ π β π΄) β§ π β€ π) β ((π β§ (π β¨ π)) β¨ π) = (π β§ ((π β¨ π) β¨ π))) | ||
Theorem | atmod3i1 38222 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) = (π β§ (π β¨ π))) | ||
Theorem | atmod3i2 38223 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) = (π β§ (π β¨ π))) | ||
Theorem | atmod4i1 38224 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β ((π β§ π) β¨ π) = ((π β¨ π) β§ π)) | ||
Theorem | atmod4i2 38225 | Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012.) (Revised by Mario Carneiro, 10-Mar-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΅ β§ π β π΅) β§ π β€ π) β ((π β§ π) β¨ π) = ((π β¨ π) β§ π)) | ||
Theorem | llnexchb2lem 38226 | Lemma for llnexchb2 38227. (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) | ||
Theorem | llnexchb2 38227 | Line exchange property (compare cvlatexchb2 37692 for atoms). (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β§ π) β€ π β (π β§ π) = (π β§ π))) | ||
Theorem | llnexch2N 38228 | Line exchange property (compare cvlatexch2 37694 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β§ π) β€ π β (π β§ π) β€ π)) | ||
Theorem | dalawlem1 38229 | Lemma for dalaw 38244. Special case of dath2 38095, where πΆ is replaced by ((π β¨ π) β§ (π β¨ π)). The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 38095. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π) β¨ π ) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π))) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem2 38230 | Lemma for dalaw 38244. Utility lemma that breaks ((π β¨ π) β§ (π β¨ π)) into a join of two pieces. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ ((((π β¨ π) β¨ π) β§ π) β¨ (((π β¨ π) β¨ π) β§ π))) | ||
Theorem | dalawlem3 38231 | Lemma for dalaw 38244. First piece of dalawlem5 38233. (Contributed by NM, 4-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem4 38232 | Lemma for dalaw 38244. Second piece of dalawlem5 38233. (Contributed by NM, 4-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem5 38233 | Lemma for dalaw 38244. Special case to eliminate the requirement Β¬ (π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) in dalawlem1 38229. (Contributed by NM, 4-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem6 38234 | Lemma for dalaw 38244. First piece of dalawlem8 38236. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem7 38235 | Lemma for dalaw 38244. Second piece of dalawlem8 38236. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem8 38236 | Lemma for dalaw 38244. Special case to eliminate the requirement Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) in dalawlem1 38229. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem9 38237 | Lemma for dalaw 38244. Special case to eliminate the requirement Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) in dalawlem1 38229. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem10 38238 | Lemma for dalaw 38244. Combine dalawlem5 38233, dalawlem8 38236, and dalawlem9 . (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ Β¬ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem11 38239 | Lemma for dalaw 38244. First part of dalawlem13 38241. (Contributed by NM, 17-Sep-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem12 38240 | Lemma for dalaw 38244. Second part of dalawlem13 38241. (Contributed by NM, 17-Sep-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π = π β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem13 38241 | Lemma for dalaw 38244. Special case to eliminate the requirement ((π β¨ π) β¨ π ) β π in dalawlem1 38229. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ Β¬ ((π β¨ π) β¨ π ) β π β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem14 38242 | Lemma for dalaw 38244. Combine dalawlem10 38238 and dalawlem13 38241. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ Β¬ (((π β¨ π) β¨ π ) β π β§ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π))) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem15 38243 | Lemma for dalaw 38244. Swap variable triples πππ and πππ in dalawlem14 38242, to obtain the elimination of the remaining conditions in dalawlem1 38229. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ Β¬ (((π β¨ π) β¨ π) β π β§ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π))) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalaw 38244 | Desargues's law, derived from Desargues's theorem dath 38094 and with no conditions on the atoms. If triples β¨π, π, π β© and β¨π, π, πβ© are centrally perspective, i.e., ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π), then they are axially perspective. Theorem 13.3 of [Crawley] p. 110. (Contributed by NM, 7-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π))))) | ||
Syntax | cpclN 38245 | Extend class notation with projective subspace closure. |
class PCl | ||
Definition | df-pclN 38246* | Projective subspace closure, which is the smallest projective subspace containing an arbitrary set of atoms. The subspace closure of the union of a set of projective subspaces is their supremum in PSubSp. Related to an analogous definition of closure used in Lemma 3.1.4 of [PtakPulmannova] p. 68. (Note that this closure is not necessarily one of the closed projective subspaces PSubCl of df-psubclN 38293.) (Contributed by NM, 7-Sep-2013.) |
β’ PCl = (π β V β¦ (π₯ β π« (Atomsβπ) β¦ β© {π¦ β (PSubSpβπ) β£ π₯ β π¦})) | ||
Theorem | pclfvalN 38247* | The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ (πΎ β π β π = (π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦})) | ||
Theorem | pclvalN 38248* | Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π΄) β (πβπ) = β© {π¦ β π β£ π β π¦}) | ||
Theorem | pclclN 38249 | Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π΄) β (πβπ) β π) | ||
Theorem | elpclN 38250* | Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) & β’ π β V β β’ ((πΎ β π β§ π β π΄) β (π β (πβπ) β βπ¦ β π (π β π¦ β π β π¦))) | ||
Theorem | elpcliN 38251 | Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ (((πΎ β π β§ π β π β§ π β π) β§ π β (πβπ)) β π β π) | ||
Theorem | pclssN 38252 | Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π β§ π β π΄) β (πβπ) β (πβπ)) | ||
Theorem | pclssidN 38253 | A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π΄) β π β (πβπ)) | ||
Theorem | pclidN 38254 | The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π) β (πβπ) = π) | ||
Theorem | pclbtwnN 38255 | A projective subspace sandwiched between a set of atoms and the set's projective subspace closure equals the closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ (((πΎ β π β§ π β π) β§ (π β π β§ π β (πβπ))) β π = (πβπ)) | ||
Theorem | pclunN 38256 | The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π΄ β§ π β π΄) β (πβ(π βͺ π)) = (πβ(π + π))) | ||
Theorem | pclun2N 38257 | The projective subspace closure of the union of two subspaces equals their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β (πβ(π βͺ π)) = (π + π)) | ||
Theorem | pclfinN 38258* | The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of [PtakPulmannova] p. 72. Compare the closed subspace version pclfinclN 38308. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β (πβπ) = βͺ π¦ β (Fin β© π« π)(πβπ¦)) | ||
Theorem | pclcmpatN 38259* | The set of projective subspaces is compactly atomistic: if an atom is in the projective subspace closure of a set of atoms, it also belongs to the projective subspace closure of a finite subset of that set. Analogous to Lemma 3.3.10 of [PtakPulmannova] p. 74. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β AtLat β§ π β π΄ β§ π β (πβπ)) β βπ¦ β Fin (π¦ β π β§ π β (πβπ¦))) | ||
Syntax | cpolN 38260 | Extend class notation with polarity of projective subspace $m$. |
class β₯π | ||
Definition | df-polarityN 38261* | Define polarity of projective subspace, which is a kind of complement of the subspace. Item 2 in [Holland95] p. 222 bottom. For more generality, we define it for all subsets of atoms, not just projective subspaces. The intersection with Atomsβπ ensures it is defined when π = β . (Contributed by NM, 23-Oct-2011.) |
β’ β₯π = (π β V β¦ (π β π« (Atomsβπ) β¦ ((Atomsβπ) β© β© π β π ((pmapβπ)β((ocβπ)βπ))))) | ||
Theorem | polfvalN 38262* | The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ (πΎ β π΅ β π = (π β π« π΄ β¦ (π΄ β© β© π β π (πβ( β₯ βπ))))) | ||
Theorem | polvalN 38263* | Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β π΅ β§ π β π΄) β (πβπ) = (π΄ β© β© π β π (πβ( β₯ βπ)))) | ||
Theorem | polval2N 38264 | Alternate expression for value of the projective subspace polarity function. Equation for polarity in [Holland95] p. 223. (Contributed by NM, 22-Jan-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (πβπ) = (πβ( β₯ β(πβπ)))) | ||
Theorem | polsubN 38265 | The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π) | ||
Theorem | polssatN 38266 | The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) | ||
Theorem | pol0N 38267 | The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ (πΎ β π΅ β ( β₯ ββ ) = π΄) | ||
Theorem | pol1N 38268 | The polarity of the whole projective subspace is the empty space. Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ (πΎ β HL β ( β₯ βπ΄) = β ) | ||
Theorem | 2pol0N 38269 | The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ β₯ = (β₯πβπΎ) β β’ (πΎ β HL β ( β₯ β( β₯ ββ )) = β ) | ||
Theorem | polpmapN 38270 | The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβ(πβπ)) = (πβ( β₯ βπ))) | ||
Theorem | 2polpmapN 38271 | Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (pmapβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΅) β ( β₯ β( β₯ β(πβπ))) = (πβπ)) | ||
Theorem | 2polvalN 38272 | Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯ βπ)) = (πβ(πβπ))) | ||
Theorem | 2polssN 38273 | A set of atoms is a subset of its double polarity. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β π β ( β₯ β( β₯ βπ))) | ||
Theorem | 3polN 38274 | Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯ β( β₯ βπ))) = ( β₯ βπ)) | ||
Theorem | polcon3N 38275 | Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π) β ( β₯ βπ) β ( β₯ βπ)) | ||
Theorem | 2polcon4bN 38276 | Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ β( β₯ βπ)) β ( β₯ β( β₯ βπ)) β ( β₯ βπ) β ( β₯ βπ))) | ||
Theorem | polcon2N 38277 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) | ||
Theorem | polcon2bN 38278 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β ( β₯ βπ) β π β ( β₯ βπ))) | ||
Theorem | pclss2polN 38279 | The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (πβπ) β ( β₯ β( β₯ βπ))) | ||
Theorem | pcl0N 38280 | The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ π = (PClβπΎ) β β’ (πΎ β HL β (πββ ) = β ) | ||
Theorem | pcl0bN 38281 | The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ((πβπ) = β β π = β )) | ||
Theorem | pmaplubN 38282 | The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (lubβπΎ) & β’ π = (pmapβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβ(πβπ)) = π) | ||
Theorem | sspmaplubN 38283 | A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) β β’ ((πΎ β HL β§ π β π΄) β π β (πβ(πβπ))) | ||
Theorem | 2pmaplubN 38284 | Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (πβ(πβ(πβ(πβπ)))) = (πβ(πβπ))) | ||
Theorem | paddunN 38285 | The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d 6841.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β(π + π)) = ( β₯ β(π βͺ π))) | ||
Theorem | poldmj1N 38286 | De Morgan's law for polarity of projective sum. (oldmj1 37578 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) | ||
Theorem | pmapj2N 38287 | The projective map of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π = (pmapβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πβ(π β¨ π)) = ( β₯ β( β₯ β((πβπ) + (πβπ))))) | ||
Theorem | pmapocjN 38288 | The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (πΉβ( β₯ β(π β¨ π))) = (πβ((πΉβπ) + (πΉβπ)))) | ||
Theorem | polatN 38289 | The polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β OL β§ π β π΄) β (πβ{π}) = (πβ( β₯ βπ))) | ||
Theorem | 2polatN 38290 | Double polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (πβ(πβ{π})) = {π}) | ||
Theorem | pnonsingN 38291 | The intersection of a set of atoms and its polarity is empty. Definition of nonsingular in [Holland95] p. 214. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (π β© (πβπ)) = β ) | ||
Syntax | cpscN 38292 | Extend class notation with set of all closed projective subspaces for a Hilbert lattice. |
class PSubCl | ||
Definition | df-psubclN 38293* | Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in [Holland95] p. 223. (Contributed by NM, 23-Jan-2012.) |
β’ PSubCl = (π β V β¦ {π β£ (π β (Atomsβπ) β§ ((β₯πβπ)β((β₯πβπ)βπ )) = π )}) | ||
Theorem | psubclsetN 38294* | The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ (πΎ β π΅ β πΆ = {π β£ (π β π΄ β§ ( β₯ β( β₯ βπ )) = π )}) | ||
Theorem | ispsubclN 38295 | The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ (πΎ β π· β (π β πΆ β (π β π΄ β§ ( β₯ β( β₯ βπ)) = π))) | ||
Theorem | psubcliN 38296 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β π· β§ π β πΆ) β (π β π΄ β§ ( β₯ β( β₯ βπ)) = π)) | ||
Theorem | psubcli2N 38297 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β π· β§ π β πΆ) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | psubclsubN 38298 | A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β πΆ) β π β π) | ||
Theorem | psubclssatN 38299 | A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β π· β§ π β πΆ) β π β π΄) | ||
Theorem | pmapidclN 38300 | Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π = (pmapβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β πΆ) β (πβ(πβπ)) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |