HomeTheorem List (p. 365 of 385)
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. 365 of 385) | < 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-26033) |
Hilbert Space Explorer
(26034-27558) |
Users' Mathboxes
(27559-38473) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdleme16b 36401 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
first part of 3rd sentence.  and 
represent f(s) and f(t)
respectively. It is unclear how this follows from s  u  t
u, as the
authors state, and we used a different proof. (Note:
the antecedent         is not used.) (Contributed
by
NM, 11-Oct-2012.)
|
     
 ![./\](_.wedge.gif "./\"){kind=small}
     
 
   ![/\](wedge.gif "/\"){kind=small}
 | ||
| Theorem | cdleme16c 36402 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
2nd part of 3rd sentence. and
represent f(s) and f(t)
respectively. We show, in their notation, s t f(s)
f(t)=s t
u. (Contributed by
NM, 11-Oct-2012.)
|
|
| ||
| Theorem | cdleme16d 36403 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
3rd part of 3rd sentence. and
represent f(s) and f(t)
respectively. We show, in their notation, (s t) (f(s)
f(t)) is an
atom. (Contributed by NM, 11-Oct-2012.)
|
|
| ||
| Theorem | cdleme16e 36404 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
3rd part of 3rd sentence. and
represent f(s) and f(t)
respectively. We show, in their notation, (s t) (f(s)
f(t))=(s
t) w. (Contributed by
NM,
11-Oct-2012.)
|
|
| ||
| Theorem | cdleme16f 36405 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
3rd part of 3rd sentence. and
represent f(s) and f(t)
respectively. We show, in their notation, (s t) (f(s)
f(t))=(f(s)
f(t)) w. (Contributed by
NM,
11-Oct-2012.)
|
|
| ||
| Theorem | cdleme16g 36406 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
Eq. (1). and
represent f(s) and
f(t) respectively. We
show, in their notation, (s t) w=(f(s)
f(t))
w. (Contributed by NM, 11-Oct-2012.)
|
|
| ||
| Theorem | cdleme16 36407 |
Part of proof of Lemma E in [Crawley] p. 113,
conclusion of 3rd
paragraph on p. 114. and
represent f(s) and f(t)
respectively. We show, in their notation, (s t) w=(f(s)
f(t)) w, whether or not u
 s t. (Contributed
by NM, 11-Oct-2012.)
|
|
| ||
| Theorem | cdleme17a 36408 |
Part of proof of Lemma E in [Crawley] p. 114,
first part of 4th
paragraph. ,
, and  represent f(s),
fs(p), and s1
respectively. We show, in their notation, fs(p)=(p q)
(q
s1). (Contributed by NM, 11-Oct-2012.)
|
|
| ||
| Theorem | cdleme17b 36409 | Lemma leading to cdleme17c 36410. (Contributed by NM, 11-Oct-2012.) |
|
| ||
| Theorem | cdleme17c 36410 |
Part of proof of Lemma E in [Crawley] p. 114,
first part of 4th
paragraph.
represents s1. We show, in their notation,
(p
q) (q s1)=q. (Contributed by NM,
11-Oct-2012.)
|
|
| ||
| Theorem | cdleme17d1 36411 |
Part of proof of Lemma E in [Crawley] p. 114,
first part of 4th
paragraph. ,
represent f(s),
fs(p) respectively. We show,
in their notation, fs(p)=q.
(Contributed by NM, 11-Oct-2012.)
|
|
| ||
| Theorem | cdleme0nex 36412* |
Part of proof of Lemma E in [Crawley] p. 114,
4th line of 4th
paragraph. Whenever (in their terminology) p q/0 (i.e. the
sublattice from 0 to p q) contains precisely three atoms, any
atom not under w must equal either p or q. (In case of 3 atoms, one of
them must be u - see cdleme0a 36333- which is under w, so the only 2
left
not under w are p and q themselves.) Note that by cvlsupr2 35465, our
 is a shorter way to express
. Thus, the negated
existential condition states there are no atoms different from p or q
that are also not under w. (Contributed by NM, 12-Nov-2012.)
|
 
| ||
| Theorem | cdleme18a 36413 |
Part of proof of Lemma E in [Crawley] p. 114,
2nd sentence of 4th
paragraph. ,
represent f(s),
fs(q) respectively. We show
fs(q) w. (Contributed by NM, 12-Oct-2012.)
|
|
| ||
| Theorem | cdleme18b 36414 |
Part of proof of Lemma E in [Crawley] p. 114,
2nd sentence of 4th
paragraph. ,
represent f(s),
fs(q) respectively. We show
fs(q) q. (Contributed by NM, 12-Oct-2012.)
|
|
| ||
| Theorem | cdleme18c 36415* |
Part of proof of Lemma E in [Crawley] p. 114,
2nd sentence of 4th
paragraph. ,
represent f(s),
fs(q) respectively. We show
fs(q) = p whenever p q has three atoms under it (implied
by the negated existential condition). (Contributed by NM,
10-Nov-2012.)
|
|
| ||
| Theorem | cdleme22gb 36416 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
 
| ||
| Theorem | cdleme18d 36417* |
Part of proof of Lemma E in [Crawley] p. 114,
4th sentence of 4th
paragraph. ,
,  ,  represent f(s), fs(r),
f(t),
ft(r) respectively. We show
fs(r)=ft(r)
for all possible r (which
must equal p or q in the case of exactly 3 atoms in p q/0 i.e.
when ...). (Contributed by NM, 12-Nov-2012.)
|
|
| ||
| Theorem | cdlemesner 36418 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
|
| ||
| Theorem | cdlemedb 36419 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
20-Nov-2012.)
|
|
| ||
| Theorem | cdlemeda 36420 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
13-Nov-2012.)
|
|
| ||
| Theorem | cdlemednpq 36421 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
18-Nov-2012.)
|
|
| ||
| Theorem | cdlemednuN 36422 |
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 36423 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
 | ||
| Theorem | cdleme20y 36424 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (Proof shortened by OpenAI, 25-Mar-2020.) |
|
| ||
| Theorem | cdleme20yOLD 36425 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) Obsolete version of cdleme20y 36424 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | cdleme19a 36426 |
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 36427 |
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 36428 |
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 36429 |
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 36430 |
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 36431 |
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 36432 |
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 36433 |
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 36434 |
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 36435 |
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 36436 |
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 36437 |
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 36438 |
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 36439 |
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 36440 |
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 36441 |
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 36442 |
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 36443 |
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 36444 |
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 36445 |
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 36446 |
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 36447 |
Combine cdleme19f 36431 and cdleme20m 36446 to eliminate
condition. (Contributed by NM,
28-Nov-2012.)
|
|
| ||
| Theorem | cdleme21a 36448 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
| ||
| Theorem | cdleme21b 36449 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21c 36450 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21at 36451 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21ct 36452 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21d 36453 |
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 36454 |
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 36455 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21g 36456 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21h 36457* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21i 36458* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21j 36459* |
Combine cdleme20 36447 and cdleme21i 36458 to eliminate
condition. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21 36460 |
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 36417 and
cdleme21j 36459 to eliminate existence condition, proving
fs(r) = ft(r)
with fewer conditions. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21k 36461 |
Eliminate condition in cdleme21 36460. (Contributed by NM,
26-Dec-2012.)
|
|
| ||
| Theorem | cdleme22aa 36462 |
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 36463 |
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 36464 |
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 36465 |
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 36466 | 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 36467 |
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 36468 |
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 36469 |
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 36470 |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme22f 36469 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 36471 |
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 36472 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
 | ||
| Theorem | cdleme23b 36473 | 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 36474 | 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 36475* | Quantified version of cdleme21k 36461. (Contributed by NM, 26-Dec-2012.) |
| ||