Home | Metamath
Proof Explorer Theorem List (p. 386 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ltrncoelN 38501 | Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 38497 uses. (Contributed by NM, 1-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβ(πΊβπ)) β π΄ β§ Β¬ (πΉβ(πΊβπ)) β€ π)) | ||
Theorem | ltrncoat 38502 | Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 38497, ltrnat 38498 uses. (Contributed by NM, 1-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) | ||
Theorem | ltrncoval 38503 | Two ways to express value of translation composition. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) | ||
Theorem | ltrncnv 38504 | The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) | ||
Theorem | ltrn11at 38505 | Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ π β π΄ β§ π β π)) β (πΉβπ) β (πΉβπ)) | ||
Theorem | ltrneq2 38506* | The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (βπ β π΄ (πΉβπ) = (πΊβπ) β πΉ = πΊ)) | ||
Theorem | ltrneq 38507* | The equality of two translations is determined by their equality at atoms not under co-atom π. (Contributed by NM, 20-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (βπ β π΄ (Β¬ π β€ π β (πΉβπ) = (πΊβπ)) β πΉ = πΊ)) | ||
Theorem | idltrn 38508 | The identity function is a lattice translation. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 18-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β ( I βΎ π΅) β π) | ||
Theorem | ltrnmw 38509 | Property of lattice translation value. Remark below Lemma B in [Crawley] p. 112. TODO: Can this be used in more places? (Contributed by NM, 20-May-2012.) (Proof shortened by OpenAI, 25-Mar-2020.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β§ π) = 0 ) | ||
Theorem | dilfsetN 38510* | The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) β β’ (πΎ β π΅ β πΏ = (π β π΄ β¦ {π β π β£ βπ₯ β π (π₯ β (πβπ) β (πβπ₯) = π₯)})) | ||
Theorem | dilsetN 38511* | The set of dilations for a fiducial atom π·. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΏβπ·) = {π β π β£ βπ₯ β π (π₯ β (πβπ·) β (πβπ₯) = π₯)}) | ||
Theorem | isdilN 38512* | The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πΏβπ·) β (πΉ β π β§ βπ₯ β π (π₯ β (πβπ·) β (πΉβπ₯) = π₯)))) | ||
Theorem | trnfsetN 38513* | The mapping from fiducial atom to set of translations. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) & β’ π = (TrnβπΎ) β β’ (πΎ β πΆ β π = (π β π΄ β¦ {π β (πΏβπ) β£ βπ β (πβπ)βπ β (πβπ)((π + (πβπ)) β© ( β₯ β{π})) = ((π + (πβπ)) β© ( β₯ β{π}))})) | ||
Theorem | trnsetN 38514* | The set of translations for a fiducial atom π·. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) & β’ π = (TrnβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πβπ·) = {π β (πΏβπ·) β£ βπ β (πβπ·)βπ β (πβπ·)((π + (πβπ)) β© ( β₯ β{π·})) = ((π + (πβπ)) β© ( β₯ β{π·}))}) | ||
Theorem | istrnN 38515* | The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) & β’ π = (TrnβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πβπ·) β (πΉ β (πΏβπ·) β§ βπ β (πβπ·)βπ β (πβπ·)((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·}))))) | ||
Syntax | ctrl 38516 | Extend class notation with set of all traces of lattice translations. |
class trL | ||
Definition | df-trl 38517* | Define trace of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ trL = (π β V β¦ (π€ β (LHypβπ) β¦ (π β ((LTrnβπ)βπ€) β¦ (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)))))) | ||
Theorem | trlfset 38518* | The set of all traces of lattice translations for a lattice πΎ. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β πΆ β (trLβπΎ) = (π€ β π» β¦ (π β ((LTrnβπΎ)βπ€) β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π€ β π₯ = ((π β¨ (πβπ)) β§ π€)))))) | ||
Theorem | trlset 38519* | The set of traces of lattice translations for a fiducial co-atom π. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β πΆ β§ π β π») β π = (π β π β¦ (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πβπ)) β§ π))))) | ||
Theorem | trlval 38520* | The value of the trace of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π) β (π βπΉ) = (β©π₯ β π΅ βπ β π΄ (Β¬ π β€ π β π₯ = ((π β¨ (πΉβπ)) β§ π)))) | ||
Theorem | trlval2 38521 | The value of the trace of a lattice translation, given any atom π not under the fiducial co-atom π. Note: this requires only the weaker assumption πΎ β Lat; we use πΎ β HL for convenience. (Contributed by NM, 20-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π βπΉ) = ((π β¨ (πΉβπ)) β§ π)) | ||
Theorem | trlcl 38522 | Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π βπΉ) β π΅) | ||
Theorem | trlcnv 38523 | The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π ββ‘πΉ) = (π βπΉ)) | ||
Theorem | trljat1 38524 | The value of a translation of an atom π not under the fiducial co-atom π, joined with trace. Equation above Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 38222? (Contributed by NM, 22-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π βπΉ)) = (π β¨ (πΉβπ))) | ||
Theorem | trljat2 38525 | The value of a translation of an atom π not under the fiducial co-atom π, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β¨ (π βπΉ)) = (π β¨ (πΉβπ))) | ||
Theorem | trljat3 38526 | The value of a translation of an atom π not under the fiducial co-atom π, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 22-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π βπΉ)) = ((πΉβπ) β¨ (π βπΉ))) | ||
Theorem | trlat 38527 | If an atom differs from its translation, the trace is an atom. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) β π)) β (π βπΉ) β π΄) | ||
Theorem | trl0 38528 | If an atom not under the fiducial co-atom π equals its lattice translation, the trace of the translation is zero. (Contributed by NM, 24-May-2012.) |
β’ β€ = (leβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) = π)) β (π βπΉ) = 0 ) | ||
Theorem | trlator0 38529 | The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013.) |
β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π βπΉ) β π΄ β¨ (π βπΉ) = 0 )) | ||
Theorem | trlatn0 38530 | The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-2013.) |
β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β ((π βπΉ) β π΄ β (π βπΉ) β 0 )) | ||
Theorem | trlnidat 38531 | The trace of a lattice translation other than the identity is an atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β (π βπΉ) β π΄) | ||
Theorem | ltrnnidn 38532 | If a lattice translation is not the identity, then the translation of any atom not under the fiducial co-atom π is different from the atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 24-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β π) | ||
Theorem | ltrnideq 38533 | Property of the identity lattice translation. (Contributed by NM, 27-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) | ||
Theorem | trlid0 38534 | The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (π β( I βΎ π΅)) = 0 ) | ||
Theorem | trlnidatb 38535 | A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 38531? Why do both this and ltrnideq 38533 need trlnidat 38531? (Contributed by NM, 4-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ β ( I βΎ π΅) β (π βπΉ) β π΄)) | ||
Theorem | trlid0b 38536 | A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ = ( I βΎ π΅) β (π βπΉ) = 0 )) | ||
Theorem | trlnid 38537 | Different translations with the same trace cannot be the identity. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (πΉ β πΊ β§ (π βπΉ) = (π βπΊ))) β πΉ β ( I βΎ π΅)) | ||
Theorem | ltrn2ateq 38538 | Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ) = π β (πΉβπ) = π)) | ||
Theorem | ltrnateq 38539 | If any atom (under π) is not equal to its translation, so is any other atom. (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = π) | ||
Theorem | ltrnatneq 38540 | If any atom (under π) is not equal to its translation, so is any other atom. TODO: Β¬ π β€ π isn't needed to prove this. Will removing it shorten (and not lengthen) proofs using it? (Contributed by NM, 6-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) β π) β (πΉβπ) β π) | ||
Theorem | ltrnatlw 38541 | If the value of an atom equals the atom in a non-identity translation, the atom is under the fiducial hyperplane. (Contributed by NM, 15-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((πΉβπ) β π β§ (πΉβπ) = π)) β π β€ π) | ||
Theorem | trlle 38542 | The trace of a lattice translation is less than the fiducial co-atom π. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π βπΉ) β€ π) | ||
Theorem | trlne 38543 | The trace of a lattice translation is not equal to any atom not under the fiducial co-atom π. Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β π β (π βπΉ)) | ||
Theorem | trlnle 38544 | The atom not under the fiducial co-atom π is not less than the trace of a lattice translation. Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β Β¬ π β€ (π βπΉ)) | ||
Theorem | trlval3 38545 | The value of the trace of a lattice translation in terms of 2 atoms. TODO: Try to shorten proof. (Contributed by NM, 3-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (πΉβπ)) β (π β¨ (πΉβπ)))) β (π βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) | ||
Theorem | trlval4 38546 | The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-May-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ (π βπΉ) β€ (π β¨ π))) β (π βπΉ) = ((π β¨ (πΉβπ)) β§ (π β¨ (πΉβπ)))) | ||
Theorem | trlval5 38547 | The value of the trace of a lattice translation in terms of itself. (Contributed by NM, 19-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π βπΉ) = ((π β¨ (π βπΉ)) β§ π)) | ||
Theorem | arglem1N 38548 | Lemma for Desargues's law. Theorem 13.3 of [Crawley] p. 110, third and fourth lines from bottom. In these lemmas, π, π, π , π, π, π, πΆ, π·, πΈ, πΉ, and πΊ represent Crawley's a0, a1, a2, b0, b1, b2, c, z0, z1, z2, and p respectively. (Contributed by NM, 28-Jun-2012.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΉ = ((π β¨ π) β§ (π β¨ π)) & β’ πΊ = ((π β¨ π) β§ (π β¨ π)) β β’ ((((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π) β§ (π β π β§ π β π β§ π β π)) β§ πΊ β π΄) β πΉ β π΄) | ||
Theorem | cdlemc1 38549 | Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 38222? (Contributed by NM, 29-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((π β¨ π) β§ π)) = (π β¨ π)) | ||
Theorem | cdlemc2 38550 | Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β (πΉβπ) β€ ((πΉβπ) β¨ ((π β¨ π) β§ π))) | ||
Theorem | cdlemc3 38551 | Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ) β€ (π β¨ (π βπΉ)) β π β€ (π β¨ (πΉβπ)))) | ||
Theorem | cdlemc4 38552 | Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ (πΉβπ))) β (π β¨ (π βπΉ)) β ((πΉβπ) β¨ ((π β¨ π) β§ π))) | ||
Theorem | cdlemc5 38553 | Lemma for cdlemc 38555. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ (πΉβπ)) β§ (πΉβπ) β π)) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc6 38554 | Lemma for cdlemc 38555. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc 38555 | Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ (πΉβπ))) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemd1 38556 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)))) β π = ((π β¨ ((π β¨ π ) β§ π)) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemd2 38557 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd3 38558 | Part of proof of Lemma D in [Crawley] p. 113. The π β π requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π) β§ π β π)) β§ (π β π΄ β§ π β π΄ β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdlemd4 38559 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π) β§ π β π)) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd5 38560 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd6 38561 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ Β¬ π β€ (π β¨ (πΉβπ))) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ) = (πΊβπ)) | ||
Theorem | cdlemd7 38562 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = (πΊβπ) β§ Β¬ π β€ (π β¨ (πΉβπ)))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd8 38563 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = π)) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd9 38564 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd 38565 | If two translations agree at any atom not under the fiducial co-atom π, then they are equal. Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β πΉ = πΊ) | ||
Theorem | ltrneq3 38566 | Two translations agree at any atom not under the fiducial co-atom π iff they are equal. (Contributed by NM, 25-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) = (πΊβπ) β πΉ = πΊ)) | ||
Theorem | cdleme00a 38567 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β π β π) | ||
Theorem | cdleme0aa 38568 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄ β§ π β π΄) β π β π΅) | ||
Theorem | cdleme0a 38569 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | ||
Theorem | cdleme0b 38570 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β π β π) | ||
Theorem | cdleme0c 38571 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π ) | ||
Theorem | cdleme0cp 38572 | Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 38955- swap consequent equality; make antecedent use df-3an 1089. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄)) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme0cq 38573 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme0dN 38574 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π )) β π β π΄) | ||
Theorem | cdleme0e 38575 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme0fN 38576 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π΄)) β π β π) | ||
Theorem | cdleme0gN 38577 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π) | ||
Theorem | cdlemeulpq 38578 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) | ||
Theorem | cdleme01N 38579 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β π β§ π β π β§ π β€ (π β¨ π)) β§ π β€ π)) | ||
Theorem | cdleme02N 38580 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β ((π β¨ π) = (π β¨ π) β§ π β€ π)) | ||
Theorem | cdleme0ex1N 38581* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ π β π) β βπ’ β π΄ (π’ β€ (π β¨ π) β§ π’ β€ π)) | ||
Theorem | cdleme0ex2N 38582* | Part of proof of Lemma E in [Crawley] p. 113. Note that (π β¨ π’) = (π β¨ π’) is a shorter way to express π’ β π β§ π’ β π β§ π’ β€ (π β¨ π). (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β βπ’ β π΄ ((π β¨ π’) = (π β¨ π’) β§ π’ β€ π)) | ||
Theorem | cdleme0moN 38583* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ β*π(π β π΄ β§ (π β¨ π) = (π β¨ π)))) β (π = π β¨ π = π)) | ||
Theorem | cdleme1b 38584 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma showing πΉ is a lattice element. πΉ represents their f(r). (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β πΉ β π΅) | ||
Theorem | cdleme1 38585 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents their f(r). Here we show r β¨ f(r) = r β¨ u (7th through 5th lines from bottom on p. 113). (Contributed by NM, 4-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ πΉ) = (π β¨ π)) | ||
Theorem | cdleme2 38586 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents f(r). π is the fiducial co-atom (hyperplane) w. Here we show that (r β¨ f(r)) β§ w = u in their notation (4th line from bottom on p. 113). (Contributed by NM, 5-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β ((π β¨ πΉ) β§ π) = π) | ||
Theorem | cdleme3b 38587 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π))) β πΉ β π ) | ||
Theorem | cdleme3c 38588 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ 0 = (0.βπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π))) β πΉ β 0 ) | ||
Theorem | cdleme3d 38589 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ πΉ = ((π β¨ π) β§ (π β¨ π)) | ||
Theorem | cdleme3e 38590 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ (π β¨ π)))) β π β π΄) | ||
Theorem | cdleme3fN 38591 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. TODO: Delete - duplicates cdleme0e 38575. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme3g 38592 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) | ||
Theorem | cdleme3h 38593 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38594 and cdleme3 38595. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) | ||
Theorem | cdleme3fa 38594 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 38595. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) | ||
Theorem | cdleme3 38595 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents f(r). π is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 38594 above, we show that f(r) β W (4th line from bottom on p. 113), meaning it is an atom and not under w, which in our notation is expressed as πΉ β π΄ β§ Β¬ πΉ β€ π. Their proof provides no details of our lemmas cdleme3b 38587 through cdleme3 38595, so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ πΉ β€ π) | ||
Theorem | cdleme4 38596 | Part of proof of Lemma E in [Crawley] p. 113. πΉ and πΊ represent f(s) and fs(r). Here show p β¨ q = r β¨ u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme4a 38597 | Part of proof of Lemma E in [Crawley] p. 114 top. πΊ represents fs(r). Auxiliary lemma derived from cdleme5 38598. We show fs(r) β€ p β¨ q. (Contributed by NM, 10-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π΄) β πΊ β€ (π β¨ π)) | ||
Theorem | cdleme5 38598 | Part of proof of Lemma E in [Crawley] p. 113. πΊ represents fs(r). We show r β¨ fs(r)) = p β¨ q at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β (π β¨ πΊ) = (π β¨ π)) | ||
Theorem | cdleme6 38599 | Part of proof of Lemma E in [Crawley] p. 113. This expresses (r β¨ fs(r)) β§ w = u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ π))) β ((π β¨ πΊ) β§ π) = π) | ||
Theorem | cdleme7aa 38600 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38606 and cdleme7 38607. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |