![]() |
Metamath
Proof Explorer Theorem List (p. 389 of 482) | < 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-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlexch3 38801 | A Hilbert lattice has the exchange property. (atexch 32178 analog.) (Contributed by NM, 15-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlexch4N 38802 | A Hilbert lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 15-Nov-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β§ π) = 0 ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlatexchb1 38803 | A version of hlexchb1 38794 for atoms. (Contributed by NM, 15-Nov-2011.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | hlatexchb2 38804 | A version of hlexchb2 38795 for atoms. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β (π β¨ π ) = (π β¨ π ))) | ||
Theorem | hlatexch1 38805 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π) β π β€ (π β¨ π))) | ||
Theorem | hlatexch2 38806 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π β€ (π β¨ π ) β π β€ (π β¨ π ))) | ||
Theorem | hlatmstcOLDN 38807* | An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in [Kalmbach] p. 140; also remark in [BeltramettiCassinelli] p. 98. (hatomistici 32159 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π = (lubβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (πβ{π¦ β π΄ β£ π¦ β€ π}) = π) | ||
Theorem | hlatle 38808* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 32168 analog.) (Contributed by NM, 4-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π β€ π β βπ β π΄ (π β€ π β π β€ π))) | ||
Theorem | hlateq 38809* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 32170 analog.) (Contributed by NM, 24-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (βπ β π΄ (π β€ π β π β€ π) β π = π)) | ||
Theorem | hlrelat1 38810* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 32160, with β§ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (π < π β βπ β π΄ (Β¬ π β€ π β§ π β€ π))) | ||
Theorem | hlrelat5N 38811* | An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (π < (π β¨ π) β§ π β€ π)) | ||
Theorem | hlrelat 38812* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 32161 analog.) (Contributed by NM, 4-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (π < (π β¨ π) β§ (π β¨ π) β€ π)) | ||
Theorem | hlrelat2 38813* | A consequence of relative atomicity. (chrelat2i 32162 analog.) (Contributed by NM, 5-Feb-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (Β¬ π β€ π β βπ β π΄ (π β€ π β§ Β¬ π β€ π))) | ||
Theorem | exatleN 38814 | A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) β (π β€ π β π = π)) | ||
Theorem | hl2at 38815* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β βπ β π΄ βπ β π΄ π β π) | ||
Theorem | atex 38816 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β π΄ β β ) | ||
Theorem | intnatN 38817 | If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (Β¬ π β€ π β§ (π β§ π) β π΄)) β Β¬ π β π΄) | ||
Theorem | 2llnne2N 38818 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β (π β¨ π) β (π β¨ π)) | ||
Theorem | 2llnneN 38819 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β (π β¨ π)) | ||
Theorem | cvr1 38820 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 32152 analog.) (Contributed by NM, 17-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (Β¬ π β€ π β ππΆ(π β¨ π))) | ||
Theorem | cvr2N 38821 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 32153 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β (π < (π β¨ π) β ππΆ(π β¨ π))) | ||
Theorem | hlrelat3 38822* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 38812. (Contributed by NM, 2-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π) β€ π)) | ||
Theorem | cvrval3 38823* | Binary relation expressing π covers π. (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = π))) | ||
Theorem | cvrval4N 38824* | Binary relation expressing π covers π. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β (ππΆπ β (π < π β§ βπ β π΄ (π β¨ π) = π))) | ||
Theorem | cvrval5 38825* | Binary relation expressing π covers π β§ π. (Contributed by NM, 7-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π))) | ||
Theorem | cvrp 38826 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 32172 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΄) β ((π β§ π) = 0 β ππΆ(π β¨ π))) | ||
Theorem | atcvr1 38827 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | atcvr2 38828 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β ππΆ(π β¨ π))) | ||
Theorem | cvrexchlem 38829 | Lemma for cvrexch 38830. (cvexchlem 32165 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) | ||
Theorem | cvrexch 38830 | A Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (cvexchi 32166 analog.) (Contributed by NM, 18-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β π΅) β ((π β§ π)πΆπ β ππΆ(π β¨ π))) | ||
Theorem | cvratlem 38831 | Lemma for cvrat 38832. (atcvatlem 32182 analog.) (Contributed by NM, 22-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β§ (π β 0 β§ π < (π β¨ π))) β (Β¬ π(leβπΎ)π β π β π΄)) | ||
Theorem | cvrat 38832 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 32183 analog.) (Contributed by NM, 22-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π < (π β¨ π)) β π β π΄)) | ||
Theorem | ltltncvr 38833 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ π < π) β Β¬ ππΆπ)) | ||
Theorem | ltcvrntr 38834 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π < π β§ ππΆπ) β Β¬ ππΆπ)) | ||
Theorem | cvrntr 38835 | The covers relation is not transitive. (cvntr 32089 analog.) (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β π΄ β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((ππΆπ β§ ππΆπ) β Β¬ ππΆπ)) | ||
Theorem | atcvr0eq 38836 | The covers relation is not transitive. (atcv0eq 32176 analog.) (Contributed by NM, 29-Nov-2011.) |
β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( 0 πΆ(π β¨ π) β π = π)) | ||
Theorem | lnnat 38837 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β π β Β¬ (π β¨ π) β π΄)) | ||
Theorem | atcvrj0 38838 | Two atoms covering the zero subspace are equal. (atcv1 32177 analog.) (Contributed by NM, 29-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π)) β (π = 0 β π = π)) | ||
Theorem | cvrat2 38839 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 32184 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄) β§ (π β π β§ ππΆ(π β¨ π))) β π β π΄) | ||
Theorem | atcvrneN 38840 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ππΆ(π β¨ π )) β π β π ) | ||
Theorem | atcvrj1 38841 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β ππΆ(π β¨ π )) | ||
Theorem | atcvrj2b 38842 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β ((π β π β§ π β€ (π β¨ π )) β ππΆ(π β¨ π ))) | ||
Theorem | atcvrj2 38843 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β ππΆ(π β¨ π )) | ||
Theorem | atleneN 38844 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π ))) β π β π ) | ||
Theorem | atltcvr 38845 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π < (π β¨ π ) β ππΆ(π β¨ π ))) | ||
Theorem | atle 38846* | Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ π β 0 ) β βπ β π΄ π β€ π) | ||
Theorem | atlt 38847 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π < (π β¨ π) β π β π)) | ||
Theorem | atlelt 38848 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ π < π)) β π < π) | ||
Theorem | 2atlt 38849* | Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΅) β§ π < π) β βπ β π΄ (π β π β§ π < π)) | ||
Theorem | atexchcvrN 38850 | Atom exchange property. Version of hlatexch2 38806 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΆ = ( β βπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (ππΆ(π β¨ π ) β ππΆ(π β¨ π ))) | ||
Theorem | atexchltN 38851 | Atom exchange property. Version of hlatexch2 38806 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π ) β (π < (π β¨ π ) β π < (π β¨ π ))) | ||
Theorem | cvrat3 38852 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 32193 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π)) β (π β§ (π β¨ π)) β π΄)) | ||
Theorem | cvrat4 38853* | A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 32194 analog.) (Contributed by NM, 30-Nov-2011.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) | ||
Theorem | cvrat42 38854* | Commuted version of cvrat4 38853. (Contributed by NM, 28-Jan-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΅ β§ π β π΄ β§ π β π΄)) β ((π β 0 β§ π β€ (π β¨ π)) β βπ β π΄ (π β€ π β§ π β€ (π β¨ π)))) | ||
Theorem | 2atjm 38855 | The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π)) β ((π β¨ π) β§ π) = π) | ||
Theorem | atbtwn 38856 | Property of a 3rd atom π on a line π β¨ π intersecting element π at π. (Contributed by NM, 30-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΅) β§ (π β€ π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) β (π β π β Β¬ π β€ π)) | ||
Theorem | atbtwnexOLDN 38857* | There exists a 3rd atom π on a line π β¨ π intersecting element π at π, such that π is different from π and not in π. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β€ π β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) | ||
Theorem | atbtwnex 38858* | Given atoms π in π and π not in π, there exists an atom π not in π such that the line π β¨ π intersects π at π. (Contributed by NM, 1-Aug-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΅ β§ π β€ π β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) | ||
Theorem | 3noncolr2 38859 | Two ways to express 3 non-colinear atoms (rotated right 2 places). (Contributed by NM, 12-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π ))) | ||
Theorem | 3noncolr1N 38860 | Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π))) | ||
Theorem | hlatcon3 38861 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π )) | ||
Theorem | hlatcon2 38862 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | 4noncolr3 38863 | A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π))) | ||
Theorem | 4noncolr2 38864 | A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 4noncolr1 38865 | A way to express 4 non-colinear atoms (rotated right 1 places). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | athgt 38866* | A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β βπ β π΄ βπ β π΄ (ππΆ(π β¨ π) β§ βπ β π΄ ((π β¨ π)πΆ((π β¨ π) β¨ π) β§ βπ β π΄ ((π β¨ π) β¨ π)πΆ(((π β¨ π) β¨ π) β¨ π )))) | ||
Theorem | 3dim0 38867* | There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β βπ β π΄ βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dimlem1 38868 | Lemma for 3dim1 38877. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((π β π β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β§ π = π) β (π β π β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π))) | ||
Theorem | 3dimlem2 38869 | Lemma for 3dim1 38877. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β§ (π β π β§ π β€ (π β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dimlem3a 38870 | Lemma for 3dim3 38879. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ ((π β¨ π ) β¨ π) β§ Β¬ π β€ (π β¨ π ) β§ π β€ ((π β¨ π ) β¨ π))) β Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | 3dimlem3 38871 | Lemma for 3dim1 38877. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ ((π β¨ π ) β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π ) β§ π β€ ((π β¨ π ) β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dimlem3OLDN 38872 | Lemma for 3dim1 38877. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ ((π β¨ π ) β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π ) β§ π β€ ((π β¨ π ) β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dimlem4a 38873 | Lemma for 3dim3 38879. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π))) β Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | 3dimlem4 38874 | Lemma for 3dim1 38877. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π ))) β§ (π β π β§ Β¬ π β€ (π β¨ π )) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dimlem4OLDN 38875 | Lemma for 3dim1 38877. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π ))) β§ (π β π β§ Β¬ π β€ (π β¨ π )) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dim1lem5 38876* | Lemma for 3dim1 38877. (Contributed by NM, 26-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dim1 38877* | Construct a 3-dimensional volume (height-4 element) on top of a given atom π. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dim2 38878* | Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dim3 38879* | Construct a new layer on top of 3 given atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β βπ β π΄ Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | 2dim 38880* | Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π))) | ||
Theorem | 1dimN 38881* | An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ ππΆ(π β¨ π)) | ||
Theorem | 1cvrco 38882 | The orthocomplement of an element covered by 1 is an atom. (Contributed by NM, 7-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) & β’ β₯ = (ocβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (ππΆ 1 β ( β₯ βπ) β π΄)) | ||
Theorem | 1cvratex 38883* | There exists an atom less than an element covered by 1. (Contributed by NM, 7-May-2012.) (Revised by Mario Carneiro, 13-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ < = (ltβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΅ β§ ππΆ 1 ) β βπ β π΄ π < π) | ||
Theorem | 1cvratlt 38884 | An atom less than or equal to an element covered by 1 is less than the element. (Contributed by NM, 7-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΅) β§ (ππΆ 1 β§ π β€ π)) β π < π) | ||
Theorem | 1cvrjat 38885 | An element covered by the lattice unity, when joined with an atom not under it, equals the lattice unity. (Contributed by NM, 30-Apr-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΄) β§ (ππΆ 1 β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) | ||
Theorem | 1cvrat 38886 | Create an atom under an element covered by the lattice unity. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 30-Apr-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΅) β§ (π β π β§ ππΆ 1 β§ Β¬ π β€ π)) β ((π β¨ π) β§ π) β π΄) | ||
Theorem | ps-1 38887 | The join of two atoms π β¨ π (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda] p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67. (Contributed by NM, 15-Nov-2011.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β€ (π β¨ π) β (π β¨ π) = (π β¨ π))) | ||
Theorem | ps-2 38888* | Lattice analogue for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in [MaedaMaeda] p. 68 and part of Theorem 16.4 in [MaedaMaeda] p. 69. (Contributed by NM, 1-Dec-2011.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ ((Β¬ π β€ (π β¨ π ) β§ π β π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π )))) β βπ’ β π΄ (π’ β€ (π β¨ π ) β§ π’ β€ (π β¨ π))) | ||
Theorem | 2atjlej 38889 | Two atoms are different if their join majorizes the join of two different atoms. (Contributed by NM, 4-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π΄ β§ π β π΄ β§ (π β¨ π) β€ (π β¨ π))) β π β π) | ||
Theorem | hlatexch3N 38890 | Rearrange join of atoms in an equality. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π) = (π β¨ π ))) β (π β¨ π) = (π β¨ π )) | ||
Theorem | hlatexch4 38891 | Exchange 2 atoms. (Contributed by NM, 13-May-2013.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ (π β¨ π) = (π β¨ π))) β (π β¨ π ) = (π β¨ π)) | ||
Theorem | ps-2b 38892 | Variation of projective geometry axiom ps-2 38888. (Contributed by NM, 3-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π ) β§ π β π β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π )))) β ((π β¨ π ) β§ (π β¨ π)) β 0 ) | ||
Theorem | 3atlem1 38893 | Lemma for 3at 38900. (Contributed by NM, 22-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem2 38894 | Lemma for 3at 38900. (Contributed by NM, 22-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ (π β π β§ π β€ (π β¨ π)) β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem3 38895 | Lemma for 3at 38900. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem4 38896 | Lemma for 3at 38900. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π )) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π )) | ||
Theorem | 3atlem5 38897 | Lemma for 3at 38900. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem6 38898 | Lemma for 3at 38900. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π β§ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem7 38899 | Lemma for 3at 38900. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3at 38900 | Any three non-colinear atoms in a (lattice) plane determine the plane uniquely. This is the 2-dimensional analogue of ps-1 38887 for lines and 4at 39023 for volumes. I could not find this proof in the literature on projective geometry (where it is either given as an axiom or stated as an unproved fact), but it is similar to Theorem 15 of Veblen, "The Foundations of Geometry" (1911), p. 18, which uses different axioms. This proof was written before I became aware of Veblen's, and it is possible that a shorter proof could be obtained by using Veblen's proof for hints. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π)) β (((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |