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-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dilfsetN 38501* | 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 38502* | 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 38503* | The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πΏβπ·) β (πΉ β π β§ βπ₯ β π (π₯ β (πβπ·) β (πΉβπ₯) = π₯)))) | ||
Theorem | trnfsetN 38504* | 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 38505* | 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 38506* | The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) & β’ π = (TrnβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πβπ·) β (πΉ β (πΏβπ·) β§ βπ β (πβπ·)βπ β (πβπ·)((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·}))))) | ||
Syntax | ctrl 38507 | Extend class notation with set of all traces of lattice translations. |
class trL | ||
Definition | df-trl 38508* | Define trace of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ trL = (π β V β¦ (π€ β (LHypβπ) β¦ (π β ((LTrnβπ)βπ€) β¦ (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)))))) | ||
Theorem | trlfset 38509* | 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 38510* | 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 38511* | 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 38512 | 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 38513 | Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π βπΉ) β π΅) | ||
Theorem | trlcnv 38514 | The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π ββ‘πΉ) = (π βπΉ)) | ||
Theorem | trljat1 38515 | 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 38213? (Contributed by NM, 22-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π βπΉ)) = (π β¨ (πΉβπ))) | ||
Theorem | trljat2 38516 | 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 38517 | 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 38518 | 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 38519 | 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 38520 | 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 38521 | 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 38522 | 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 38523 | 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 38524 | Property of the identity lattice translation. (Contributed by NM, 27-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) | ||
Theorem | trlid0 38525 | The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (π β( I βΎ π΅)) = 0 ) | ||
Theorem | trlnidatb 38526 | A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 38522? Why do both this and ltrnideq 38524 need trlnidat 38522? (Contributed by NM, 4-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ β ( I βΎ π΅) β (π βπΉ) β π΄)) | ||
Theorem | trlid0b 38527 | 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 38528 | Different translations with the same trace cannot be the identity. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (πΉ β πΊ β§ (π βπΉ) = (π βπΊ))) β πΉ β ( I βΎ π΅)) | ||
Theorem | ltrn2ateq 38529 | Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ) = π β (πΉβπ) = π)) | ||
Theorem | ltrnateq 38530 | 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 38531 | 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 38532 | 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 38533 | 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 38534 | 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 38535 | 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 38536 | 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 38537 | 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 38538 | 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 38539 | 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 38540 | Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 38213? (Contributed by NM, 29-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((π β¨ π) β§ π)) = (π β¨ π)) | ||
Theorem | cdlemc2 38541 | 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 38542 | 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 38543 | 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 38544 | Lemma for cdlemc 38546. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ (πΉβπ)) β§ (πΉβπ) β π)) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc6 38545 | Lemma for cdlemc 38546. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc 38546 | Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ (πΉβπ))) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemd1 38547 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)))) β π = ((π β¨ ((π β¨ π ) β§ π)) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemd2 38548 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd3 38549 | 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 38550 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π) β§ π β π)) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd5 38551 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd6 38552 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ Β¬ π β€ (π β¨ (πΉβπ))) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ) = (πΊβπ)) | ||
Theorem | cdlemd7 38553 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = (πΊβπ) β§ Β¬ π β€ (π β¨ (πΉβπ)))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd8 38554 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = π)) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd9 38555 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd 38556 | 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 38557 | 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 38558 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((πΎ β HL β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ Β¬ π β€ (π β¨ π)) β π β π) | ||
Theorem | cdleme0aa 38559 | 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 38560 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | ||
Theorem | cdleme0b 38561 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β π β π) | ||
Theorem | cdleme0c 38562 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄) β§ (π β π΄ β§ Β¬ π β€ π)) β π β π ) | ||
Theorem | cdleme0cp 38563 | Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 38946- swap consequent equality; make antecedent use df-3an 1090. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄)) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme0cq 38564 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdleme0dN 38565 | 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 38566 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme0fN 38567 | 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 38568 | 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 38569 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄)) β π β€ (π β¨ π)) | ||
Theorem | cdleme01N 38570 | 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 38571 | 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 38572* | 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 38573* | 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 38574* | 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 38575 | 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 38576 | 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 38577 | 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 38578 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π))) β πΉ β π ) | ||
Theorem | cdleme3c 38579 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ 0 = (0.βπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π))) β πΉ β 0 ) | ||
Theorem | cdleme3d 38580 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ πΉ = ((π β¨ π) β§ (π β¨ π)) | ||
Theorem | cdleme3e 38581 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ (π β¨ π)))) β π β π΄) | ||
Theorem | cdleme3fN 38582 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. TODO: Delete - duplicates cdleme0e 38566. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme3g 38583 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π) | ||
Theorem | cdleme3h 38584 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 38585 and cdleme3 38586. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) & β’ π = ((π β¨ π ) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) | ||
Theorem | cdleme3fa 38585 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 38586. (Contributed by NM, 6-Oct-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π ) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) | ||
Theorem | cdleme3 38586 | Part of proof of Lemma E in [Crawley] p. 113. πΉ represents f(r). π is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 38585 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 38578 through cdleme3 38586, 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 38587 | 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 38588 | Part of proof of Lemma E in [Crawley] p. 114 top. πΊ represents fs(r). Auxiliary lemma derived from cdleme5 38589. We show fs(r) β€ p β¨ q. (Contributed by NM, 10-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ π β π΄) β πΊ β€ (π β¨ π)) | ||
Theorem | cdleme5 38589 | 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 38590 | 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 38591 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38597 and cdleme7 38598. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) | ||
Theorem | cdleme7a 38592 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38597 and cdleme7 38598. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ πΊ = ((π β¨ π) β§ (πΉ β¨ π)) | ||
Theorem | cdleme7b 38593 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38597 and cdleme7 38598. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π) β§ π β€ (π β¨ π))) β π β π΄) | ||
Theorem | cdleme7c 38594 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38597 and cdleme7 38598. (Contributed by NM, 7-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π) | ||
Theorem | cdleme7d 38595 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38597 and cdleme7 38598. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π) | ||
Theorem | cdleme7e 38596 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 38597 and cdleme7 38598. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β (0.βπΎ)) | ||
Theorem | cdleme7ga 38597 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 38598. (Contributed by NM, 8-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π΄) | ||
Theorem | cdleme7 38598 | Part of proof of Lemma E in [Crawley] p. 113. πΊ and πΉ represent fs(r) and f(s) respectively. π is the fiducial co-atom (hyperplane) that they call w. Here and in cdleme7ga 38597 above, we show that fs(r) β W (top of p. 114), meaning it is an atom and not under w, which in our notation is expressed as πΊ β π΄ β§ Β¬ πΊ β€ π. (Note that we do not have a symbol for their W.) Their proof provides no details of our cdleme7aa 38591 through cdleme7 38598, so there may be a simpler proof that we have overlooked. (Contributed by NM, 9-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) & β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π β¨ π) β§ π))) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ πΊ β€ π) | ||
Theorem | cdleme8 38599 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. πΆ represents s1. In their notation, we prove p β¨ s1 = p β¨ s. (Contributed by NM, 9-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β (π β¨ πΆ) = (π β¨ π)) | ||
Theorem | cdleme9a 38600 | Part of proof of Lemma E in [Crawley] p. 113. πΆ represents s1, which we prove is an atom. (Contributed by NM, 10-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΆ = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β πΆ β π΄) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |