Home Metamath Proof ExplorerTheorem List (p. 314 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-32836)

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

Theoremcdlemefs45ee 31301* Explicit expansion of cdlemefs45 31300. TODO: use to shorten cdlemefs45 31300 uses? Should be assigned to a hypothesis letter? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.)

Theoremcdlemefs45eN 31302* Explicit expansion of cdlemefs45 31300. TODO: use to shorten cdlemefs45 31300 uses? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.)

Theoremcdleme32sn1awN 31303* Show that is an atom not under when . (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.)

Theoremcdleme41sn3a 31304* Show that is under when . (Contributed by NM, 19-Mar-2013.)

Theoremcdleme32sn2awN 31305* Show that is an atom not under when . (Contributed by NM, 6-Mar-2013.) (New usage is discouraged.)

Theoremcdleme32snaw 31306* Show that is an atom not under . (Contributed by NM, 6-Mar-2013.)

Theoremcdleme32snb 31307* Show closure of . (Contributed by NM, 1-Mar-2013.)

Theoremcdleme32fva 31308* Part of proof of Lemma D in [Crawley] p. 113. Value of at an atom not under . (Contributed by NM, 2-Mar-2013.)

Theoremcdleme32fva1 31309* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.)

Theoremcdleme32fvaw 31310* Show that is an atom not under when is an atom not under . (Contributed by NM, 18-Apr-2013.)

Theoremcdleme32fvcl 31311* Part of proof of Lemma D in [Crawley] p. 113. Closure of the function . (Contributed by NM, 10-Feb-2013.)

Theoremcdleme32a 31312* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.)

Theoremcdleme32b 31313* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.)

Theoremcdleme32c 31314* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.)

Theoremcdleme32d 31315* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)

Theoremcdleme32e 31316* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)

Theoremcdleme32f 31317* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)

Theoremcdleme32le 31318* Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.)

Theoremcdleme35a 31319 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35fnpq 31320 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)

Theoremcdleme35b 31321 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35c 31322 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35d 31323 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35e 31324 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35f 31325 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35g 31326 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.)

Theoremcdleme35h 31327 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)

Theoremcdleme35h2 31328 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)

Theoremcdleme35sn2aw 31329* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one outside of line case; compare cdleme32sn2awN 31305. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)

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

Theoremcdleme36a 31331 Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)

Theoremcdleme36m 31332 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.)

Theoremcdleme37m 31333 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)

Theoremcdleme38m 31334 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT (Contributed by NM, 13-Mar-2013.)

Theoremcdleme38n 31335 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT TODO shorter if proved directly from cdleme36m 31332 and cdleme37m 31333? (Contributed by NM, 14-Mar-2013.)

Theoremcdleme39a 31336 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT. , , , serve as f(t), f(u), ft(), ft(). Put hypotheses of cdleme38n 31335 in convention of cdleme32sn1awN 31303. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)

Theoremcdleme39n 31337 Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT. , , , serve as f(t), f(u), ft(), ft(). Put hypotheses of cdleme38n 31335 in convention of cdleme32sn1awN 31303. TODO see if this hypothesis conversion would be better if done earlier. (Contributed by NM, 15-Mar-2013.)

Theoremcdleme40m 31338* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT Use proof idea from cdleme32sn1awN 31303. (Contributed by NM, 18-Mar-2013.)

Theoremcdleme40n 31339* Part of proof of Lemma E in [Crawley] p. 113. Show that f(x) is one-to-one on line. TODO: FIX COMMENT TODO get rid of '.<' class? (Contributed by NM, 18-Mar-2013.)

Theoremcdleme40v 31340* Part of proof of Lemma E in [Crawley] p. 113. Change bound variables in (but we use for convenience since we have its hypotheses available) . (Contributed by NM, 18-Mar-2013.)

Theoremcdleme40w 31341* Part of proof of Lemma E in [Crawley] p. 113. Apply cdleme40v 31340 bound variable change to . TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)

Theoremcdleme42a 31342 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.)

Theoremcdleme42c 31343 Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.)

Theoremcdleme42d 31344 Part of proof of Lemma E in [Crawley] p. 113. Match . (Contributed by NM, 6-Mar-2013.)

Theoremcdleme41sn3aw 31345* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is different on and off the line. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)

Theoremcdleme41sn4aw 31346* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for on and off line. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)

Theoremcdleme41snaw 31347* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 31306. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)

Theoremcdleme41fva11 31348* Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is one-to-one for r in W (r an atom not under w). TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.)

Theoremcdleme42b 31349* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.)

Theoremcdleme42e 31350* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42f 31351* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42g 31352* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42h 31353* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42i 31354* Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.)

Theoremcdleme42k 31355* Part of proof of Lemma E in [Crawley] p. 113. Since F ' S =/= F'R when S =/= R (i.e. 1-1); then ( ( F ' R ) .\/ ( F ' S ) ) is 2-dim therefore = ( ( F ' R ) .\/ V ) by cdleme42i 31354 and ps-1 30348 TODO: FIX COMMENT (Contributed by NM, 20-Mar-2013.)

Theoremcdleme42ke 31356* Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT (Contributed by NM, 2-Apr-2013.)

Theoremcdleme42keg 31357* Part of proof of Lemma E in [Crawley] p. 113. Remove condition. TODO: FIX COMMENT TODO: Use instead of cdleme42ke 31356 and even combine with it? (Contributed by NM, 22-Apr-2013.)
<