Home Metamath Proof ExplorerTheorem List (p. 313 of 329) < 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-22426) Hilbert Space Explorer (22427-23949) Users' Mathboxes (23950-32835)

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

Theoremcdleme21e 31201 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 31202 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

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

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

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

Theoremcdleme21j 31206* Combine cdleme20 31194 and cdleme21i 31205 to eliminate condition. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21 31207 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 31165 and cdleme21j 31206 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)

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

Theoremcdleme22aa 31209 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 31210 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 31211 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 31212 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 31213 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)

Theoremcdleme22e 31214 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 31215 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 31216 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 31217 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 31216 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 31218 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 31219 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)

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

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

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

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

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

Theoremcdleme25c 31225* Transform cdleme25b 31224. (Contributed by NM, 1-Jan-2013.)

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

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

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

Theoremcdleme26e 31229* 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 31230* 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 31231* 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 31232* 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 31233* 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 31234* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 31232 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 31235* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 31232 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 31236* Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.)

Theoremcdleme27a 31237* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 31233 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 31238* Lemma for cdleme27N 31239. (Contributed by NM, 3-Feb-2013.)

Theoremcdleme27N 31239* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme27a 31237. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.)

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

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

Theoremcdleme28c 31242* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme28b 31241. TODO: FIX COMMENT (Contributed by NM, 6-Feb-2013.)

Theoremcdleme28 31243* Quantified version of cdleme28c 31242. (Compare cdleme24 31222.) (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29ex 31244* Lemma for cdleme29b 31245. (Compare cdleme25a 31223.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29b 31245* Transform cdleme28 31243. (Compare cdleme25b 31224.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29c 31246* Transform cdleme28b 31241. (Compare cdleme25c 31225.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcdlemefrs29pre00 31265 ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 30900. (Contributed by NM, 29-Mar-2013.)

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

Theoremcdlemefrs29bpre1 31267* TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)

Theoremcdlemefrs29cpre1 31268* TODO FIX COMMENT (Contributed by NM, 29-Mar-2013.)

Theoremcdlemefrs29clN 31269* TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 31268. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)

Theoremcdlemefrs32fva 31270* Part of proof of Lemma E in [Crawley] p. 113. Value of at an atom not under . TODO: FIX COMMENT TODO: consolidate uses of lhpmat 30900 here and elsewhere, and presence/absence of term. Also, why can proof be shortened with cdleme29cl 31247? What is difference from cdlemefs27cl 31283? (Contributed by NM, 29-Mar-2013.)

Theoremcdlemefrs32fva1 31271* Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.)