HomeTheorem List (p. 344 of 360)
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. 344 of 360) | < 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-24492) |
Hilbert Space Explorer
(24493-26017) |
Users' Mathboxes
(26018-35975) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemednpq 34301 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma. 
represents s2. (Contributed by NM,
18-Nov-2012.)
|
         
 ![./\](_.wedge.gif "./\"){kind=small}
      
    ![/\](wedge.gif "/\"){kind=small}     | ||
| Theorem | cdlemednuN 34302 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
18-Nov-2012.)
(New usage is discouraged.)
|
 | ||
| Theorem | cdleme20zN 34303 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
 | ||
| Theorem | cdleme20y 34304 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) |
|
| ||
| Theorem | cdleme19a 34305 |
Part of proof of Lemma E in [Crawley] p. 113,
5th paragraph on p. 114,
1st line.
represents s2. In their notation, we prove
that if r
 s  t, then s2=(s t) w.
(Contributed by NM,
13-Nov-2012.)
|
| ||
| Theorem | cdleme19b 34306 |
Part of proof of Lemma E in [Crawley] p. 113,
5th paragraph on p. 114,
1st line. ,
, represent s2, f(s), f(t). In their
notation, we prove that if r s t, then s2 f(s)
f(t).
(Contributed by NM, 13-Nov-2012.)
|
|
| ||
| Theorem | cdleme19c 34307 |
Part of proof of Lemma E in [Crawley] p. 113,
5th paragraph on p. 114,
1st line. ,
represent s2, f(s). We prove f(s)
s2. (Contributed by NM, 13-Nov-2012.)
|
|
| ||
| Theorem | cdleme19d 34308 |
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.)
|
|
| ||
| Theorem | cdleme19e 34309 |
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 34310 |
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 34311 |
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 34312 |
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 34313 |
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 34314 |
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 34315 |
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 34316 |
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 34317 |
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 34318 |
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 34319 |
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 34320 |
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 34321 |
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 34322 |
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 34323 |
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 34324 |
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 34325 |
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 34326 |
Combine cdleme19f 34310 and cdleme20m 34325 to eliminate
condition. (Contributed by NM,
28-Nov-2012.)
|
|
| ||
| Theorem | cdleme21a 34327 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
| ||
| Theorem | cdleme21b 34328 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21c 34329 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21at 34330 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21ct 34331 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21d 34332 |
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 34333 |
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 34334 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21g 34335 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21h 34336* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
 | ||
| Theorem | cdleme21i 34337* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
 | ||
| Theorem | cdleme21j 34338* |
Combine cdleme20 34326 and cdleme21i 34337 to eliminate
condition. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21 34339 |
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 34297 and
cdleme21j 34338 to eliminate existence condition, proving
fs(r) = ft(r)
with fewer conditions. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21k 34340 |
Eliminate condition in cdleme21 34339. (Contributed by NM,
26-Dec-2012.)
|
|
| ||
| Theorem | cdleme22aa 34341 |
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 34342 |
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 34343 |
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 34344 |
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 34345 | 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 34346 |
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 34347 |
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 34348 |
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 34349 |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme22f 34348 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 34350 |
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 34351 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
 | ||
| Theorem | cdleme23b 34352 | 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 34353 | 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 34354* | Quantified version of cdleme21k 34340. (Contributed by NM, 26-Dec-2012.) |
| ||
| Theorem | cdleme25a 34355* | Lemma for cdleme25b 34356. (Contributed by NM, 1-Jan-2013.) |
|
| ||
| Theorem | cdleme25b 34356* |
Transform cdleme24 34354. TODO get rid of $d's on ,
(Contributed by NM, 1-Jan-2013.)
|
| ||
| Theorem | cdleme25c 34357* | Transform cdleme25b 34356. (Contributed by NM, 1-Jan-2013.) |
| ||
| Theorem | cdleme25dN 34358* | Transform cdleme25c 34357. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme25cl 34359* | Show closure of the unique element in cdleme25c 34357. (Contributed by NM, 2-Feb-2013.) |
 
| ||
| Theorem | cdleme25cv 34360* | Change bound variables in cdleme25c 34357. (Contributed by NM, 2-Feb-2013.) |
|
| ||
| Theorem | cdleme26e 34361* |
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 34362* |
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 34363* |
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 34364* |
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 34365* |
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 34366* |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme26fALTN 34364 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 34367* |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme26fALTN 34364 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 34368* |
Part of proof of Lemma E in [Crawley] p. 113.
Closure of  .
(Contributed by NM, 6-Feb-2013.)
|
| ||
| Theorem | cdleme27a 34369* |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme26f 34365 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.)
|
|
| ||