Home Metamath Proof ExplorerTheorem List (p. 309 of 325) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-22374) Hilbert Space Explorer (22375-23897) Users' Mathboxes (23898-32447)

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

Theoremcdleme20k 30801 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s2, f(s), t2, f(t). (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20l1 30802 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20l2 30803 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20l 30804 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20m 30805 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 30806 Combine cdleme19f 30790 and cdleme20m 30805 to eliminate condition. (Contributed by NM, 28-Nov-2012.)

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

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

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

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

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

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

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

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

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

Theoremcdleme21j 30818* Combine cdleme20 30806 and cdleme21i 30817 to eliminate condition. (Contributed by NM, 29-Nov-2012.)

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

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

Theoremcdleme22aa 30821 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 30822 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 30823 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 30824 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 30825 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)

Theoremcdleme22e 30826 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 30827 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 30828 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 30829 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 30828 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 30830 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 30831 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)

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

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

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

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

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

Theoremcdleme25c 30837* Transform cdleme25b 30836. (Contributed by NM, 1-Jan-2013.)

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

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

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

Theoremcdleme26e 30841* 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 30842* 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 30843* 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 30844* 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 30845* 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 30846* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 30844 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 30847* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 30844 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 30848* Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.)

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

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

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

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

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

Theoremcdleme28 30855* Quantified version of cdleme28c 30854. (Compare cdleme24 30834.) (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29ex 30856* Lemma for cdleme29b 30857. (Compare cdleme25a 30835.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29b 30857* Transform cdleme28 30855. (Compare cdleme25b 30836.) TODO: FIX COMMENT (Contributed by NM, 7-Feb-2013.)

Theoremcdleme29c 30858* Transform cdleme28b 30853. (Compare cdleme25c 30837.) TODO: FIX COMMENT (Contributed by NM, 8-Feb-2013.)

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

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

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

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

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

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

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

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

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

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

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

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