Home | Metamath
Proof Explorer Theorem List (p. 294 of 311) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-31058) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | ltrneq3 29301 | Two translations agree at any atom not under the fiducial co-atom iff they are equal. (Contributed by NM, 25-Jul-2013.) |
Theorem | cdleme00a 29302 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme0aa 29303 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme0a 29304 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
Theorem | cdleme0b 29305 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme0c 29306 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 12-Jun-2012.) |
Theorem | cdleme0cp 29307 | Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 29690- swap consequent equality; make antecedent use df-3an 941. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme0cq 29308 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.) |
Theorem | cdleme0dN 29309 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme0e 29310 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme0fN 29311 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme0gN 29312 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
Theorem | cdlemeulpq 29313 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.) |
Theorem | cdleme01N 29314 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme02N 29315 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme0ex1N 29316* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme0ex2N 29317* | 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.) |
Theorem | cdleme0moN 29318* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme1b 29319 | 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.) |
Theorem | cdleme1 29320 | 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.) |
Theorem | cdleme2 29321 | 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.) |
Theorem | cdleme3b 29322 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3c 29323 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3d 29324 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3e 29325 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3fN 29326 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. TODO: Delete - duplicates cdleme0e 29310. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme3g 29327 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme3h 29328 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29329 and cdleme3 29330. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3fa 29329 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 29330. (Contributed by NM, 6-Oct-2012.) |
Theorem | cdleme3 29330 | Part of proof of Lemma E in [Crawley] p. 113. represents f(r). is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 29329 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 29322 through cdleme3 29330, so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme4 29331 | Part of proof of Lemma E in [Crawley] p. 113. and represent f(s) and f_{s}(r). Here show p q = r u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme4a 29332 | Part of proof of Lemma E in [Crawley] p. 114 top. represents f_{s}(r). Auxiliary lemma derived from cdleme5 29333. We show f_{s}(r) p q. (Contributed by NM, 10-Nov-2012.) |
Theorem | cdleme5 29333 | Part of proof of Lemma E in [Crawley] p. 113. represents f_{s}(r). We show r f_{s}(r)) = p q at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme6 29334 | Part of proof of Lemma E in [Crawley] p. 113. This expresses (r f_{s}(r)) w = u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7aa 29335 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29341 and cdleme7 29342. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7a 29336 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29341 and cdleme7 29342. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7b 29337 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29341 and cdleme7 29342. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7c 29338 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29341 and cdleme7 29342. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7d 29339 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29341 and cdleme7 29342. (Contributed by NM, 8-Jun-2012.) |
Theorem | cdleme7e 29340 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29341 and cdleme7 29342. (Contributed by NM, 8-Jun-2012.) |
Theorem | cdleme7ga 29341 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 29342. (Contributed by NM, 8-Jun-2012.) |
Theorem | cdleme7 29342 | Part of proof of Lemma E in [Crawley] p. 113. and represent f_{s}(r) and f(s) respectively. is the fiducial co-atom (hyperplane) that they call w. Here and in cdleme7ga 29341 above, we show that f_{s}(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 29335 through cdleme7 29342, so there may be a simpler proof that we have overlooked. (Contributed by NM, 9-Jun-2012.) |
Theorem | cdleme8 29343 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents s_{1}. In their notation, we prove p s_{1} = p s. (Contributed by NM, 9-Jun-2012.) |
Theorem | cdleme9a 29344 | Part of proof of Lemma E in [Crawley] p. 113. represents s_{1}, which we prove is an atom. (Contributed by NM, 10-Jun-2012.) |
Theorem | cdleme9b 29345 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
Theorem | cdleme9 29346 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. and represent s_{1} and f(s) respectively. In their notation, we prove f(s) s_{1} = q s_{1}. (Contributed by NM, 10-Jun-2012.) |
Theorem | cdleme10 29347 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents s_{2}. In their notation, we prove s s_{2} = s r. (Contributed by NM, 9-Jun-2012.) |
Theorem | cdleme8tN 29348 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents t_{1}. In their notation, we prove p t_{1} = p t. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme9taN 29349 | Part of proof of Lemma E in [Crawley] p. 113. represents t_{1}, which we prove is an atom. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme9tN 29350 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. and represent t_{1} and f(t) respectively. In their notation, we prove f(t) t_{1} = q t_{1}. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme10tN 29351 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents t_{2}. In their notation, we prove t t_{2} = t r. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme16aN 29352 | 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.) |
Theorem | cdleme11a 29353 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 12-Jun-2012.) |
Theorem | cdleme11c 29354 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme11dN 29355 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme11e 29356 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme11fN 29357 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme11g 29358 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11h 29359 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11j 29360 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11k 29361 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme11l 29362 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29363. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme11 29363 | 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 29353 through cdleme11 29363, so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme12 29364 | 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.) |
Theorem | cdleme13 29365 | 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.) |
Theorem | cdleme14 29366 | 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 28979 to cdleme13 29365. and represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.) |
Theorem | cdleme15a 29367 | 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 s_{1}) (q s_{1})) ((p t_{1}) (q t_{1})). We represent f(s), f(t), s_{1}, and t_{1} with , , , and respectively. The order of our operations is slightly different. (Contributed by NM, 9-Oct-2012.) |
Theorem | cdleme15b 29368 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (p s_{1}) (q s_{1})=s_{1}. We represent s_{1} with . (Contributed by NM, 10-Oct-2012.) |
Theorem | cdleme15c 29369 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((p s_{1}) (q s_{1})) ((p t_{1}) (q t_{1}))=s_{1} t_{1}. and represent s_{1} and t_{1} respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.) |
Theorem | cdleme15d 29370 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s_{1} t_{1} w. and represent s_{1} and t_{1} respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.) |
Theorem | cdleme15 29371 | 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.) |
Theorem | cdleme16b 29372 | 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.) |
Theorem | cdleme16c 29373 | 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.) |
Theorem | cdleme16d 29374 | 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.) |
Theorem | cdleme16e 29375 | 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.) |
Theorem | cdleme16f 29376 | 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.) |
Theorem | cdleme16g 29377 | 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.) |
Theorem | cdleme16 29378 | 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.) |
Theorem | cdleme17a 29379 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , , and represent f(s), f_{s}(p), and s_{1} respectively. We show, in their notation, f_{s}(p)=(p q) (q s_{1}). (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17b 29380 | Lemma leading to cdleme17c 29381. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17c 29381 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. represents s_{1}. We show, in their notation, (p q) (q s_{1})=q. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17d1 29382 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , represent f(s), f_{s}(p) respectively. We show, in their notation, f_{s}(p)=q. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme0nex 29383* | 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 29304- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 28437, 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.) |
Theorem | cdleme18a 29384 | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), f_{s}(q) respectively. We show f_{s}(q) w. (Contributed by NM, 12-Oct-2012.) |
Theorem | cdleme18b 29385 | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), f_{s}(q) respectively. We show f_{s}(q) q. (Contributed by NM, 12-Oct-2012.) |
Theorem | cdleme18c 29386* | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), f_{s}(q) respectively. We show f_{s}(q) = p whenever p q has three atoms under it (implied by the negated existential condition). (Contributed by NM, 10-Nov-2012.) |
Theorem | cdleme22gb 29387 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
Theorem | cdleme18d 29388* | Part of proof of Lemma E in [Crawley] p. 114, 4th sentence of 4th paragraph. , , , represent f(s), f_{s}(r), f(t), f_{t}(r) respectively. We show f_{s}(r)=f_{t}(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.) |
Theorem | cdlemesner 29389 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemedb 29390 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdlemeda 29391 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemednpq 29392 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdlemednuN 29393 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20zN 29394 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20y 29395 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme19a 29396 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. represents s_{2}. In their notation, we prove that if r s t, then s_{2=}(s t) w. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdleme19b 29397 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. , , represent s_{2}, f(s), f(t). In their notation, we prove that if r s t, then s_{2} f(s) f(t). (Contributed by NM, 13-Nov-2012.) |
Theorem | cdleme19c 29398 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. , represent s_{2}, f(s). We prove f(s) s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdleme19d 29399 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114. , , represent s_{2}, f(s), f(t). We prove f(s) s_{2} = f(s) f(t). (Contributed by NM, 14-Nov-2012.) |