HomeTheorem List (p. 338 of 354)
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 354) | < 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-24265) |
Hilbert Space Explorer
(24266-25790) |
Users' Mathboxes
(25791-35368) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdleme19d 33701 |
Part of proof of Lemma E in [Crawley] p. 113,
5th paragraph on p. 114.
 ,  ,  represent s2, f(s), f(t). We prove f(s) 
s2 = f(s) f(t). (Contributed by NM, 14-Nov-2012.)
|
         
 ![./\](_.wedge.gif "./\"){kind=small}
       
 
 
   ![/\](wedge.gif "/\"){kind=small}
| ||
| Theorem | cdleme19e 33702 |
Part of proof of Lemma E in [Crawley] p. 113,
5th paragraph on p. 114,
line 2. , , , represent s2, f(s),
t2, f(t).
We prove f(s) s2=f(t) t2.
(Contributed by NM,
14-Nov-2012.)
|
|
| ||
| Theorem | cdleme19f 33703 |
Part of proof of Lemma E in [Crawley] p. 113,
5th paragraph on p. 114,
line 3. ,
,  , , ,
 represent s2,
f(s), fs(r), t2, f(t), ft(r). We
prove that if r  s
t, then ft(r) = ft(r). (Contributed by NM, 14-Nov-2012.)
|
|
| ||
| Theorem | cdleme20aN 33704 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114.
, , , represent s2, f(s),
t2, f(t).
(Contributed by NM, 14-Nov-2012.) (New usage is discouraged.)
|
| ||
| Theorem | cdleme20bN 33705 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114,
second line. ,
, , represent s2, f(s),
t2,
f(t). We show v s2 = v t2.
(Contributed by NM,
15-Nov-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cdleme20c 33706 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114,
second line. ,
, , represent s2, f(s),
t2,
f(t). (Contributed by NM, 15-Nov-2012.)
|
|
| ||
| Theorem | cdleme20d 33707 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114,
second line. ,
, , represent s2, f(s),
t2,
f(t). (Contributed by NM, 17-Nov-2012.)
|
|
| ||
| Theorem | cdleme20e 33708 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114,
4th line. ,
, , represent s2, f(s),
t2, f(t).
We show <f(s),s2,s> and
<f(t),t2,t> are centrally perspective.
(Contributed by NM, 17-Nov-2012.)
|
|
| ||
| Theorem | cdleme20f 33709 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114,
4th line. ,
, , represent s2, f(s),
t2, f(t).
We show <f(s),s2,s> and
<f(t),t2,t> are axially perspective.
(Contributed by NM, 17-Nov-2012.)
|
|
| ||
| Theorem | cdleme20g 33710 |
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,
18-Nov-2012.)
|
|
| ||
| Theorem | cdleme20h 33711 |
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,
18-Nov-2012.)
|
|
| ||
| Theorem | cdleme20i 33712 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114,
antepenultimate line. , , , represent s2, f(s),
t2, f(t). We show (f(s) s2) (f(t)
t2) p
q.
(Contributed by NM, 18-Nov-2012.)
|
|
| ||
| Theorem | cdleme20j 33713 |
Part of proof of Lemma E in [Crawley] p. 113,
last paragraph on p. 114.
, , , represent s2, f(s),
t2, f(t). We show
s2 t2.
(Contributed by NM, 18-Nov-2012.)
|
|
| ||
| Theorem | cdleme20k 33714 |
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.)
|
|
| ||
| Theorem | cdleme20l1 33715 |
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.)
|
 | ||
| Theorem | cdleme20l2 33716 |
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.)
|
|
| ||
| Theorem | cdleme20l 33717 |
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.)
|
|
| ||
| Theorem | cdleme20m 33718 |
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.)
|
|
| ||
| Theorem | cdleme20 33719 |
Combine cdleme19f 33703 and cdleme20m 33718 to eliminate
condition. (Contributed by NM,
28-Nov-2012.)
|
|
| ||
| Theorem | cdleme21a 33720 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
| ||
| Theorem | cdleme21b 33721 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21c 33722 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21at 33723 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21ct 33724 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21d 33725 |
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.)
|
|
| ||
| Theorem | cdleme21e 33726 |
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.)
|
|
| ||
| Theorem | cdleme21f 33727 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21g 33728 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21h 33729* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
 | ||
| Theorem | cdleme21i 33730* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
 | ||
| Theorem | cdleme21j 33731* |
Combine cdleme20 33719 and cdleme21i 33730 to eliminate
condition. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21 33732 |
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 33690 and
cdleme21j 33731 to eliminate existence condition, proving
fs(r) = ft(r)
with fewer conditions. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21k 33733 |
Eliminate condition in cdleme21 33732. (Contributed by NM,
26-Dec-2012.)
|
|
| ||
| Theorem | cdleme22aa 33734 |
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.)
|
|
| ||
| Theorem | cdleme22a 33735 |
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.)
|
|
| ||
| Theorem | cdleme22b 33736 |
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.)
|
|
| ||
| Theorem | cdleme22cN 33737 |
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.)
|
|
| ||
| Theorem | cdleme22d 33738 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.) |
|
| ||
| Theorem | cdleme22e 33739 |
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.)
|
|
| ||
| Theorem | cdleme22eALTN 33740 |
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.)
|
| ||
| Theorem | cdleme22f 33741 |
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.)
|
|
| ||
| Theorem | cdleme22f2 33742 |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme22f 33741 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.)
|
|
| ||
| Theorem | cdleme22g 33743 |
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.)
|
|
| ||
| Theorem | cdleme23a 33744 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
 | ||
| Theorem | cdleme23b 33745 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
|
| ||
| Theorem | cdleme23c 33746 | Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.) |
|
| ||
| Theorem | cdleme24 33747* | Quantified version of cdleme21k 33733. (Contributed by NM, 26-Dec-2012.) |
| ||
| Theorem | cdleme25a 33748* | Lemma for cdleme25b 33749. (Contributed by NM, 1-Jan-2013.) |
|
| ||
| Theorem | cdleme25b 33749* |
Transform cdleme24 33747. TODO get rid of $d's on ,
(Contributed by NM, 1-Jan-2013.)
|
| ||
| Theorem | cdleme25c 33750* | Transform cdleme25b 33749. (Contributed by NM, 1-Jan-2013.) |
| ||
| Theorem | cdleme25dN 33751* | Transform cdleme25c 33750. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme25cl 33752* | Show closure of the unique element in cdleme25c 33750. (Contributed by NM, 2-Feb-2013.) |
 
| ||
| Theorem | cdleme25cv 33753* | Change bound variables in cdleme25c 33750. (Contributed by NM, 2-Feb-2013.) |
|
| ||
| Theorem | cdleme26e 33754* |
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.)
|
|
| ||
| Theorem | cdleme26ee 33755* |
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.)
|
|
| ||
| Theorem | cdleme26eALTN 33756* |
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.)
|
|
| ||
| Theorem | cdleme26fALTN 33757* |
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.)
|
|
| ||
| Theorem | cdleme26f 33758* |
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.)
|
|
| ||
| Theorem | cdleme26f2ALTN 33759* |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme26fALTN 33757 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.)
|
|
| ||
| Theorem | cdleme26f2 33760* |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme26fALTN 33757 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.)
|
|
| ||
| Theorem | cdleme27cl 33761* |
Part of proof of Lemma E in [Crawley] p. 113.
Closure of  .
(Contributed by NM, 6-Feb-2013.)
|
| ||
| Theorem | cdleme27a 33762* |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme26f 33758 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.)
|
|
| ||
| Theorem | cdleme27b 33763* | Lemma for cdleme27N 33764. (Contributed by NM, 3-Feb-2013.) |
|
| ||
| Theorem | cdleme27N 33764* |
Part of proof of Lemma E in [Crawley] p. 113.
Eliminate the
antecedent in cdleme27a 33762. (Contributed by NM,
3-Feb-2013.) (New usage is discouraged.)
|
|
| ||
| Theorem | cdleme28a 33765* | Lemma for cdleme25b 33749. TODO: FIX COMMENT (Contributed by NM, 4-Feb-2013.) |
|
| ||