Home | Metamath
Proof Explorer Theorem List (p. 355 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ldilcnv 35401 | The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013.) |
Theorem | ldilco 35402 | The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.) |
Theorem | ltrnfset 35403* | The set of all lattice translations for a lattice . (Contributed by NM, 11-May-2012.) |
Theorem | ltrnset 35404* | The set of lattice translations for a fiducial co-atom . (Contributed by NM, 11-May-2012.) |
Theorem | isltrn 35405* | The predicate "is a lattice translation". Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.) |
Theorem | isltrn2N 35406* | The predicate "is a lattice translation". Version of isltrn 35405 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.) |
Theorem | ltrnu 35407 | 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.) |
Theorem | ltrnldil 35408 | A lattice translation is a lattice dilation. (Contributed by NM, 20-May-2012.) |
Theorem | ltrnlaut 35409 | A lattice translation is a lattice automorphism. (Contributed by NM, 20-May-2012.) |
Theorem | ltrn1o 35410 | A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.) |
Theorem | ltrncl 35411 | Closure of a lattice translation. (Contributed by NM, 20-May-2012.) |
Theorem | ltrn11 35412 | One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012.) |
Theorem | ltrncnvnid 35413 | If a translation is different from the identity, so is its converse. (Contributed by NM, 17-Jun-2013.) |
Theorem | ltrncoidN 35414 | 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.) |
Theorem | ltrnle 35415 | Less-than or equal property of a lattice translation. (Contributed by NM, 20-May-2012.) |
Theorem | ltrncnvleN 35416 | Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013.) (New usage is discouraged.) |
Theorem | ltrnm 35417 | Lattice translation of a meet. (Contributed by NM, 20-May-2012.) |
Theorem | ltrnj 35418 | Lattice translation of a meet. TODO: change antecedent to (Contributed by NM, 25-May-2012.) |
Theorem | ltrncvr 35419 | Covering property of a lattice translation. (Contributed by NM, 20-May-2012.) |
Theorem | ltrnval1 35420 | Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012.) |
Theorem | ltrnid 35421* | 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.) |
Theorem | ltrnnid 35422* | 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.) |
Theorem | ltrnatb 35423 | The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012.) |
Theorem | ltrncnvatb 35424 | The converse of the lattice translation of an atom is an atom. (Contributed by NM, 2-Jun-2012.) |
Theorem | ltrnel 35425 | 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.) |
Theorem | ltrnat 35426 | The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 35425 uses. (Contributed by NM, 25-May-2012.) |
Theorem | ltrncnvat 35427 | The converse of the lattice translation of an atom is an atom. (Contributed by NM, 9-May-2013.) |
Theorem | ltrncnvel 35428 | The converse of the lattice translation of an atom not under the fiducial co-atom. (Contributed by NM, 10-May-2013.) |
Theorem | ltrncoelN 35429 | Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 35425 uses. (Contributed by NM, 1-May-2013.) (New usage is discouraged.) |
Theorem | ltrncoat 35430 | Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 35425, ltrnat 35426 uses. (Contributed by NM, 1-May-2013.) |
Theorem | ltrncoval 35431 | Two ways to express value of translation composition. (Contributed by NM, 31-May-2013.) |
Theorem | ltrncnv 35432 | The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.) |
Theorem | ltrn11at 35433 | Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013.) |
Theorem | ltrneq2 35434* | The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014.) |
Theorem | ltrneq 35435* | The equality of two translations is determined by their equality at atoms not under co-atom . (Contributed by NM, 20-Jun-2013.) |
Theorem | idltrn 35436 | The identity function is a lattice translation. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 18-May-2012.) |
Theorem | ltrnmw 35437 | 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.) |
Theorem | ltrnmwOLD 35438 | 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.) Obsolete version of ltrnmw 35437 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | dilfsetN 35439* | The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-2012.) (New usage is discouraged.) |
Theorem | dilsetN 35440* | The set of dilations for a fiducial atom . (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
Theorem | isdilN 35441* | The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
Theorem | trnfsetN 35442* | The mapping from fiducial atom to set of translations. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
Theorem | trnsetN 35443* | The set of translations for a fiducial atom . (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
Theorem | istrnN 35444* | The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.) |
Syntax | ctrl 35445 | Extend class notation with set of all traces of lattice translations. |
Definition | df-trl 35446* | Define trace of a lattice translation. (Contributed by NM, 20-May-2012.) |
Theorem | trlfset 35447* | The set of all traces of lattice translations for a lattice . (Contributed by NM, 20-May-2012.) |
Theorem | trlset 35448* | The set of traces of lattice translations for a fiducial co-atom . (Contributed by NM, 20-May-2012.) |
Theorem | trlval 35449* | The value of the trace of a lattice translation. (Contributed by NM, 20-May-2012.) |
Theorem | trlval2 35450 | 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 ; we use for convenience. (Contributed by NM, 20-May-2012.) |
Theorem | trlcl 35451 | Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.) |
Theorem | trlcnv 35452 | The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.) |
Theorem | trljat1 35453 | 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 35150? (Contributed by NM, 22-May-2012.) |
Theorem | trljat2 35454 | 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.) |
Theorem | trljat3 35455 | 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.) |
Theorem | trlat 35456 | 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.) |
Theorem | trl0 35457 | 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.) |
Theorem | trlator0 35458 | The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013.) |
Theorem | trlatn0 35459 | The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-2013.) |
Theorem | trlnidat 35460 | 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.) |
Theorem | ltrnnidn 35461 | 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.) |
Theorem | ltrnideq 35462 | Property of the identity lattice translation. (Contributed by NM, 27-May-2012.) |
Theorem | trlid0 35463 | The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013.) |
Theorem | trlnidatb 35464 | A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 35460? Why do both this and ltrnideq 35462 need trlnidat 35460? (Contributed by NM, 4-Jun-2013.) |
Theorem | trlid0b 35465 | A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013.) |
Theorem | trlnid 35466 | Different translations with the same trace cannot be the identity. (Contributed by NM, 26-Jul-2013.) |
Theorem | ltrn2ateq 35467 | Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012.) |
Theorem | ltrnateq 35468 | If any atom (under ) is not equal to its translation, so is any other atom. (Contributed by NM, 6-May-2013.) |
Theorem | ltrnatneq 35469 | 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.) |
Theorem | ltrnatlw 35470 | 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.) |
Theorem | trlle 35471 | The trace of a lattice translation is less than the fiducial co-atom . (Contributed by NM, 25-May-2012.) |
Theorem | trlne 35472 | 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.) |
Theorem | trlnle 35473 | 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.) |
Theorem | trlval3 35474 | 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.) |
Theorem | trlval4 35475 | The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-May-2013.) |
Theorem | trlval5 35476 | The value of the trace of a lattice translation in terms of itself. (Contributed by NM, 19-Jul-2013.) |
Theorem | arglem1N 35477 | Lemma for Desargues' law. Theorem 13.3 of [Crawley] p. 110, 3rd and 4th 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.) |
Theorem | cdlemc1 35478 | Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 35150? (Contributed by NM, 29-May-2012.) |
Theorem | cdlemc2 35479 | Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.) |
Theorem | cdlemc3 35480 | Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
Theorem | cdlemc4 35481 | Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
Theorem | cdlemc5 35482 | Lemma for cdlemc 35484. (Contributed by NM, 26-May-2012.) |
Theorem | cdlemc6 35483 | Lemma for cdlemc 35484. (Contributed by NM, 26-May-2012.) |
Theorem | cdlemc 35484 | Lemma C in [Crawley] p. 113. (Contributed by NM, 26-May-2012.) |
Theorem | cdlemd1 35485 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
Theorem | cdlemd2 35486 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 29-May-2012.) |
Theorem | cdlemd3 35487 | Part of proof of Lemma D in [Crawley] p. 113. The requirement is not mentioned in their proof. (Contributed by NM, 29-May-2012.) |
Theorem | cdlemd4 35488 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
Theorem | cdlemd5 35489 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 30-May-2012.) |
Theorem | cdlemd6 35490 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-May-2012.) |
Theorem | cdlemd7 35491 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
Theorem | cdlemd8 35492 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Jun-2012.) |
Theorem | cdlemd9 35493 | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.) |
Theorem | cdlemd 35494 | 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.) |
Theorem | ltrneq3 35495 | Two translations agree at any atom not under the fiducial co-atom iff they are equal. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdleme00a 35496 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme0aa 35497 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme0a 35498 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
Theorem | cdleme0b 35499 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme0c 35500 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |