![]() |
Metamath
Proof Explorer Theorem List (p. 396 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30702) |
![]() (30703-32225) |
![]() (32226-48151) |
Type | Label | Description |
---|---|---|
Statement | ||
Definition | df-ldil 39501* | Define set of all lattice dilations. Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
β’ LDil = (π β V β¦ (π€ β (LHypβπ) β¦ {π β (LAutβπ) β£ βπ₯ β (Baseβπ)(π₯(leβπ)π€ β (πβπ₯) = π₯)})) | ||
Definition | df-ltrn 39502* | Define set of all lattice translations. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
β’ LTrn = (π β V β¦ (π€ β (LHypβπ) β¦ {π β ((LDilβπ)βπ€) β£ βπ β (Atomsβπ)βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ Β¬ π(leβπ)π€) β ((π(joinβπ)(πβπ))(meetβπ)π€) = ((π(joinβπ)(πβπ))(meetβπ)π€))})) | ||
Definition | df-dilN 39503* | Define set of all dilations. Definition of dilation in [Crawley] p. 111. (Contributed by NM, 30-Jan-2012.) |
β’ Dil = (π β V β¦ (π β (Atomsβπ) β¦ {π β (PAutβπ) β£ βπ₯ β (PSubSpβπ)(π₯ β ((WAtomsβπ)βπ) β (πβπ₯) = π₯)})) | ||
Definition | df-trnN 39504* | Define set of all translations. Definition of translation in [Crawley] p. 111. (Contributed by NM, 4-Feb-2012.) |
β’ Trn = (π β V β¦ (π β (Atomsβπ) β¦ {π β ((Dilβπ)βπ) β£ βπ β ((WAtomsβπ)βπ)βπ β ((WAtomsβπ)βπ)((π(+πβπ)(πβπ)) β© ((β₯πβπ)β{π})) = ((π(+πβπ)(πβπ)) β© ((β₯πβπ)β{π}))})) | ||
Theorem | ldilfset 39505* | The mapping from fiducial co-atom π€ to its set of lattice dilations. (Contributed by NM, 11-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = (LAutβπΎ) β β’ (πΎ β πΆ β (LDilβπΎ) = (π€ β π» β¦ {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π€ β (πβπ₯) = π₯)})) | ||
Theorem | ldilset 39506* | The set of lattice dilations for a fiducial co-atom π. (Contributed by NM, 11-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = (LAutβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ ((πΎ β πΆ β§ π β π») β π· = {π β πΌ β£ βπ₯ β π΅ (π₯ β€ π β (πβπ₯) = π₯)}) | ||
Theorem | isldil 39507* | The predicate "is a lattice dilation". Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = (LAutβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ ((πΎ β πΆ β§ π β π») β (πΉ β π· β (πΉ β πΌ β§ βπ₯ β π΅ (π₯ β€ π β (πΉβπ₯) = π₯)))) | ||
Theorem | ldillaut 39508 | A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012.) |
β’ π» = (LHypβπΎ) & β’ πΌ = (LAutβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π·) β πΉ β πΌ) | ||
Theorem | ldil1o 39509 | A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π·) β πΉ:π΅β1-1-ontoβπ΅) | ||
Theorem | ldilval 39510 | Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π· β§ (π β π΅ β§ π β€ π)) β (πΉβπ) = π) | ||
Theorem | idldil 39511 | The identity function is a lattice dilation. (Contributed by NM, 18-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ ((πΎ β π΄ β§ π β π») β ( I βΎ π΅) β π·) | ||
Theorem | ldilcnv 39512 | The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π·) β β‘πΉ β π·) | ||
Theorem | ldilco 39513 | The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π· β§ πΊ β π·) β (πΉ β πΊ) β π·) | ||
Theorem | ltrnfset 39514* | The set of all lattice translations for a lattice πΎ. (Contributed by NM, 11-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β πΆ β (LTrnβπΎ) = (π€ β π» β¦ {π β ((LDilβπΎ)βπ€) β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π€ β§ Β¬ π β€ π€) β ((π β¨ (πβπ)) β§ π€) = ((π β¨ (πβπ)) β§ π€))})) | ||
Theorem | ltrnset 39515* | The set of lattice translations for a fiducial co-atom π. (Contributed by NM, 11-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((πΎ β π΅ β§ π β π») β π = {π β π· β£ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πβπ)) β§ π) = ((π β¨ (πβπ)) β§ π))}) | ||
Theorem | isltrn 39516* | The predicate "is a lattice translation". Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((πΎ β π΅ β§ π β π») β (πΉ β π β (πΉ β π· β§ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))))) | ||
Theorem | isltrn2N 39517* | The predicate "is a lattice translation". Version of isltrn 39516 that considers only different π and π. TODO: Can this eliminate some separate proofs for the π = π case? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((πΎ β π΅ β§ π β π») β (πΉ β π β (πΉ β π· β§ βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π β§ π β π) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π))))) | ||
Theorem | ltrnu 39518 | Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom π. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 20-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β π β§ π β π») β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΉβπ)) β§ π) = ((π β¨ (πΉβπ)) β§ π)) | ||
Theorem | ltrnldil 39519 | A lattice translation is a lattice dilation. (Contributed by NM, 20-May-2012.) |
β’ π» = (LHypβπΎ) & β’ π· = ((LDilβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π) β πΉ β π·) | ||
Theorem | ltrnlaut 39520 | A lattice translation is a lattice automorphism. (Contributed by NM, 20-May-2012.) |
β’ π» = (LHypβπΎ) & β’ πΌ = (LAutβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π) β πΉ β πΌ) | ||
Theorem | ltrn1o 39521 | A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π) β πΉ:π΅β1-1-ontoβπ΅) | ||
Theorem | ltrncl 39522 | Closure of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π β§ π β π΅) β (πΉβπ) β π΅) | ||
Theorem | ltrn11 39523 | One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β π΅)) β ((πΉβπ) = (πΉβπ) β π = π)) | ||
Theorem | ltrncnvnid 39524 | If a translation is different from the identity, so is its converse. (Contributed by NM, 17-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β β‘πΉ β ( I βΎ π΅)) | ||
Theorem | ltrncoidN 39525 | Two translations are equal if the composition of one with the converse of the other is the zero translation. This is an analogue of vector subtraction. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β ((πΉ β β‘πΊ) = ( I βΎ π΅) β πΉ = πΊ)) | ||
Theorem | ltrnle 39526 | Less-than or equal property of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β π΅)) β (π β€ π β (πΉβπ) β€ (πΉβπ))) | ||
Theorem | ltrncnvleN 39527 | Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β π΅)) β (π β€ π β (β‘πΉβπ) β€ (β‘πΉβπ))) | ||
Theorem | ltrnm 39528 | Lattice translation of a meet. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β π΅)) β (πΉβ(π β§ π)) = ((πΉβπ) β§ (πΉβπ))) | ||
Theorem | ltrnj 39529 | Lattice translation of a meet. TODO: change antecedent to πΎ β HL (Contributed by NM, 25-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β π΅)) β (πΉβ(π β¨ π)) = ((πΉβπ) β¨ (πΉβπ))) | ||
Theorem | ltrncvr 39530 | Covering property of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β π΅)) β (ππΆπ β (πΉβπ)πΆ(πΉβπ))) | ||
Theorem | ltrnval1 39531 | Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ πΉ β π β§ (π β π΅ β§ π β€ π)) β (πΉβπ) = π) | ||
Theorem | ltrnid 39532* | A lattice translation is the identity function iff all atoms not under the fiducial co-atom π are equal to their values. (Contributed by NM, 24-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (βπ β π΄ (Β¬ π β€ π β (πΉβπ) = π) β πΉ = ( I βΎ π΅))) | ||
Theorem | ltrnnid 39533* | If a lattice translation is not the identity, then there is an atom not under the fiducial co-atom π and not equal to its translation. (Contributed by NM, 24-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΉ β ( I βΎ π΅)) β βπ β π΄ (Β¬ π β€ π β§ (πΉβπ) β π)) | ||
Theorem | ltrnatb 39534 | The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΅) β (π β π΄ β (πΉβπ) β π΄)) | ||
Theorem | ltrncnvatb 39535 | The converse of the lattice translation of an atom is an atom. (Contributed by NM, 2-Jun-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΅) β (π β π΄ β (β‘πΉβπ) β π΄)) | ||
Theorem | ltrnel 39536 | The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 22-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) | ||
Theorem | ltrnat 39537 | The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 39536 uses. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (πΉβπ) β π΄) | ||
Theorem | ltrncnvat 39538 | The converse of the lattice translation of an atom is an atom. (Contributed by NM, 9-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π΄) β (β‘πΉβπ) β π΄) | ||
Theorem | ltrncnvel 39539 | The converse of the lattice translation of an atom not under the fiducial co-atom. (Contributed by NM, 10-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((β‘πΉβπ) β π΄ β§ Β¬ (β‘πΉβπ) β€ π)) | ||
Theorem | ltrncoelN 39540 | Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 39536 uses. (Contributed by NM, 1-May-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβ(πΊβπ)) β π΄ β§ Β¬ (πΉβ(πΊβπ)) β€ π)) | ||
Theorem | ltrncoat 39541 | Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 39536, ltrnat 39537 uses. (Contributed by NM, 1-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β (πΉβ(πΊβπ)) β π΄) | ||
Theorem | ltrncoval 39542 | Two ways to express value of translation composition. (Contributed by NM, 31-May-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β ((πΉ β πΊ)βπ) = (πΉβ(πΊβπ))) | ||
Theorem | ltrncnv 39543 | The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β β‘πΉ β π) | ||
Theorem | ltrn11at 39544 | Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ π β π΄ β§ π β π)) β (πΉβπ) β (πΉβπ)) | ||
Theorem | ltrneq2 39545* | The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β (βπ β π΄ (πΉβπ) = (πΊβπ) β πΉ = πΊ)) | ||
Theorem | ltrneq 39546* | 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 39547 | 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 39548 | 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 39549* | 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 39550* | 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 39551* | The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πΏβπ·) β (πΉ β π β§ βπ₯ β π (π₯ β (πβπ·) β (πΉβπ₯) = π₯)))) | ||
Theorem | trnfsetN 39552* | 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 39553* | 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 39554* | The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (PSubSpβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) & β’ π = (PAutβπΎ) & β’ πΏ = (DilβπΎ) & β’ π = (TrnβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πΉ β (πβπ·) β (πΉ β (πΏβπ·) β§ βπ β (πβπ·)βπ β (πβπ·)((π + (πΉβπ)) β© ( β₯ β{π·})) = ((π + (πΉβπ)) β© ( β₯ β{π·}))))) | ||
Syntax | ctrl 39555 | Extend class notation with set of all traces of lattice translations. |
class trL | ||
Definition | df-trl 39556* | Define trace of a lattice translation. (Contributed by NM, 20-May-2012.) |
β’ trL = (π β V β¦ (π€ β (LHypβπ) β¦ (π β ((LTrnβπ)βπ€) β¦ (β©π₯ β (Baseβπ)βπ β (Atomsβπ)(Β¬ π(leβπ)π€ β π₯ = ((π(joinβπ)(πβπ))(meetβπ)π€)))))) | ||
Theorem | trlfset 39557* | 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 39558* | 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 39559* | 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 39560 | 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 39561 | Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π βπΉ) β π΅) | ||
Theorem | trlcnv 39562 | The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (π ββ‘πΉ) = (π βπΉ)) | ||
Theorem | trljat1 39563 | 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 39261? (Contributed by NM, 22-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ (π βπΉ)) = (π β¨ (πΉβπ))) | ||
Theorem | trljat2 39564 | 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 39565 | 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 39566 | 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 39567 | 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 39568 | 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 39569 | 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 39570 | 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 39571 | 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 39572 | Property of the identity lattice translation. (Contributed by NM, 27-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉ = ( I βΎ π΅) β (πΉβπ) = π)) | ||
Theorem | trlid0 39573 | The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (π β( I βΎ π΅)) = 0 ) | ||
Theorem | trlnidatb 39574 | A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 39570? Why do both this and ltrnideq 39572 need trlnidat 39570? (Contributed by NM, 4-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΉ β ( I βΎ π΅) β (π βπΉ) β π΄)) | ||
Theorem | trlid0b 39575 | 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 39576 | Different translations with the same trace cannot be the identity. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (πΉ β πΊ β§ (π βπΉ) = (π βπΊ))) β πΉ β ( I βΎ π΅)) | ||
Theorem | ltrn2ateq 39577 | Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πΉβπ) = π β (πΉβπ) = π)) | ||
Theorem | ltrnateq 39578 | 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 39579 | 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 39580 | 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 39581 | 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 39582 | 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 39583 | 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 39584 | 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 39585 | 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 39586 | 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 39587 | 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 39588 | Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 39261? (Contributed by NM, 29-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ ((π β¨ π) β§ π)) = (π β¨ π)) | ||
Theorem | cdlemc2 39589 | 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 39590 | 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 39591 | 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 39592 | Lemma for cdlemc 39594. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (Β¬ π β€ (π β¨ (πΉβπ)) β§ (πΉβπ) β π)) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc6 39593 | Lemma for cdlemc 39594. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemc 39594 | Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ (πΉβπ))) β (πΉβπ) = ((π β¨ (π βπΉ)) β§ ((πΉβπ) β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemd1 39595 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π β§ Β¬ π β€ (π β¨ π)))) β π = ((π β¨ ((π β¨ π ) β§ π)) β§ (π β¨ ((π β¨ π ) β§ π)))) | ||
Theorem | cdlemd2 39596 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd3 39597 | 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 39598 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β€ (π β¨ π) β§ π β π)) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd5 39599 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ π β π΄) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((πΉβπ) = (πΊβπ) β§ (πΉβπ) = (πΊβπ))) β (πΉβπ ) = (πΊβπ )) | ||
Theorem | cdlemd6 39600 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ Β¬ π β€ (π β¨ (πΉβπ))) β§ (πΉβπ) = (πΊβπ)) β (πΉβπ) = (πΊβπ)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |