Home Metamath Proof ExplorerTheorem List (p. 306 of 322) < 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-22262) Hilbert Space Explorer (22263-23785) Users' Mathboxes (23786-32130)

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

Theoremcdleme21j 30501* Combine cdleme20 30489 and cdleme21i 30500 to eliminate condition. (Contributed by NM, 29-Nov-2012.)

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

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

Theoremcdleme22aa 30504 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 30505 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 30506 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 30507 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 30508 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)

Theoremcdleme22e 30509 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 30510 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 30511 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 30512 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 30511 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 30513 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 30514 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)

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

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

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

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

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

Theoremcdleme25c 30520* Transform cdleme25b 30519. (Contributed by NM, 1-Jan-2013.)

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

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

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

Theoremcdleme26e 30524* 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 30525* 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 30526* 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 30527* 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 30528* 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 30529* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 30527 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 30530* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 30527 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 30531* Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.)

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

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

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

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

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

Theoremcdleme28 30538* Quantified version of cdleme28c 30537. (Compare cdleme24 30517.) (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29ex 30539* Lemma for cdleme29b 30540. (Compare cdleme25a 30518.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29b 30540* Transform cdleme28 30538. (Compare cdleme25b 30519.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29c 30541* Transform cdleme28b 30536. (Compare cdleme25c 30520.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcdlemefrs32fva 30565* 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 30195 here and elsewhere, and presence/absence of term. Also, why can proof be shortened with cdleme29cl 30542? What is difference from cdlemefs27cl 30578? (Contributed by NM, 29-Mar-2013.)

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

Theoremcdlemefr29exN 30567* Lemma for cdlemefs29bpre1N 30582. (Compare cdleme25a 30518.) TODO: FIX COMMENT TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)

Theoremcdlemefr27cl 30568 Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 23-Mar-2013.)

Theoremcdlemefr32sn2aw 30569* Show that is an atom not under when . (Contributed by NM, 28-Mar-2013.)

Theoremcdlemefr32snb 30570* Show closure of . (Contributed by NM, 28-Mar-2013.)

Theoremcdlemefr29bpre0N 30571* TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.)

Theoremcdlemefr29clN 30572* Show closure of the unique element in cdleme29c 30541. TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)

Theoremcdleme43frv1snN 30573* Value of when . (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.)

Theoremcdlemefr32fvaN 30574* Part of proof of Lemma E in [Crawley] p. 113. Value of at an atom not under . TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.)

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