Home | Metamath
Proof Explorer Theorem List (p. 295 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 | cdleme19f 29401 | 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 29402 | 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 29403 | 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 29404 | 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 29405 | 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 29406 | 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 29407 | 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 29408 | 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 29409 | 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 29410 | 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 29411 | 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 29412 | 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 29413 | 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 29414 | 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 29415 | 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 29416 | 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 29417 | Combine cdleme19f 29401 and cdleme20m 29416 to eliminate condition. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21a 29418 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21b 29419 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21c 29420 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21at 29421 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21ct 29422 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21d 29423 | 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 29424 | 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 29425 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21g 29426 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21h 29427* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21i 29428* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21j 29429* | Combine cdleme20 29417 and cdleme21i 29428 to eliminate condition. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21 29430 | 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 29388 and cdleme21j 29429 to eliminate existence condition, proving f_{s}(r) = f_{t}(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21k 29431 | Eliminate condition in cdleme21 29430. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme22aa 29432 | 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 29433 | 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 29434 | 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 29435 | 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 29436 | 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 29437 | 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 29438 | 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 29439 | 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 29440 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 29439 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 29441 | 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 29442 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme23b 29443 | 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 29444 | 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 29445* | Quantified version of cdleme21k 29431. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme25a 29446* | Lemma for cdleme25b 29447. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25b 29447* | Transform cdleme24 29445. TODO get rid of $d's on , (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25c 29448* | Transform cdleme25b 29447. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25dN 29449* | Transform cdleme25c 29448. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
Theorem | cdleme25cl 29450* | Show closure of the unique element in cdleme25c 29448. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme25cv 29451* | Change bound variables in cdleme25c 29448. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26e 29452* | 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. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26ee 29453* | 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. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26eALTN 29454* | 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. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme26fALTN 29455* | 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 t t v, then f_{t}(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme26f 29456* | 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 t t v, then f_{t}(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) |
Theorem | cdleme26f2ALTN 29457* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 29455 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) f_{s}(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme26f2 29458* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 29455 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) f_{s}(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) |
Theorem | cdleme27cl 29459* | Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme27a 29460* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 29456 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) f_{s}(t) v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.) |
Theorem | cdleme27b 29461* | Lemma for cdleme27N 29462. (Contributed by NM, 3-Feb-2013.) |
Theorem | cdleme27N 29462* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme27a 29460. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme28a 29463* | Lemma for cdleme25b 29447. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.) |
Theorem | cdleme28b 29464* | Lemma for cdleme25b 29447. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.) |