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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pmapjoin 38201 | 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 38202 | 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 38203 | 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 38204 | 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 38205 | A version of the modular law pmod1i 38197 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ (πΉβ(π β¨ π)) = ((πΉβπ) + (πΉβπ))) β ((π β¨ π) β§ π) = (π β¨ (π β§ π)))) | ||
Theorem | atmod1i1 38206 | Version of modular law pmod1i 38197 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 38207 | Version of modular law pmod1i 38197 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 38208 | Version of modular law pmod1i 38197 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 38209 | Version of modular law pmod1i 38197 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 38210 | Version of modular law pmod2iN 38198 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 38211 | Version of modular law pmod2iN 38198 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 38212 | Version of modular law pmod1i 38197 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 38213 | 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 38214 | 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 38215 | 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 38216 | 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 38217 | Lemma for llnexchb2 38218. (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ π) β§ (π β§ π) β π΄) β ((π β§ π) β€ (π β¨ π) β (π β§ π) = (π β§ (π β¨ π)))) | ||
Theorem | llnexchb2 38218 | Line exchange property (compare cvlatexchb2 37683 for atoms). (Contributed by NM, 17-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β§ π) β€ π β (π β§ π) = (π β§ π))) | ||
Theorem | llnexch2N 38219 | Line exchange property (compare cvlatexch2 37685 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ ((π β§ π) β π΄ β§ π β π)) β ((π β§ π) β€ π β (π β§ π) β€ π)) | ||
Theorem | dalawlem1 38220 | Lemma for dalaw 38235. Special case of dath2 38086, where πΆ is replaced by ((π β¨ π) β§ (π β¨ π)). The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 38086. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (((π β¨ π) β¨ π ) β π β§ ((π β¨ π) β¨ π) β π) β§ ((Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π))) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem2 38221 | Lemma for dalaw 38235. Utility lemma that breaks ((π β¨ π) β§ (π β¨ π)) into a join of two pieces. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ ((((π β¨ π) β¨ π) β§ π) β¨ (((π β¨ π) β¨ π) β§ π))) | ||
Theorem | dalawlem3 38222 | Lemma for dalaw 38235. First piece of dalawlem5 38224. (Contributed by NM, 4-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem4 38223 | Lemma for dalaw 38235. Second piece of dalawlem5 38224. (Contributed by NM, 4-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem5 38224 | Lemma for dalaw 38235. Special case to eliminate the requirement Β¬ (π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) in dalawlem1 38220. (Contributed by NM, 4-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem6 38225 | Lemma for dalaw 38235. First piece of dalawlem8 38227. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem7 38226 | Lemma for dalaw 38235. Second piece of dalawlem8 38227. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π) β¨ π) β§ π) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem8 38227 | Lemma for dalaw 38235. Special case to eliminate the requirement Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) in dalawlem1 38220. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem9 38228 | Lemma for dalaw 38235. Special case to eliminate the requirement Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) in dalawlem1 38220. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem10 38229 | Lemma for dalaw 38235. Combine dalawlem5 38224, dalawlem8 38227, and dalawlem9 . (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ Β¬ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem11 38230 | Lemma for dalaw 38235. First part of dalawlem13 38232. (Contributed by NM, 17-Sep-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β€ (π β¨ π ) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem12 38231 | Lemma for dalaw 38235. Second part of dalawlem13 38232. (Contributed by NM, 17-Sep-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π = π β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem13 38232 | Lemma for dalaw 38235. Special case to eliminate the requirement ((π β¨ π) β¨ π ) β π in dalawlem1 38220. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ Β¬ ((π β¨ π) β¨ π ) β π β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem14 38233 | Lemma for dalaw 38235. Combine dalawlem10 38229 and dalawlem13 38232. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ Β¬ (((π β¨ π) β¨ π ) β π β§ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π ) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π))) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalawlem15 38234 | Lemma for dalaw 38235. Swap variable triples πππ and πππ in dalawlem14 38233, to obtain the elimination of the remaining conditions in dalawlem1 38220. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ Β¬ (((π β¨ π) β¨ π) β π β§ (Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π) β§ Β¬ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π))) β§ ((π β¨ π) β§ (π β¨ π)) β€ (π β¨ π)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β¨ π) β§ (π β¨ π)) β€ (((π β¨ π ) β§ (π β¨ π)) β¨ ((π β¨ π) β§ (π β¨ π)))) | ||
Theorem | dalaw 38235 | Desargues's law, derived from Desargues's theorem dath 38085 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 38236 | Extend class notation with projective subspace closure. |
class PCl | ||
Definition | df-pclN 38237* | 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 38284.) (Contributed by NM, 7-Sep-2013.) |
β’ PCl = (π β V β¦ (π₯ β π« (Atomsβπ) β¦ β© {π¦ β (PSubSpβπ) β£ π₯ β π¦})) | ||
Theorem | pclfvalN 38238* | The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ (πΎ β π β π = (π₯ β π« π΄ β¦ β© {π¦ β π β£ π₯ β π¦})) | ||
Theorem | pclvalN 38239* | Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π΄) β (πβπ) = β© {π¦ β π β£ π β π¦}) | ||
Theorem | pclclN 38240 | Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π΄) β (πβπ) β π) | ||
Theorem | elpclN 38241* | Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) & β’ π β V β β’ ((πΎ β π β§ π β π΄) β (π β (πβπ) β βπ¦ β π (π β π¦ β π β π¦))) | ||
Theorem | elpcliN 38242 | Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ (((πΎ β π β§ π β π β§ π β π) β§ π β (πβπ)) β π β π) | ||
Theorem | pclssN 38243 | Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π β§ π β π΄) β (πβπ) β (πβπ)) | ||
Theorem | pclssidN 38244 | 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 38245 | The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β π β§ π β π) β (πβπ) = π) | ||
Theorem | pclbtwnN 38246 | 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 38247 | 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 38248 | 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 38249* | 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 38299. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β AtLat β§ π β π΄) β (πβπ) = βͺ π¦ β (Fin β© π« π)(πβπ¦)) | ||
Theorem | pclcmpatN 38250* | 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 38251 | Extend class notation with polarity of projective subspace $m$. |
class β₯π | ||
Definition | df-polarityN 38252* | 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 38253* | The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ (πΎ β π΅ β π = (π β π« π΄ β¦ (π΄ β© β© π β π (πβ( β₯ βπ))))) | ||
Theorem | polvalN 38254* | Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β π΅ β§ π β π΄) β (πβπ) = (π΄ β© β© π β π (πβ( β₯ βπ)))) | ||
Theorem | polval2N 38255 | 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 38256 | 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 38257 | 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 38258 | The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ (πΎ β π΅ β ( β₯ ββ ) = π΄) | ||
Theorem | pol1N 38259 | 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 38260 | The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ β₯ = (β₯πβπΎ) β β’ (πΎ β HL β ( β₯ β( β₯ ββ )) = β ) | ||
Theorem | polpmapN 38261 | The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ π = (pmapβπΎ) & β’ π = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβ(πβπ)) = (πβ( β₯ βπ))) | ||
Theorem | 2polpmapN 38262 | Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (pmapβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΅) β ( β₯ β( β₯ β(πβπ))) = (πβπ)) | ||
Theorem | 2polvalN 38263 | Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯ βπ)) = (πβ(πβπ))) | ||
Theorem | 2polssN 38264 | 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 38265 | Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ( β₯ β( β₯ β( β₯ βπ))) = ( β₯ βπ)) | ||
Theorem | polcon3N 38266 | Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π) β ( β₯ βπ) β ( β₯ βπ)) | ||
Theorem | 2polcon4bN 38267 | Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (( β₯ β( β₯ βπ)) β ( β₯ β( β₯ βπ)) β ( β₯ βπ) β ( β₯ βπ))) | ||
Theorem | polcon2N 38268 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) | ||
Theorem | polcon2bN 38269 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β ( β₯ βπ) β π β ( β₯ βπ))) | ||
Theorem | pclss2polN 38270 | 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 38271 | The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
β’ π = (PClβπΎ) β β’ (πΎ β HL β (πββ ) = β ) | ||
Theorem | pcl0bN 38272 | The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) β β’ ((πΎ β HL β§ π β π΄) β ((πβπ) = β β π = β )) | ||
Theorem | pmaplubN 38273 | 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 38274 | 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 38275 | Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (pmapβπΎ) β β’ ((πΎ β HL β§ π β π΄) β (πβ(πβ(πβ(πβπ)))) = (πβ(πβπ))) | ||
Theorem | paddunN 38276 | 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 6842.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β(π + π)) = ( β₯ β(π βͺ π))) | ||
Theorem | poldmj1N 38277 | De Morgan's law for polarity of projective sum. (oldmj1 37569 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) | ||
Theorem | pmapj2N 38278 | 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 38279 | 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 38280 | 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 38281 | 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 38282 | 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 38283 | Extend class notation with set of all closed projective subspaces for a Hilbert lattice. |
class PSubCl | ||
Definition | df-psubclN 38284* | 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 38285* | The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ (πΎ β π΅ β πΆ = {π β£ (π β π΄ β§ ( β₯ β( β₯ βπ )) = π )}) | ||
Theorem | ispsubclN 38286 | The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ (πΎ β π· β (π β πΆ β (π β π΄ β§ ( β₯ β( β₯ βπ)) = π))) | ||
Theorem | psubcliN 38287 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β π· β§ π β πΆ) β (π β π΄ β§ ( β₯ β( β₯ βπ)) = π)) | ||
Theorem | psubcli2N 38288 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ β₯ = (β₯πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β π· β§ π β πΆ) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | psubclsubN 38289 | A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
β’ π = (PSubSpβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β πΆ) β π β π) | ||
Theorem | psubclssatN 38290 | A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β π· β§ π β πΆ) β π β π΄) | ||
Theorem | pmapidclN 38291 | Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
β’ π = (lubβπΎ) & β’ π = (pmapβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β πΆ) β (πβ(πβπ)) = π) | ||
Theorem | 0psubclN 38292 | The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ πΆ = (PSubClβπΎ) β β’ (πΎ β HL β β β πΆ) | ||
Theorem | 1psubclN 38293 | The set of all atoms is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ (πΎ β HL β π΄ β πΆ) | ||
Theorem | atpsubclN 38294 | A point (singleton of an atom) is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β π΄) β {π} β πΆ) | ||
Theorem | pmapsubclN 38295 | A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (pmapβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβπ) β πΆ) | ||
Theorem | ispsubcl2N 38296* | Alternate predicate for "is a closed projective subspace". Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π = (pmapβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ (πΎ β HL β (π β πΆ β βπ¦ β π΅ π = (πβπ¦))) | ||
Theorem | psubclinN 38297 | The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β (π β© π) β πΆ) | ||
Theorem | paddatclN 38298 | The projective sum of a closed subspace and an atom is a closed projective subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (π + {π}) β πΆ) | ||
Theorem | pclfinclN 38299 | The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 38249 and also pclcmpatN 38250. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PClβπΎ) & β’ π = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β Fin) β (πβπ) β π) | ||
Theorem | linepsubclN 38300 | A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
β’ π = (LinesβπΎ) & β’ πΆ = (PSubClβπΎ) β β’ ((πΎ β HL β§ π β π) β π β πΆ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |