![]() |
Metamath
Proof Explorer Theorem List (p. 390 of 481) | < 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-30640) |
![]() (30641-32163) |
![]() (32164-48040) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lplnle 38901* | 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 38902 | A lattice line (or atom) cannot majorize a lattice plane. (Contributed by NM, 8-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π΄ β§ π β π΄)) β Β¬ π β€ (π β¨ π )) | ||
Theorem | lplnnleat 38903 | A lattice plane cannot majorize an atom. (Contributed by NM, 14-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π΄) β Β¬ π β€ π) | ||
Theorem | lplnnlelln 38904 | 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 38905 | The join of two atoms is not a lattice plane. (Contributed by NM, 16-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β Β¬ (π β¨ π ) β π) | ||
Theorem | lplnneat 38906 | No lattice plane is an atom. (Contributed by NM, 15-Jul-2012.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π΄) | ||
Theorem | lplnnelln 38907 | No lattice plane is a lattice line. (Contributed by NM, 19-Jun-2012.) |
β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π) | ||
Theorem | lplnn0N 38908 | A lattice plane is nonzero. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
β’ 0 = (0.βπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π) β π β 0 ) | ||
Theorem | islpln2a 38909 | The predicate "is a lattice plane" for join of atoms. (Contributed by NM, 16-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (((π β¨ π ) β¨ π) β π β (π β π β§ Β¬ π β€ (π β¨ π )))) | ||
Theorem | islpln2ah 38910 | The predicate "is a lattice plane" for join of atoms. Version of islpln2a 38909 expressed with an abbreviation hypothesis. (Contributed by NM, 30-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β (π β π β (π β π β§ Β¬ π β€ (π β¨ π )))) | ||
Theorem | lplnriaN 38911 | 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 38912 | 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 | lplnric 38913 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β Β¬ π β€ (π β¨ π )) | ||
Theorem | lplnri1 38914 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β π β π ) | ||
Theorem | lplnri2N 38915 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) | ||
Theorem | lplnri3N 38916 | Property of a lattice plane expressed as the join of 3 atoms. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β π β π) | ||
Theorem | lplnllnneN 38917 | Two lattice lines defined by atoms defining a lattice plane are not equal. (Contributed by NM, 9-Oct-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = ((π β¨ π ) β¨ π) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π) β (π β¨ π) β (π β¨ π)) | ||
Theorem | llncvrlpln2 38918 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 24-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β ππΆπ) | ||
Theorem | llncvrlpln 38919 | An element covering a lattice line is a lattice plane and vice-versa. (Contributed by NM, 26-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β π β π β π)) | ||
Theorem | 2lplnmN 38920 | If the join of two lattice planes covers one of them, their meet is a lattice line. (Contributed by NM, 30-Jun-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ ππΆ(π β¨ π)) β (π β§ π) β π) | ||
Theorem | 2llnmj 38921 | The meet of two lattice lines is an atom iff their join is a lattice plane. (Contributed by NM, 27-Jun-2012.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β ((π β§ π) β π΄ β (π β¨ π) β π)) | ||
Theorem | 2atmat 38922 | The meet of two intersecting lines (expressed as joins of atoms) is an atom. (Contributed by NM, 21-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ π β€ ((π β¨ π) β¨ π ))) β ((π β¨ π) β§ (π β¨ π)) β π΄) | ||
Theorem | lplncmp 38923 | If two lattice planes are comparable, they are equal. (Contributed by NM, 24-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β (π β€ π β π = π)) | ||
Theorem | lplnexatN 38924* | Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β βπ β π΄ (Β¬ π β€ π β§ π = (π β¨ π))) | ||
Theorem | lplnexllnN 38925* | Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ π β€ π) β βπ¦ β π (Β¬ π β€ π¦ β§ π = (π¦ β¨ π))) | ||
Theorem | lplnnlt 38926 | Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012.) |
β’ < = (ltβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π < π) | ||
Theorem | 2llnjaN 38927 | The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 38928 in terms of atoms). (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((((πΎ β HL β§ π β π) β§ (π β π΄ β§ π β π΄ β§ π β π ) β§ (π β π΄ β§ π β π΄ β§ π β π)) β§ ((π β¨ π ) β€ π β§ (π β¨ π) β€ π β§ (π β¨ π ) β (π β¨ π))) β ((π β¨ π ) β¨ (π β¨ π)) = π) | ||
Theorem | 2llnjN 38928 | The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ (π β€ π β§ π β€ π β§ π β π)) β (π β¨ π) = π) | ||
Theorem | 2llnm2N 38929 | The meet of two different lattice lines in a lattice plane is an atom. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ (π β€ π β§ π β€ π β§ π β π)) β (π β§ π) β π΄) | ||
Theorem | 2llnm3N 38930 | Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ (π β€ π β§ π β€ π)) β (π β§ π) β 0 ) | ||
Theorem | 2llnm4 38931 | Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π β§ π β π) β§ (π β€ π β§ π β€ π)) β (π β§ π) β 0 ) | ||
Theorem | 2llnmeqat 38932 | An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LLinesβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π΄) β§ (π β π β§ π β€ (π β§ π))) β π = (π β§ π)) | ||
Theorem | lvolset 38933* | The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ (πΎ β π΄ β π = {π₯ β π΅ β£ βπ¦ β π π¦πΆπ₯}) | ||
Theorem | islvol 38934* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ (πΎ β π΄ β (π β π β (π β π΅ β§ βπ¦ β π π¦πΆπ))) | ||
Theorem | islvol4 38935* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β (π β π β βπ¦ β π π¦πΆπ)) | ||
Theorem | lvoli 38936 | Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β π· β§ π β π΅ β§ π β π) β§ ππΆπ) β π β π) | ||
Theorem | islvol3 38937* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ¦ β π βπ β π΄ (Β¬ π β€ π¦ β§ π = (π¦ β¨ π)))) | ||
Theorem | lvoli3 38938 | Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π΄) β§ Β¬ π β€ π) β (π β¨ π) β π) | ||
Theorem | lvolbase 38939 | A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π = (LVolsβπΎ) β β’ (π β π β π β π΅) | ||
Theorem | islvol5 38940* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π β βπ β π΄ βπ β π΄ βπ β π΄ βπ β π΄ ((π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ π = (((π β¨ π) β¨ π) β¨ π )))) | ||
Theorem | islvol2 38941* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ (πΎ β HL β (π β π β (π β π΅ β§ βπ β π΄ βπ β π΄ βπ β π΄ βπ β π΄ ((π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ π = (((π β¨ π) β¨ π) β¨ π ))))) | ||
Theorem | lvoli2 38942 | The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (((π β¨ π) β¨ π ) β¨ π) β π) | ||
Theorem | lvolnle3at 38943 | A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β HL β§ π β π) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β Β¬ π β€ ((π β¨ π) β¨ π )) | ||
Theorem | lvolnleat 38944 | An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π΄) β Β¬ π β€ π) | ||
Theorem | lvolnlelln 38945 | A lattice line cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π β€ π) | ||
Theorem | lvolnlelpln 38946 | A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π β€ π) | ||
Theorem | 3atnelvolN 38947 | The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β Β¬ ((π β¨ π) β¨ π ) β π) | ||
Theorem | 2atnelvolN 38948 | The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β Β¬ (π β¨ π) β π) | ||
Theorem | lvolneatN 38949 | No lattice volume is an atom. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π΄) | ||
Theorem | lvolnelln 38950 | No lattice volume is a lattice line. (Contributed by NM, 15-Jul-2012.) |
β’ π = (LLinesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π) | ||
Theorem | lvolnelpln 38951 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |
β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π) β Β¬ π β π) | ||
Theorem | lvoln0N 38952 | A lattice volume is nonzero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
β’ 0 = (0.βπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π) β π β 0 ) | ||
Theorem | islvol2aN 38953 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((((π β¨ π) β¨ π ) β¨ π) β π β (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π )))) | ||
Theorem | 4atlem0a 38954 | Lemma for 4at 38974. (Contributed by NM, 10-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ (Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β Β¬ π β€ ((π β¨ π) β¨ π)) | ||
Theorem | 4atlem0ae 38955 | Lemma for 4at 38974. (Contributed by NM, 10-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π )) | ||
Theorem | 4atlem0be 38956 | Lemma for 4at 38974. (Contributed by NM, 10-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β π β π ) | ||
Theorem | 4atlem3 38957 | Lemma for 4at 38974. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β ((Β¬ π β€ ((π β¨ π) β¨ π) β¨ Β¬ π β€ ((π β¨ π) β¨ π)) β¨ (Β¬ π β€ ((π β¨ π) β¨ π) β¨ Β¬ π β€ ((π β¨ π) β¨ π)))) | ||
Theorem | 4atlem3a 38958 | Lemma for 4at 38974. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (Β¬ π β€ ((π β¨ π) β¨ π) β¨ Β¬ π β€ ((π β¨ π) β¨ π) β¨ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 4atlem3b 38959 | Lemma for 4at 38974. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (Β¬ π β€ ((π β¨ π) β¨ π) β¨ Β¬ π β€ ((π β¨ π) β¨ π))) | ||
Theorem | 4atlem4a 38960 | Lemma for 4at 38974. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ ((π β¨ π ) β¨ π))) | ||
Theorem | 4atlem4b 38961 | Lemma for 4at 38974. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ ((π β¨ π ) β¨ π))) | ||
Theorem | 4atlem4c 38962 | Lemma for 4at 38974. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ ((π β¨ π) β¨ π))) | ||
Theorem | 4atlem4d 38963 | Lemma for 4at 38974. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄)) β ((π β¨ π) β¨ (π β¨ π)) = (π β¨ ((π β¨ π) β¨ π ))) | ||
Theorem | 4atlem9 38964 | Lemma for 4at 38974. Substitute π for π. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π) β¨ π )) β (π β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4atlem10a 38965 | Lemma for 4at 38974. Substitute π for π . (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (π β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4atlem10b 38966 | Lemma for 4at 38974. Substitute π for π (cont.). (Contributed by NM, 10-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ ((π β¨ π) β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β§ (π β€ ((π β¨ π) β¨ (π β¨ π)) β§ π β€ ((π β¨ π) β¨ (π β¨ π)))) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π))) | ||
Theorem | 4atlem10 38967 | Lemma for 4at 38974. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ ((π β π΄ β§ π β π΄) β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β ((π β¨ π) β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4atlem11a 38968 | Lemma for 4at 38974. Substitute π for π. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (π β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4atlem11b 38969 | Lemma for 4at 38974. Substitute π for π (cont.). (Contributed by NM, 10-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π )) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ (π β€ ((π β¨ π) β¨ (π β¨ π)) β§ π β€ ((π β¨ π) β¨ (π β¨ π)) β§ π β€ ((π β¨ π) β¨ (π β¨ π)))) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π))) | ||
Theorem | 4atlem11 38970 | Lemma for 4at 38974. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β ((π β¨ (π β¨ π)) β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4atlem12a 38971 | Lemma for 4at 38974. Substitute π for π. (Contributed by NM, 9-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β (π β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4atlem12b 38972 | Lemma for 4at 38974. Substitute π for π (cont.). (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ ((π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π )) β§ Β¬ π β€ ((π β¨ π) β¨ π)) β§ ((π β€ ((π β¨ π) β¨ (π β¨ π)) β§ π β€ ((π β¨ π) β¨ (π β¨ π))) β§ (π β€ ((π β¨ π) β¨ (π β¨ π)) β§ π β€ ((π β¨ π) β¨ (π β¨ π))))) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π))) | ||
Theorem | 4atlem12 38973 | Lemma for 4at 38974. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (((π β¨ π) β¨ (π β¨ π)) β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4at 38974 | Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 38838 and 3at 38851. (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β (((π β¨ π) β¨ (π β¨ π)) β€ ((π β¨ π) β¨ (π β¨ π)) β ((π β¨ π) β¨ (π β¨ π)) = ((π β¨ π) β¨ (π β¨ π)))) | ||
Theorem | 4at2 38975 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ Β¬ π β€ ((π β¨ π) β¨ π ))) β ((((π β¨ π) β¨ π ) β¨ π) β€ (((π β¨ π) β¨ π) β¨ π) β (((π β¨ π) β¨ π ) β¨ π) = (((π β¨ π) β¨ π) β¨ π))) | ||
Theorem | lplncvrlvol2 38976 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β HL β§ π β π β§ π β π) β§ π β€ π) β ππΆπ) | ||
Theorem | lplncvrlvol 38977 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ ππΆπ) β (π β π β π β π)) | ||
Theorem | lvolcmp 38978 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β (π β€ π β π = π)) | ||
Theorem | lvolnltN 38979 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
β’ < = (ltβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β Β¬ π < π) | ||
Theorem | 2lplnja 38980 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 38981 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = (LVolsβπΎ) β β’ ((((πΎ β HL β§ π β π) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ ((π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ (((π β¨ π) β¨ π ) β€ π β§ ((π β¨ π) β¨ π) β€ π β§ ((π β¨ π) β¨ π ) β ((π β¨ π) β¨ π))) β (((π β¨ π) β¨ π ) β¨ ((π β¨ π) β¨ π)) = π) | ||
Theorem | 2lplnj 38981 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ (π β€ π β§ π β€ π β§ π β π)) β (π β¨ π) = π) | ||
Theorem | 2lplnm2N 38982 | The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ (π β π β§ π β π β§ π β π) β§ (π β€ π β§ π β€ π β§ π β π)) β (π β§ π) β π) | ||
Theorem | 2lplnmj 38983 | The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = (LLinesβπΎ) & β’ π = (LPlanesβπΎ) & β’ π = (LVolsβπΎ) β β’ ((πΎ β HL β§ π β π β§ π β π) β ((π β§ π) β π β (π β¨ π) β π)) | ||
Theorem | dalemkehl 38984 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β πΎ β HL) | ||
Theorem | dalemkelat 38985 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β πΎ β Lat) | ||
Theorem | dalemkeop 38986 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β πΎ β OP) | ||
Theorem | dalempea 38987 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π΄) | ||
Theorem | dalemqea 38988 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π΄) | ||
Theorem | dalemrea 38989 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π΄) | ||
Theorem | dalemsea 38990 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π΄) | ||
Theorem | dalemtea 38991 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π΄) | ||
Theorem | dalemuea 38992 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π΄) | ||
Theorem | dalemyeo 38993 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π) | ||
Theorem | dalemzeo 38994 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β π β π) | ||
Theorem | dalemclpjs 38995 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β πΆ β€ (π β¨ π)) | ||
Theorem | dalemclqjt 38996 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β πΆ β€ (π β¨ π)) | ||
Theorem | dalemclrju 38997 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β πΆ β€ (π β¨ π)) | ||
Theorem | dalem-clpjq 38998 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) β β’ (π β Β¬ πΆ β€ (π β¨ π)) | ||
Theorem | dalemceb 38999 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) & β’ π΄ = (AtomsβπΎ) β β’ (π β πΆ β (BaseβπΎ)) | ||
Theorem | dalempeb 39000 | Lemma for dath 39097. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π ) β§ Β¬ πΆ β€ (π β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π))))) & β’ π΄ = (AtomsβπΎ) β β’ (π β π β (BaseβπΎ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |