Home | Metamath
Proof Explorer Theorem List (p. 293 of 309) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme20m 29201 | 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 29202 | Combine cdleme19f 29186 and cdleme20m 29201 to eliminate condition. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21a 29203 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21b 29204 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21c 29205 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21at 29206 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21ct 29207 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21d 29208 | 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 29209 | 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 29210 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21g 29211 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21h 29212* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21i 29213* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21j 29214* | Combine cdleme20 29202 and cdleme21i 29213 to eliminate condition. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21 29215 | 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 29173 and cdleme21j 29214 to eliminate existence condition, proving f_{s}(r) = f_{t}(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21k 29216 | Eliminate condition in cdleme21 29215. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme22aa 29217 | 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 29218 | 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 29219 | 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 29220 | 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 29221 | 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 29222 | 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 29223 | 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 29224 | 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 29225 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 29224 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 29226 | 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 29227 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme23b 29228 | 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 29229 | 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 29230* | Quantified version of cdleme21k 29216. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme25a 29231* | Lemma for cdleme25b 29232. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25b 29232* | Transform cdleme24 29230. TODO get rid of $d's on , (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25c 29233* | Transform cdleme25b 29232. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25dN 29234* | Transform cdleme25c 29233. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
Theorem | cdleme25cl 29235* | Show closure of the unique element in cdleme25c 29233. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme25cv 29236* | Change bound variables in cdleme25c 29233. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26e 29237* | 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 29238* | 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 29239* | 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 29240* | 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 29241* | 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 29242* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 29240 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 29243* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 29240 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 29244* | Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme27a 29245* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 29241 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 29246* | Lemma for cdleme27N 29247. (Contributed by NM, 3-Feb-2013.) |
Theorem | cdleme27N 29247* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme27a 29245. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme28a 29248* | Lemma for cdleme25b 29232. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.) |
Theorem | cdleme28b 29249* | Lemma for cdleme25b 29232. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme28c 29250* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme28b 29249. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme28 29251* | Quantified version of cdleme28c 29250. (Compare cdleme24 29230.) (Contributed by NM, 7-Feb-2013.) |
Theorem | cdleme29ex 29252* | Lemma for cdleme29b 29253. (Compare cdleme25a 29231.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.) |
Theorem | cdleme29b 29253* | Transform cdleme28 29251. (Compare cdleme25b 29232.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.) |
Theorem | cdleme29c 29254* | Transform cdleme28b 29249. (Compare cdleme25c 29233.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.) |
Theorem | cdleme29cl 29255* | Show closure of the unique element in cdleme28c 29250. (Contributed by NM, 8-Feb-2013.) |
Theorem | cdleme30a 29256 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.) |
Theorem | cdleme31so 29257* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
Theorem | cdleme31sn 29258* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31sn1 29259* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31se 29260* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31se2 29261* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdleme31sc 29262* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
Theorem | cdleme31sde 29263* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
Theorem | cdleme31snd 29264* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme31sdnN 29265* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme31sn1c 29266* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.) |
Theorem | cdleme31sn2 29267* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31fv 29268* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
Theorem | cdleme31fv1 29269* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
Theorem | cdleme31fv1s 29270* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
Theorem | cdleme31fv2 29271* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.) |
Theorem | cdleme31id 29272* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemefrs29pre00 29273 | ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 28908. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefrs29bpre0 29274* | TODO fix comment. (Contributed by NM, 29-Mar-2013.) |