Home Metamath Proof ExplorerTheorem List (p. 312 of 329) < 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-22452) Hilbert Space Explorer (22453-23975) Users' Mathboxes (23976-32860)

Theorem List for Metamath Proof Explorer - 31101-31200   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcdlemd9 31101 Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Jun-2012.)

Theoremcdlemd 31102 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.)

Theoremltrneq3 31103 Two translations agree at any atom not under the fiducial co-atom iff they are equal. (Contributed by NM, 25-Jul-2013.)

Theoremcdleme00a 31104 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.)

Theoremcdleme0aa 31105 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.)

Theoremcdleme0a 31106 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.)

Theoremcdleme0b 31107 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.)

Theoremcdleme0c 31108 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.)

Theoremcdleme0cp 31109 Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 31492- swap consequent equality; make antecedent use df-3an 939. (Contributed by NM, 13-Jun-2012.)

Theoremcdleme0cq 31110 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.)

Theoremcdleme0dN 31111 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.)

Theoremcdleme0e 31112 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.)

Theoremcdleme0fN 31113 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)

Theoremcdleme0gN 31114 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)

Theoremcdlemeulpq 31115 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.)

Theoremcdleme01N 31116 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)

Theoremcdleme02N 31117 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)

Theoremcdleme0ex1N 31118* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)

Theoremcdleme0ex2N 31119* 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.)

Theoremcdleme0moN 31120* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.)

Theoremcdleme1b 31121 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.)

Theoremcdleme1 31122 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.)

Theoremcdleme2 31123 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.)

Theoremcdleme3b 31124 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. (Contributed by NM, 6-Jun-2012.)

Theoremcdleme3c 31125 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. (Contributed by NM, 6-Jun-2012.)

Theoremcdleme3d 31126 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. (Contributed by NM, 6-Jun-2012.)

Theoremcdleme3e 31127 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. (Contributed by NM, 6-Jun-2012.)

Theoremcdleme3fN 31128 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. TODO: Delete - duplicates cdleme0e 31112. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.)

Theoremcdleme3g 31129 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. (Contributed by NM, 7-Jun-2012.)

Theoremcdleme3h 31130 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 31131 and cdleme3 31132. (Contributed by NM, 6-Jun-2012.)

Theoremcdleme3fa 31131 Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 31132. (Contributed by NM, 6-Oct-2012.)

Theoremcdleme3 31132 Part of proof of Lemma E in [Crawley] p. 113. represents f(r). is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 31131 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 31124 through cdleme3 31132, so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012.)

Theoremcdleme4 31133 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.)

Theoremcdleme4a 31134 Part of proof of Lemma E in [Crawley] p. 114 top. represents fs(r). Auxiliary lemma derived from cdleme5 31135. We show fs(r) p q. (Contributed by NM, 10-Nov-2012.)

Theoremcdleme5 31135 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.)

Theoremcdleme6 31136 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.)

Theoremcdleme7aa 31137 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31143 and cdleme7 31144. (Contributed by NM, 7-Jun-2012.)

Theoremcdleme7a 31138 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31143 and cdleme7 31144. (Contributed by NM, 7-Jun-2012.)

Theoremcdleme7b 31139 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31143 and cdleme7 31144. (Contributed by NM, 7-Jun-2012.)

Theoremcdleme7c 31140 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31143 and cdleme7 31144. (Contributed by NM, 7-Jun-2012.)

Theoremcdleme7d 31141 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31143 and cdleme7 31144. (Contributed by NM, 8-Jun-2012.)

Theoremcdleme7e 31142 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 31143 and cdleme7 31144. (Contributed by NM, 8-Jun-2012.)

Theoremcdleme7ga 31143 Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 31144. (Contributed by NM, 8-Jun-2012.)

Theoremcdleme7 31144 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 31143 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 31137 through cdleme7 31144, so there may be a simpler proof that we have overlooked. (Contributed by NM, 9-Jun-2012.)

Theoremcdleme8 31145 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.)

Theoremcdleme9a 31146 Part of proof of Lemma E in [Crawley] p. 113. represents s1, which we prove is an atom. (Contributed by NM, 10-Jun-2012.)

Theoremcdleme9b 31147 Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.)

Theoremcdleme9 31148 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. and represent s1 and f(s) respectively. In their notation, we prove f(s) s1 = q s1. (Contributed by NM, 10-Jun-2012.)

Theoremcdleme10 31149 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents s2. In their notation, we prove s s2 = s r. (Contributed by NM, 9-Jun-2012.)

Theoremcdleme8tN 31150 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents t1. In their notation, we prove p t1 = p t. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)

Theoremcdleme9taN 31151 Part of proof of Lemma E in [Crawley] p. 113. represents t1, which we prove is an atom. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)

Theoremcdleme9tN 31152 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. and represent t1 and f(t) respectively. In their notation, we prove f(t) t1 = q t1. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)

Theoremcdleme10tN 31153 Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents t2. In their notation, we prove t t2 = t r. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.)

Theoremcdleme16aN 31154 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s u t u. (Contributed by NM, 9-Oct-2012.) (New usage is discouraged.)

Theoremcdleme11a 31155 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 12-Jun-2012.)

Theoremcdleme11c 31156 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 13-Jun-2012.)

Theoremcdleme11dN 31157 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.)

Theoremcdleme11e 31158 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 13-Jun-2012.)

Theoremcdleme11fN 31159 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.)

Theoremcdleme11g 31160 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 14-Jun-2012.)

Theoremcdleme11h 31161 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 14-Jun-2012.)

Theoremcdleme11j 31162 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 14-Jun-2012.)

Theoremcdleme11k 31163 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 15-Jun-2012.)

Theoremcdleme11l 31164 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31165. (Contributed by NM, 15-Jun-2012.)

Theoremcdleme11 31165 Part of proof of Lemma E in [Crawley] p. 113, 1st sentence of 3rd paragraph on p. 114. and represent f(s) and f(t) respectively. Their proof provides no details of our cdleme11a 31155 through cdleme11 31165, so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-2012.)

Theoremcdleme12 31166 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. and represent f(s) and f(t) respectively. (Contributed by NM, 16-Jun-2012.)

Theoremcdleme13 31167 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, "<s,t,p> and <f(s),f(t),q> are centrally perspective." and represent f(s) and f(t) respectively. (Contributed by NM, 7-Oct-2012.)

Theoremcdleme14 31168 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, "<s,t,p> and <f(s),f(t),q> ... are axially perspective." We apply dalaw 30781 to cdleme13 31167. and represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.)

Theoremcdleme15a 31169 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((s p) (f(s) q)) ((t p) (f(t) q))=((p s1) (q s1)) ((p t1) (q t1)). We represent f(s), f(t), s1, and t1 with , , , and respectively. The order of our operations is slightly different. (Contributed by NM, 9-Oct-2012.)

Theoremcdleme15b 31170 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (p s1) (q s1)=s1. We represent s1 with . (Contributed by NM, 10-Oct-2012.)

Theoremcdleme15c 31171 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((p s1) (q s1)) ((p t1) (q t1))=s1 t1. and represent s1 and t1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.)

Theoremcdleme15d 31172 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s1 t1 w. and represent s1 and t1 respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.)

Theoremcdleme15 31173 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (s t) (f(s) f(t)) w. We use , for f(s), f(t) respectively. (Contributed by NM, 10-Oct-2012.)

Theoremcdleme16b 31174 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, first part of 3rd sentence. and represent f(s) and f(t) respectively. It is unclear how this follows from s u t u, as the authors state, and we used a different proof. (Note: the antecedent is not used.) (Contributed by NM, 11-Oct-2012.)

Theoremcdleme16c 31175 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 2nd part of 3rd sentence. and represent f(s) and f(t) respectively. We show, in their notation, s t f(s) f(t)=s t u. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme16d 31176 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. and represent f(s) and f(t) respectively. We show, in their notation, (s t) (f(s) f(t)) is an atom. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme16e 31177 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. and represent f(s) and f(t) respectively. We show, in their notation, (s t) (f(s) f(t))=(s t) w. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme16f 31178 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, 3rd part of 3rd sentence. and represent f(s) and f(t) respectively. We show, in their notation, (s t) (f(s) f(t))=(f(s) f(t)) w. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme16g 31179 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, Eq. (1). and represent f(s) and f(t) respectively. We show, in their notation, (s t) w=(f(s) f(t)) w. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme16 31180 Part of proof of Lemma E in [Crawley] p. 113, conclusion of 3rd paragraph on p. 114. and represent f(s) and f(t) respectively. We show, in their notation, (s t) w=(f(s) f(t)) w, whether or not u s t. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme17a 31181 Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , , and represent f(s), fs(p), and s1 respectively. We show, in their notation, fs(p)=(p q) (q s1). (Contributed by NM, 11-Oct-2012.)

Theoremcdleme17b 31182 Lemma leading to cdleme17c 31183. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme17c 31183 Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. represents s1. We show, in their notation, (p q) (q s1)=q. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme17d1 31184 Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , represent f(s), fs(p) respectively. We show, in their notation, fs(p)=q. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme0nex 31185* Part of proof of Lemma E in [Crawley] p. 114, 4th line of 4th paragraph. Whenever (in their terminology) p q/0 (i.e. the sublattice from 0 to p q) contains precisely three atoms, any atom not under w must equal either p or q. (In case of 3 atoms, one of them must be u - see cdleme0a 31106- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 30239, our is a shorter way to express . Thus, the negated existential condition states there are no atoms different from p or q that are also not under w. (Contributed by NM, 12-Nov-2012.)

Theoremcdleme18a 31186 Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), fs(q) respectively. We show fs(q) w. (Contributed by NM, 12-Oct-2012.)

Theoremcdleme18b 31187 Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), fs(q) respectively. We show fs(q) q. (Contributed by NM, 12-Oct-2012.)

Theoremcdleme18c 31188* Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), fs(q) respectively. We show fs(q) = p whenever p q has three atoms under it (implied by the negated existential condition). (Contributed by NM, 10-Nov-2012.)

Theoremcdleme22gb 31189 Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.)

Theoremcdleme18d 31190* Part of proof of Lemma E in [Crawley] p. 114, 4th sentence of 4th paragraph. , , , represent f(s), fs(r), f(t), ft(r) respectively. We show fs(r)=ft(r) for all possible r (which must equal p or q in the case of exactly 3 atoms in p q/0 i.e. when ...). (Contributed by NM, 12-Nov-2012.)

Theoremcdlemesner 31191 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.)

Theoremcdlemedb 31192 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 20-Nov-2012.)

Theoremcdlemeda 31193 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 13-Nov-2012.)

Theoremcdlemednpq 31194 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 18-Nov-2012.)

TheoremcdlemednuN 31195 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.)

Theoremcdleme20zN 31196 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.)

Theoremcdleme20y 31197 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.)

Theoremcdleme19a 31198 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. represents s2. In their notation, we prove that if r s t, then s2=(s t) w. (Contributed by NM, 13-Nov-2012.)

Theoremcdleme19b 31199 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. , , represent s2, f(s), f(t). In their notation, we prove that if r s t, then s2 f(s) f(t). (Contributed by NM, 13-Nov-2012.)

Theoremcdleme19c 31200 Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. , represent s2, f(s). We prove f(s) s2. (Contributed by NM, 13-Nov-2012.)