Home | Metamath
Proof Explorer Theorem List (p. 365 of 385) | < 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-26033) |
Hilbert Space Explorer
(26034-27558) |
Users' Mathboxes
(27559-38473) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme16b 36401 | 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 36402 | 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 36403 | 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 36404 | 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 36405 | 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 36406 | 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 36407 | 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 36408 | 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 36409 | Lemma leading to cdleme17c 36410. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17c 36410 | 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 36411 | 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 36412* | 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 36333- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 35465, 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 36413 | 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 36414 | 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 36415* | 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 36416 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
Theorem | cdleme18d 36417* | 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 36418 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemedb 36419 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdlemeda 36420 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemednpq 36421 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdlemednuN 36422 | 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 36423 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20y 36424 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (Proof shortened by OpenAI, 25-Mar-2020.) |
Theorem | cdleme20yOLD 36425 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) Obsolete version of cdleme20y 36424 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
Theorem | cdleme19a 36426 | 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 36427 | 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 36428 | 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 36429 | 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.) |
Theorem | cdleme19e 36430 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 2. , , , represent s_{2}, f(s), t_{2}, f(t). We prove f(s) s_{2=f}(t) t_{2}. (Contributed by NM, 14-Nov-2012.) |
Theorem | cdleme19f 36431 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 3. , , , , , represent s_{2}, f(s), f_{s}(r), t_{2}, f(t), f_{t}(r). We prove that if r s t, then f_{t}(r) = f_{t}(r). (Contributed by NM, 14-Nov-2012.) |
Theorem | cdleme20aN 36432 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 14-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20bN 36433 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. , , , represent s_{2}, f(s), t_{2}, f(t). We show v s_{2} = v t_{2}. (Contributed by NM, 15-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20c 36434 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 15-Nov-2012.) |
Theorem | cdleme20d 36435 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme20e 36436 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line. , , , represent s_{2}, f(s), t_{2}, f(t). We show <f(s),s_{2},s> and <f(t),t_{2},t> are centrally perspective. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme20f 36437 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line. , , , represent s_{2}, f(s), t_{2}, f(t). We show <f(s),s_{2},s> and <f(t),t_{2},t> are axially perspective. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme20g 36438 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20h 36439 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20i 36440 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). We show (f(s) s_{2}) (f(t) t_{2}) p q. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20j 36441 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114. , , , represent s_{2}, f(s), t_{2}, f(t). We show s_{2} t_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20k 36442 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20l1 36443 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s_{2}, f(s), t_{2}, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20l2 36444 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s_{2}, f(s), t_{2}, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20l 36445 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s_{2}, f(s), t_{2}, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20m 36446 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , , , represent s_{2}, f(s), f_{s}(r), t_{2}, f(t), f_{t}(r) respectively. We prove that if r s t and u s t, then f_{s}(r) = f_{t}(r). (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20 36447 | Combine cdleme19f 36431 and cdleme20m 36446 to eliminate condition. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21a 36448 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21b 36449 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21c 36450 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21at 36451 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21ct 36452 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21d 36453 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s_{2}, f(s), f_{s}(r), z_{2}, f(z), f_{z}(r) respectively. We prove f_{s}(r) = f_{z}(r). (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21e 36454 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s_{2}, f(s), f_{s}(r), z_{2}, f(z), f_{z}(r) respectively. We prove that if u s z, then f_{t}(r) = f_{z}(r). (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21f 36455 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21g 36456 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21h 36457* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21i 36458* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21j 36459* | Combine cdleme20 36447 and cdleme21i 36458 to eliminate condition. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21 36460 | Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. , , , , , represent s_{2}, f(s), f_{s}(r), t_{2}, f(t), f_{t}(r) respectively. Combine cdleme18d 36417 and cdleme21j 36459 to eliminate existence condition, proving f_{s}(r) = f_{t}(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21k 36461 | Eliminate condition in cdleme21 36460. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme22aa 36462 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t v = p q implies v = u. (Contributed by NM, 2-Dec-2012.) |
Theorem | cdleme22a 36463 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 3rd line on p. 115. Show that t v = p q implies v = u. (Contributed by NM, 30-Nov-2012.) |
Theorem | cdleme22b 36464 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t v =/= p q and s p q implies t p q. (Contributed by NM, 2-Dec-2012.) |
Theorem | cdleme22cN 36465 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 5th line on p. 115. Show that t v =/= p q and s p q implies v p q. (Contributed by NM, 3-Dec-2012.) (New usage is discouraged.) |
Theorem | cdleme22d 36466 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.) |
Theorem | cdleme22e 36467 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. (Contributed by NM, 6-Dec-2012.) |
Theorem | cdleme22eALTN 36468 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.) |
Theorem | cdleme22f 36469 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), f_{t}(s) respectively. If s t v, then f_{t}(s) f(t) v. (Contributed by NM, 6-Dec-2012.) |
Theorem | cdleme22f2 36470 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 36469 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) f_{s}(t) v. (Contributed by NM, 7-Dec-2012.) |
Theorem | cdleme22g 36471 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(s), f(t) respectively. If s t v and s p q, then f(s) f(t) v. (Contributed by NM, 6-Dec-2012.) |
Theorem | cdleme23a 36472 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme23b 36473 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme23c 36474 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme24 36475* | Quantified version of cdleme21k 36461. (Contributed by NM, 26-Dec-2012.) |