Home Metamath Proof ExplorerTheorem 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)

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

Theoremcdleme20m 29201 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , , , represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. We prove that if r s t and u s t, then fs(r) = ft(r). (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20 29202 Combine cdleme19f 29186 and cdleme20m 29201 to eliminate condition. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21a 29203 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21b 29204 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21c 29205 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21at 29206 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21ct 29207 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21d 29208 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove fs(r) = fz(r). (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21e 29209 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove that if u s z, then ft(r) = fz(r). (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21f 29210 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21g 29211 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21h 29212* Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21i 29213* Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21j 29214* Combine cdleme20 29202 and cdleme21i 29213 to eliminate condition. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21 29215 Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. , , , , , represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. Combine cdleme18d 29173 and cdleme21j 29214 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21k 29216 Eliminate condition in cdleme21 29215. (Contributed by NM, 26-Dec-2012.)

Theoremcdleme22aa 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.)

Theoremcdleme22a 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.)

Theoremcdleme22b 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.)

Theoremcdleme22cN 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.)

Theoremcdleme22d 29221 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)

Theoremcdleme22e 29222 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. (Contributed by NM, 6-Dec-2012.)

Theoremcdleme22eALTN 29223 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.)

Theoremcdleme22f 29224 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), ft(s) respectively. If s t v, then ft(s) f(t) v. (Contributed by NM, 6-Dec-2012.)

Theoremcdleme22f2 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) fs(t) v. (Contributed by NM, 7-Dec-2012.)

Theoremcdleme22g 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.)

Theoremcdleme23a 29227 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)

Theoremcdleme23b 29228 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)

Theoremcdleme23c 29229 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)

Theoremcdleme24 29230* Quantified version of cdleme21k 29216. (Contributed by NM, 26-Dec-2012.)

Theoremcdleme25a 29231* Lemma for cdleme25b 29232. (Contributed by NM, 1-Jan-2013.)

Theoremcdleme25b 29232* Transform cdleme24 29230. TODO get rid of \$d's on , (Contributed by NM, 1-Jan-2013.)

Theoremcdleme25c 29233* Transform cdleme25b 29232. (Contributed by NM, 1-Jan-2013.)

Theoremcdleme25dN 29234* Transform cdleme25c 29233. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.)

Theoremcdleme25cl 29235* Show closure of the unique element in cdleme25c 29233. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme25cv 29236* Change bound variables in cdleme25c 29233. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme26e 29237* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme26ee 29238* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme26eALTN 29239* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)

Theoremcdleme26fALTN 29240* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), ft(s) respectively. If t t v, then ft(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)

Theoremcdleme26f 29241* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), ft(s) respectively. If t t v, then ft(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)

Theoremcdleme26f2ALTN 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) fs(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)

Theoremcdleme26f2 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) fs(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)

Theoremcdleme27cl 29244* Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.)

Theoremcdleme27a 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) fs(t) v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)

Theoremcdleme27b 29246* Lemma for cdleme27N 29247. (Contributed by NM, 3-Feb-2013.)

Theoremcdleme27N 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.)

Theoremcdleme28a 29248* Lemma for cdleme25b 29232. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.)

Theoremcdleme28b 29249* Lemma for cdleme25b 29232. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)

Theoremcdleme28c 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.)

Theoremcdleme28 29251* Quantified version of cdleme28c 29250. (Compare cdleme24 29230.) (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29ex 29252* Lemma for cdleme29b 29253. (Compare cdleme25a 29231.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29b 29253* Transform cdleme28 29251. (Compare cdleme25b 29232.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29c 29254* Transform cdleme28b 29249. (Compare cdleme25c 29233.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)

Theoremcdleme29cl 29255* Show closure of the unique element in cdleme28c 29250. (Contributed by NM, 8-Feb-2013.)

Theoremcdleme30a 29256 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.)

Theoremcdleme31so 29257* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)

Theoremcdleme31sn 29258* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)

Theoremcdleme31sn1 29259* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)

Theoremcdleme31se 29260* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)

Theoremcdleme31se2 29261* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.)

Theoremcdleme31sc 29262* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)

Theoremcdleme31sde 29263* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.)

Theoremcdleme31snd 29264* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.)

Theoremcdleme31sdnN 29265* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.)

Theoremcdleme31sn1c 29266* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.)

Theoremcdleme31sn2 29267* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.)

Theoremcdleme31fv 29268* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)

Theoremcdleme31fv1 29269* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.)

Theoremcdleme31fv1s 29270* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.)

Theoremcdleme31fv2 29271* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.)

Theoremcdleme31id 29272* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.)

Theoremcdlemefrs29pre00 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.)

Theoremcdlemefrs29bpre0 29274* TODO fix comment. (Contributed by NM, 29-Mar-2013.)