HomeTheorem List (p. 340 of 410)
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. 340 of 410) | < 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-26627) |
Hilbert Space Explorer
(26628-28150) |
Users' Mathboxes
(28151-40909) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdleme17d1 33901 |
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.)
|
         
 ![./\](_.wedge.gif "./\"){kind=small}
       
 
   ![/\](wedge.gif "/\"){kind=small} 
 | ||
| Theorem | cdleme0nex 33902* |
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 33823- which is under w, so the only 2
left
not under w are p and q themselves.) Note that by cvlsupr2 32955, 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 33903 |
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 33904 |
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 33905* |
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 33906 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
 
| ||
| Theorem | cdleme18d 33907* |
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 33908 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
|
| ||
| Theorem | cdlemedb 33909 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
20-Nov-2012.)
|
|
| ||
| Theorem | cdlemeda 33910 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
13-Nov-2012.)
|
|
| ||
| Theorem | cdlemednpq 33911 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
18-Nov-2012.)
|
|
| ||
| Theorem | cdlemednuN 33912 |
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 33913 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
 | ||
| Theorem | cdleme20y 33914 | 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 33915 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) Obsolete version of cdleme20y 33914 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | cdleme19a 33916 |
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 33917 |
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 33918 |
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 33919 |
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 33920 |
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 33921 |
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 33922 |
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 33923 |
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 33924 |
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 33925 |
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 33926 |
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 33927 |
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 33928 |
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 33929 |
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 33930 |
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 33931 |
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 33932 |
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 33933 |
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 33934 |
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 33935 |
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 33936 |
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 33937 |
Combine cdleme19f 33921 and cdleme20m 33936 to eliminate
condition. (Contributed by NM,
28-Nov-2012.)
|
|
| ||
| Theorem | cdleme21a 33938 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
| ||
| Theorem | cdleme21b 33939 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21c 33940 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
|
| ||
| Theorem | cdleme21at 33941 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21ct 33942 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21d 33943 |
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 33944 |
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 33945 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21g 33946 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21h 33947* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21i 33948* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
|
| ||
| Theorem | cdleme21j 33949* |
Combine cdleme20 33937 and cdleme21i 33948 to eliminate
condition. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21 33950 |
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 33907 and
cdleme21j 33949 to eliminate existence condition, proving
fs(r) = ft(r)
with fewer conditions. (Contributed by NM, 29-Nov-2012.)
|
|
| ||
| Theorem | cdleme21k 33951 |
Eliminate condition in cdleme21 33950. (Contributed by NM,
26-Dec-2012.)
|
|
| ||
| Theorem | cdleme22aa 33952 |
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 33953 |
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 33954 |
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 33955 |
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 33956 | 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 33957 |
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 33958 |
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 33959 |
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 33960 |
Part of proof of Lemma E in [Crawley] p. 113.
cdleme22f 33959 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 33961 |
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 33962 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
 | ||
| Theorem | cdleme23b 33963 | 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 33964 | 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 33965* | Quantified version of cdleme21k 33951. (Contributed by NM, 26-Dec-2012.) |
| ||
| Theorem | cdleme25a 33966* | Lemma for cdleme25b 33967. (Contributed by NM, 1-Jan-2013.) |
|
| ||
| Theorem | cdleme25b 33967* |
Transform cdleme24 33965. TODO get rid of $d's on ,
(Contributed by NM, 1-Jan-2013.)
|
| ||
| Theorem | cdleme25c 33968* | Transform cdleme25b 33967. (Contributed by NM, 1-Jan-2013.) |
| ||
| Theorem | cdleme25dN 33969* | Transform cdleme25c 33968. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme25cl 33970* | Show closure of the unique element in cdleme25c 33968. (Contributed by NM, 2-Feb-2013.) |
 
| ||
| Theorem | cdleme25cv 33971* | Change bound variables in cdleme25c 33968. (Contributed by NM, 2-Feb-2013.) |
|
| ||
| Theorem | cdleme26e 33972* |
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 33973* |
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 33974* |
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.)
|
|
| ||