Home | Metamath
Proof Explorer Theorem List (p. 379 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | hlatcon2 37801 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | 4noncolr3 37802 | A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π))) | ||
Theorem | 4noncolr2 37803 | A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 4noncolr1 37804 | A way to express 4 non-colinear atoms (rotated right 1 places). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | athgt 37805* | 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 37806* | There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (πΎ β HL β βπ β π΄ βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dimlem1 37807 | Lemma for 3dim1 37816. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((π β π β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β§ π = π) β (π β π β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π))) | ||
Theorem | 3dimlem2 37808 | Lemma for 3dim1 37816. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β§ (π β π β§ π β€ (π β¨ π ))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dimlem3a 37809 | Lemma for 3dim3 37818. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ ((π β¨ π ) β¨ π) β§ Β¬ π β€ (π β¨ π ) β§ π β€ ((π β¨ π ) β¨ π))) β Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | 3dimlem3 37810 | Lemma for 3dim1 37816. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ ((π β¨ π ) β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π ) β§ π β€ ((π β¨ π ) β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dimlem3OLDN 37811 | Lemma for 3dim1 37816. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ ((π β¨ π ) β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π ) β§ π β€ ((π β¨ π ) β¨ π))) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dimlem4a 37812 | Lemma for 3dim3 37818. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ (π β¨ π ) β§ Β¬ π β€ ((π β¨ π ) β¨ π))) β Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | 3dimlem4 37813 | Lemma for 3dim1 37816. (Contributed by NM, 25-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π ))) β§ (π β π β§ Β¬ π β€ (π β¨ π )) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dimlem4OLDN 37814 | Lemma for 3dim1 37816. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π ))) β§ (π β π β§ Β¬ π β€ (π β¨ π )) β§ Β¬ π β€ ((π β¨ π ) β¨ π)) β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) | ||
Theorem | 3dim1lem5 37815* | Lemma for 3dim1 37816. (Contributed by NM, 26-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((π’ β π΄ β§ π£ β π΄ β§ π€ β π΄) β§ (π β π’ β§ Β¬ π£ β€ (π β¨ π’) β§ Β¬ π€ β€ ((π β¨ π’) β¨ π£))) β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dim1 37816* | 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 37817* | Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β βπ β π΄ βπ β π΄ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 3dim3 37818* | Construct a new layer on top of 3 given atoms. (Contributed by NM, 27-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β βπ β π΄ Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | 2dim 37819* | Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012.) |
β’ β¨ = (joinβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ π β π΄) β βπ β π΄ βπ β π΄ (ππΆ(π β¨ π) β§ (π β¨ π)πΆ((π β¨ π) β¨ π))) | ||
Theorem | 1dimN 37820* | 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 37821 | 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 37822* | 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 37823 | 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 37824 | 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 37825 | 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 37826 | 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 37827* | 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 37828 | 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 37829 | Rearrange join of atoms in an equality. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ (π β¨ π) = (π β¨ π ))) β (π β¨ π) = (π β¨ π )) | ||
Theorem | hlatexch4 37830 | Exchange 2 atoms. (Contributed by NM, 13-May-2013.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π β π β§ (π β¨ π) = (π β¨ π))) β (π β¨ π ) = (π β¨ π)) | ||
Theorem | ps-2b 37831 | Variation of projective geometry axiom ps-2 37827. (Contributed by NM, 3-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (Β¬ π β€ (π β¨ π ) β§ π β π β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π )))) β ((π β¨ π ) β§ (π β¨ π)) β 0 ) | ||
Theorem | 3atlem1 37832 | Lemma for 3at 37839. (Contributed by NM, 22-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem2 37833 | Lemma for 3at 37839. (Contributed by NM, 22-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ (π β π β§ π β€ (π β¨ π)) β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem3 37834 | Lemma for 3at 37839. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem4 37835 | Lemma for 3at 37839. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π )) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π )) | ||
Theorem | 3atlem5 37836 | Lemma for 3at 37839. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π β§ Β¬ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem6 37837 | Lemma for 3at 37839. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π β§ π β€ (π β¨ π)) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3atlem7 37838 | Lemma for 3at 37839. (Contributed by NM, 23-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π) β§ ((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π)) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π)) | ||
Theorem | 3at 37839 | Any three non-colinear atoms in a (lattice) plane determine the plane uniquely. This is the 2-dimensional analogue of ps-1 37826 for lines and 4at 37962 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 β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ π β π)) β (((π β¨ π) β¨ π ) β€ ((π β¨ π) β¨ π) β ((π β¨ π) β¨ π ) = ((π β¨ π) β¨ π))) | ||
Syntax | clln 37840 | Extend class notation with set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice. |
class LLines | ||
Syntax | clpl 37841 | Extend class notation with set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice. |
class LPlanes | ||
Syntax | clvol 37842 | Extend class notation with set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice. |
class LVols | ||
Syntax | clines 37843 | Extend class notation with set of all projective lines for a Hilbert lattice. |
class Lines | ||
Syntax | cpointsN 37844 | Extend class notation with set of all projective points. |
class Points | ||
Syntax | cpsubsp 37845 | Extend class notation with set of all projective subspaces. |
class PSubSp | ||
Syntax | cpmap 37846 | Extend class notation with projective map. |
class pmap | ||
Definition | df-llines 37847* | Define the set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice π, in other words all elements of height 2 (or lattice dimension 2 or projective dimension 1). (Contributed by NM, 16-Jun-2012.) |
β’ LLines = (π β V β¦ {π₯ β (Baseβπ) β£ βπ β (Atomsβπ)π( β βπ)π₯}) | ||
Definition | df-lplanes 37848* | Define the set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice π, in other words all elements of height 3 (or lattice dimension 3 or projective dimension 2). (Contributed by NM, 16-Jun-2012.) |
β’ LPlanes = (π β V β¦ {π₯ β (Baseβπ) β£ βπ β (LLinesβπ)π( β βπ)π₯}) | ||
Definition | df-lvols 37849* | Define the set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice π, in other words all elements of height 4 (or lattice dimension 4 or projective dimension 3). (Contributed by NM, 1-Jul-2012.) |
β’ LVols = (π β V β¦ {π₯ β (Baseβπ) β£ βπ β (LPlanesβπ)π( β βπ)π₯}) | ||
Definition | df-lines 37850* | Define set of all projective lines for a Hilbert lattice (actually in any set at all, for simplicity). The join of two distinct atoms equals a line. Definition of lines in item 1 of [Holland95] p. 222. (Contributed by NM, 19-Sep-2011.) |
β’ Lines = (π β V β¦ {π β£ βπ β (Atomsβπ)βπ β (Atomsβπ)(π β π β§ π = {π β (Atomsβπ) β£ π(leβπ)(π(joinβπ)π)})}) | ||
Definition | df-pointsN 37851* | Define set of all projective points in a Hilbert lattice (actually in any set at all, for simplicity). A projective point is the singleton of a lattice atom. Definition 15.1 of [MaedaMaeda] p. 61. Note that item 1 in [Holland95] p. 222 defines a point as the atom itself, but this leads to a complicated subspace ordering that may be either membership or inclusion based on its arguments. (Contributed by NM, 2-Oct-2011.) |
β’ Points = (π β V β¦ {π β£ βπ β (Atomsβπ)π = {π}}) | ||
Definition | df-psubsp 37852* | Define set of all projective subspaces. Based on definition of subspace in [Holland95] p. 212. (Contributed by NM, 2-Oct-2011.) |
β’ PSubSp = (π β V β¦ {π β£ (π β (Atomsβπ) β§ βπ β π βπ β π βπ β (Atomsβπ)(π(leβπ)(π(joinβπ)π) β π β π ))}) | ||
Definition | df-pmap 37853* | Define projective map for π at π. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.) |
β’ pmap = (π β V β¦ (π β (Baseβπ) β¦ {π β (Atomsβπ) β£ π(leβπ)π})) | ||
Theorem | llnset 37854* | The set of lattice lines in a Hilbert lattice. (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (πΎ β π· β π = {π₯ β π΅ β£ βπ β π΄ ππΆπ₯}) | ||
Theorem | islln 37855* | The predicate "is a lattice line". (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (πΎ β π· β (π β π β (π β π΅ β§ βπ β π΄ ππΆπ))) | ||
Theorem | islln4 37856* | The predicate "is a lattice line". (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β π· β§ π β π΅) β (π β π β βπ β π΄ ππΆπ)) | ||
Theorem | llni 37857 | Condition implying a lattice line. (Contributed by NM, 17-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β π· β§ π β π΅ β§ π β π΄) β§ ππΆπ) β π β π) | ||
Theorem | llnbase 37858 | A lattice line is a lattice element. (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π = (LLinesβπΎ) β β’ (π β π β π β π΅) | ||
Theorem | islln3 37859* | The predicate "is a lattice line". (Contributed by NM, 17-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ β π΄ βπ β π΄ (π β π β§ π = (π β¨ π)))) | ||
Theorem | islln2 37860* | The predicate "is a lattice line". (Contributed by NM, 23-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (πΎ β HL β (π β π β (π β π΅ β§ βπ β π΄ βπ β π΄ (π β π β§ π = (π β¨ π))))) | ||
Theorem | llni2 37861 | The join of two different atoms is a lattice line. (Contributed by NM, 26-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β π) | ||
Theorem | llnnleat 37862 | An atom cannot majorize a lattice line. (Contributed by NM, 8-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π΄) β Β¬ π β€ π) | ||
Theorem | llnneat 37863 | A lattice line is not an atom. (Contributed by NM, 19-Jun-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π΄) | ||
Theorem | 2atneat 37864 | The join of two distinct atoms is not an atom. (Contributed by NM, 12-Oct-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π)) β Β¬ (π β¨ π) β π΄) | ||
Theorem | llnn0 37865 | A lattice line is nonzero. (Contributed by NM, 15-Jul-2012.) |
β’ 0 = (0.βπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π) β π β 0 ) | ||
Theorem | islln2a 37866 | The predicate "is a lattice line" in terms of atoms. (Contributed by NM, 15-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ((π β¨ π) β π β π β π)) | ||
Theorem | llnle 37867* | Any element greater than 0 and not an atom majorizes a lattice line. (Contributed by NM, 28-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π΅) β§ (π β 0 β§ Β¬ π β π΄)) β βπ¦ β π π¦ β€ π) | ||
Theorem | atcvrlln2 37868 | An atom under a line is covered by it. (Contributed by NM, 2-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π) β§ π β€ π) β ππΆπ) | ||
Theorem | atcvrlln 37869 | An element covering an atom is a lattice line and vice-versa. (Contributed by NM, 18-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β π΄ β π β π)) | ||
Theorem | llnexatN 37870* | Given an atom on a line, there is another atom whose join equals the line. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β βπ β π΄ (π β π β§ π = (π β¨ π))) | ||
Theorem | llncmp 37871 | If two lattice lines are comparable, they are equal. (Contributed by NM, 19-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β (π β€ π β π = π)) | ||
Theorem | llnnlt 37872 | Two lattice lines cannot satisfy the less than relation. (Contributed by NM, 26-Jun-2012.) |
β’ < = (ltβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π < π) | ||
Theorem | 2llnmat 37873 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ (π β π β§ (π β§ π) β 0 )) β (π β§ π) β π΄) | ||
Theorem | 2at0mat0 37874 | Special case of 2atmat0 37875 where one atom could be zero. (Contributed by NM, 30-May-2013.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ (π β π΄ β¨ π = 0 ) β§ (π β¨ π) β (π β¨ π))) β (((π β¨ π) β§ (π β¨ π)) β π΄ β¨ ((π β¨ π) β§ (π β¨ π)) = 0 )) | ||
Theorem | 2atmat0 37875 | The meet of two unequal lines (expressed as joins of atoms) is an atom or zero. (Contributed by NM, 2-Dec-2012.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ (π β¨ π) β (π β¨ π))) β (((π β¨ π) β§ (π β¨ π)) β π΄ β¨ ((π β¨ π) β§ (π β¨ π)) = 0 )) | ||
Theorem | 2atm 37876 | An atom majorized by two different atom joins (which could be atoms or lines) is equal to their intersection. (Contributed by NM, 30-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π) β§ (π β¨ π) β (π β¨ π))) β π = ((π β¨ π) β§ (π β¨ π))) | ||
Theorem | ps-2c 37877 | Variation of projective geometry axiom ps-2 37827. (Contributed by NM, 3-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ ((Β¬ π β€ (π β¨ π ) β§ π β π) β§ (π β¨ π ) β (π β¨ π) β§ (π β€ (π β¨ π) β§ π β€ (π β¨ π )))) β ((π β¨ π ) β§ (π β¨ π)) β π΄) | ||
Theorem | lplnset 37878* | The set of lattice planes in a Hilbert lattice. (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (πΎ β π΄ β π = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) | ||
Theorem | islpln 37879* | The predicate "is a lattice plane". (Contributed by NM, 16-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (πΎ β π΄ β (π β π β (π β π΅ β§ βπ¦ β π π¦πΆπ))) | ||
Theorem | islpln4 37880* | The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β (π β π β βπ¦ β π π¦πΆπ)) | ||
Theorem | lplni 37881 | Condition implying a lattice plane. (Contributed by NM, 20-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β π· β§ π β π΅ β§ π β π) β§ ππΆπ) β π β π) | ||
Theorem | islpln3 37882* | The predicate "is a lattice plane". (Contributed by NM, 17-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ¦ β π βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) | ||
Theorem | lplnbase 37883 | A lattice plane is a lattice element. (Contributed by NM, 17-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π = (LPlanesβπΎ) β β’ (π β π β π β π΅) | ||
Theorem | islpln5 37884* | The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 24-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π)))) | ||
Theorem | islpln2 37885* | The predicate "is a lattice plane" in terms of atoms. (Contributed by NM, 25-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ (πΎ β HL β (π β π β (π β π΅ β§ βπ β π΄ βπ β π΄ βπ β π΄ (π β π β§ Β¬ π β€ (π β¨ π) β§ π = ((π β¨ π) β¨ π))))) | ||
Theorem | lplni2 37886 | The join of 3 different atoms is a lattice plane. (Contributed by NM, 4-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π ))) β ((π β¨ π ) β¨ π) β π) | ||
Theorem | lvolex3N 37887* | There is an atom outside of a lattice plane i.e. a 3-dimensional lattice volume exists. (Contributed by NM, 28-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β βπ β π΄ Β¬ π β€ π) | ||
Theorem | llnmlplnN 37888 | The intersection of a line with a plane not containing it is an atom. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ (Β¬ π β€ π β§ (π β§ π) β 0 )) β (π β§ π) β π΄) | ||
Theorem | lplnle 37889* | Any element greater than 0 and not an atom and not a lattice line majorizes a lattice plane. (Contributed by NM, 28-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π΅) β§ (π β 0 β§ Β¬ π β π΄ β§ Β¬ π β π)) β βπ¦ β π π¦ β€ π) | ||
Theorem | lplnnle2at 37890 | A lattice line (or atom) cannot majorize a lattice plane. (Contributed by NM, 8-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄)) β Β¬ π β€ (π β¨ π )) | ||
Theorem | lplnnleat 37891 | A lattice plane cannot majorize an atom. (Contributed by NM, 14-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π΄) β Β¬ π β€ π) | ||
Theorem | lplnnlelln 37892 | A lattice plane is not less than or equal to a lattice line. (Contributed by NM, 14-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π β€ π) | ||
Theorem | 2atnelpln 37893 | The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β Β¬ (π β¨ π ) β π) | ||
Theorem | lplnneat 37894 | No lattice plane is an atom. (Contributed by NM, 15-Jul-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π΄) | ||
Theorem | lplnnelln 37895 | No lattice plane is a lattice line. (Contributed by NM, 19-Jun-2012.) |
β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π) | ||
Theorem | lplnn0N 37896 | A lattice plane is nonzero. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
β’ 0 = (0.βπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β π β 0 ) | ||
Theorem | islpln2a 37897 | The predicate "is a lattice plane" for join of atoms. (Contributed by NM, 16-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π ) β¨ π) β π β (π β π β§ Β¬ π β€ (π β¨ π )))) | ||
Theorem | islpln2ah 37898 | The predicate "is a lattice plane" for join of atoms. Version of islpln2a 37897 expressed with an abbreviation hypothesis. (Contributed by NM, 30-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β π β (π β π β§ Β¬ π β€ (π β¨ π )))) | ||
Theorem | lplnriaN 37899 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β Β¬ π β€ (π β¨ π)) | ||
Theorem | lplnribN 37900 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β Β¬ π β€ (π β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |