HomeTheorem List (p. 338 of 394)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 338 of 394) | < 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-26406) |
Hilbert Space Explorer
(26407-27929) |
Users' Mathboxes
(27930-39313) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemefs32fvaN 33701* |
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 33307
here and elsewhere, and presence/absence of        term.
Also, why can proof be shortened with cdleme27cl 33645? What is difference
from cdlemefs27cl 33692? (Contributed by NM, 29-Mar-2013.)
(New usage is discouraged.)
|
       
 ![./\](_.wedge.gif "./\"){kind=small}
     
 
  
   ![/\](wedge.gif "/\"){kind=small}
 
  
  
 
  ![]_](_urbrack.gif "]_"){kind=small}
| ||
| Theorem | cdlemefs32fva1 33702* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 29-Mar-2013.) |
| ||
| Theorem | cdlemefs31fv1 33703* |
Value of when .
TODO This may be useful for shortening others that now use riotasv 32243
3d . TODO: FIX COMMENT.
***END OF VALUE AT ATOM STUFF TO REPLACE
ONES BELOW***
"cdleme3xsn1aw" decreased using "cdlemefs32sn1aw"
"cdleme32sn1aw" decreased from 3302 to 36 using "cdlemefs32sn1aw".
"cdleme32sn2aw" decreased from 1687 to 26 using "cdlemefr32sn2aw".
"cdleme32snaw" decreased from 376 to 375 using "cdlemefs32sn1aw".
"cdleme32snaw" decreased from 375 to 368 using "cdlemefr32sn2aw".
"cdleme35sn3a" decreased from 547 to 523 using "cdleme43frv1sn".
(Contributed by NM, 27-Mar-2013.)
|
 
| ||
| Theorem | cdlemefr44 33704* | Value of f(r) when r is an atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefr45 instead? TODO FIX COMMENT (Contributed by NM, 31-Mar-2013.) |
|
| ||
| Theorem | cdlemefs44 33705* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using more compact hypotheses. TODO: eliminate and use cdlemefs45 33708 instead TODO FIX COMMENT (Contributed by NM, 31-Mar-2013.) |
|
| ||
| Theorem | cdlemefr45 33706* | Value of f(r) when r is an atom not under pq, using very compact hypotheses. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
|
| ||
| Theorem | cdlemefr45e 33707* | Explicit expansion of cdlemefr45 33706. TODO: use to shorten cdlemefr45 33706 uses? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.) |
|
| ||
| Theorem | cdlemefs45 33708* | Value of fs(r) when r is an atom under pq and s is any atom not under pq, using very compact hypotheses. TODO FIX COMMENT (Contributed by NM, 1-Apr-2013.) |
|
| ||
| Theorem | cdlemefs45ee 33709* |
Explicit expansion of cdlemefs45 33708. TODO: use to shorten cdlemefs45 33708
uses? Should
be
assigned to a hypothesis letter? TODO FIX COMMENT (Contributed by NM,
10-Apr-2013.)
|
|
| ||
| Theorem | cdlemefs45eN 33710* | Explicit expansion of cdlemefs45 33708. TODO: use to shorten cdlemefs45 33708 uses? TODO FIX COMMENT (Contributed by NM, 10-Apr-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme32sn1awN 33711* |
Show that is an atom
not under when
. (Contributed by NM,
6-Mar-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdleme41sn3a 33712* |
Show that is under
when
. (Contributed by NM,
19-Mar-2013.)
|
|
| ||
| Theorem | cdleme32sn2awN 33713* |
Show that is an atom
not under when
. (Contributed by NM, 6-Mar-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdleme32snaw 33714* |
Show that is an atom
not under .
(Contributed
by NM, 6-Mar-2013.)
|
|
| ||
| Theorem | cdleme32snb 33715* |
Show closure of .
(Contributed by NM, 1-Mar-2013.)
|
|
| ||
| Theorem | cdleme32fva 33716* |
Part of proof of Lemma D in [Crawley] p. 113.
Value of at an atom
not under .
(Contributed by NM, 2-Mar-2013.)
|
|
| ||
| Theorem | cdleme32fva1 33717* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 2-Mar-2013.) |
|
| ||
| Theorem | cdleme32fvaw 33718* |
Show that is
an atom not under
when is an
atom not under . (Contributed by NM, 18-Apr-2013.)
|
|
| ||
| Theorem | cdleme32fvcl 33719* |
Part of proof of Lemma D in [Crawley] p. 113.
Closure of the function
. (Contributed
by NM, 10-Feb-2013.)
|
| ||
| Theorem | cdleme32a 33720* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
|
| ||
| Theorem | cdleme32b 33721* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
|
| ||
| Theorem | cdleme32c 33722* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 19-Feb-2013.) |
|
| ||
| Theorem | cdleme32d 33723* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme32e 33724* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme32f 33725* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme32le 33726* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 20-Feb-2013.) |
|
| ||
| Theorem | cdleme35a 33727 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35fnpq 33728 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
|
| ||
| Theorem | cdleme35b 33729 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35c 33730 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35d 33731 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35e 33732 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35f 33733 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35g 33734 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 10-Mar-2013.) |
|
| ||
| Theorem | cdleme35h 33735 |
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.)
|
| ||
| Theorem | cdleme35h2 33736 |
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.)
|
|
| ||
| Theorem | cdleme35sn2aw 33737* |
Part of proof of Lemma E in [Crawley] p. 113.
Show that f(x) is
one-to-one outside of line case; compare cdleme32sn2awN 33713.
TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.)
|
|
| ||
| Theorem | cdleme35sn3a 33738* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 19-Mar-2013.) |
|
| ||
| Theorem | cdleme36a 33739 | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT (Contributed by NM, 11-Mar-2013.) |
|
| ||
| Theorem | cdleme36m 33740 |
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.)
|
| ||
| Theorem | cdleme37m 33741 |
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.)
|
| ||
| Theorem | cdleme38m 33742 |
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.)
|
|
| ||
| Theorem | cdleme38n 33743 |
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 33740 and cdleme37m 33741? (Contributed by NM,
14-Mar-2013.)
|
|
| ||
| Theorem | cdleme39a 33744 |
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 33743 in convention of cdleme32sn1awN 33711. TODO
see if this hypothesis conversion would be better if done earlier.
(Contributed by NM, 15-Mar-2013.)
|
|
| ||
| Theorem | cdleme39n 33745 |
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 33743 in convention of cdleme32sn1awN 33711. TODO see
if this hypothesis conversion would be better if done earlier.
(Contributed by NM, 15-Mar-2013.)
|
|
| ||
| Theorem | cdleme40m 33746* |
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 33711. (Contributed by NM, 18-Mar-2013.)
|
 
| ||
| Theorem | cdleme40n 33747* |
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.)
|
| ||
| Theorem | cdleme40v 33748* |
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.)
|
|
| ||
| Theorem | cdleme40w 33749* |
Part of proof of Lemma E in [Crawley] p. 113.
Apply cdleme40v 33748 bound
variable change to .
TODO: FIX COMMENT (Contributed
by NM, 19-Mar-2013.)
|
|
| ||
| Theorem | cdleme42a 33750 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 3-Mar-2013.) |
|
| ||
| Theorem | cdleme42c 33751 |
Part of proof of Lemma E in [Crawley] p. 113.
Match .
(Contributed by NM, 6-Mar-2013.)
|
|
| ||
| Theorem | cdleme42d 33752 |
Part of proof of Lemma E in [Crawley] p. 113.
Match
. (Contributed by NM, 6-Mar-2013.)
|
|
| ||
| Theorem | cdleme41sn3aw 33753* |
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.)
|
|
| ||
| Theorem | cdleme41sn4aw 33754* |
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.)
|
|
| ||
| Theorem | cdleme41snaw 33755* | Part of proof of Lemma E in [Crawley] p. 113. Show that f(r) is for combined cases; compare cdleme32snaw 33714. TODO: FIX COMMENT (Contributed by NM, 18-Mar-2013.) |
|
| ||
| Theorem | cdleme41fva11 33756* | 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.) |
|
| ||
| Theorem | cdleme42b 33757* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 6-Mar-2013.) |
|
| ||
| Theorem | cdleme42e 33758* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Mar-2013.) |
|
| ||