HomeTheorem List (p. 358 of 377)
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. 358 of 377) | < 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-25811) |
Hilbert Space Explorer
(25812-27336) |
Users' Mathboxes
(27337-37662) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdleme3fa 35701 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 35702. (Contributed by NM, 6-Oct-2012.) |
         
 ![./\](_.wedge.gif "./\"){kind=small}
       
  
   ![/\](wedge.gif "/\"){kind=small}  
 | ||
| Theorem | cdleme3 35702 |
Part of proof of Lemma E in [Crawley] p. 113.
represents f(r).
is the
fiducial co-atom (hyperplane) w. Here and in cdleme3fa 35701
above, we show that f(r) W (4th line from bottom on p. 113),
meaning it is an atom and not under w, which in our notation is
expressed as
. Their proof provides no
details
of our lemmas cdleme3b 35694 through cdleme3 35702, so there may be a simpler
proof that we have overlooked. (Contributed by NM, 7-Jun-2012.)
|
|
| ||
| Theorem | cdleme4 35703 |
Part of proof of Lemma E in [Crawley] p. 113.
and  represent
f(s) and fs(r). Here show p  q = r u at the top of
p. 114. (Contributed by NM, 7-Jun-2012.)
|
|
| ||
| Theorem | cdleme4a 35704 |
Part of proof of Lemma E in [Crawley] p. 114
top. represents
fs(r). Auxiliary lemma derived from
cdleme5 35705. We show fs(r) 
p q.
(Contributed by NM, 10-Nov-2012.)
|
| ||
| Theorem | cdleme5 35705 |
Part of proof of Lemma E in [Crawley] p. 113.
represents
fs(r).
We show r
fs(r)) = p q at the top of p. 114.
(Contributed by NM, 7-Jun-2012.)
|
|
| ||
| Theorem | cdleme6 35706 |
Part of proof of Lemma E in [Crawley] p. 113.
This expresses (r
fs(r)) w = u at the top of p. 114. (Contributed by
NM,
7-Jun-2012.)
|
|
| ||
| Theorem | cdleme7aa 35707 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35713 and cdleme7 35714. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7a 35708 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35713 and cdleme7 35714. (Contributed by NM, 7-Jun-2012.) |
 | ||
| Theorem | cdleme7b 35709 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35713 and cdleme7 35714. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7c 35710 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35713 and cdleme7 35714. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7d 35711 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35713 and cdleme7 35714. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7e 35712 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35713 and cdleme7 35714. (Contributed by NM, 8-Jun-2012.) |
 | ||
| Theorem | cdleme7ga 35713 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 35714. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7 35714 |
Part of proof of Lemma E in [Crawley] p. 113.
and represent
fs(r) and f(s) respectively. is the fiducial co-atom
(hyperplane)
that they call w. Here and in cdleme7ga 35713 above, we show that fs(r)
W (top of p.
114), meaning it is an atom and not under w, which
in our notation is expressed as
. (Note that
we do not have a symbol for their W.) Their proof provides no details of
our cdleme7aa 35707 through cdleme7 35714, so there may be a simpler proof that
we have overlooked. (Contributed by NM, 9-Jun-2012.)
|
|
| ||
| Theorem | cdleme8 35715 |
Part of proof of Lemma E in [Crawley] p. 113,
2nd paragraph on p. 114.
 represents
s1. In their notation, we prove p s1 = p
s.
(Contributed by NM, 9-Jun-2012.)
|
|
| ||
| Theorem | cdleme9a 35716 |
Part of proof of Lemma E in [Crawley] p. 113.
represents
s1,
which we prove is an atom. (Contributed by NM, 10-Jun-2012.)
|
|
| ||
| Theorem | cdleme9b 35717 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
 
| ||
| Theorem | cdleme9 35718 |
Part of proof of Lemma E in [Crawley] p. 113,
2nd paragraph on p. 114.
and represent s1 and f(s) respectively. In their notation,
we prove f(s) s1 = q s1.
(Contributed by NM,
10-Jun-2012.)
|
|
| ||
| Theorem | cdleme10 35719 |
Part of proof of Lemma E in [Crawley] p. 113,
2nd paragraph on p. 114.
 represents
s2. In their notation, we prove s s2 = s
r.
(Contributed by NM, 9-Jun-2012.)
|
|
| ||
| Theorem | cdleme8tN 35720 |
Part of proof of Lemma E in [Crawley] p. 113,
2nd paragraph on p. 114.
 represents
t1. In their notation, we prove p t1 = p
t.
(Contributed by NM, 8-Oct-2012.)
(New usage is discouraged.)
|
| ||
| Theorem | cdleme9taN 35721 |
Part of proof of Lemma E in [Crawley] p. 113.
represents
t1,
which we prove is an atom. (Contributed by NM, 8-Oct-2012.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdleme9tN 35722 |
Part of proof of Lemma E in [Crawley] p. 113,
2nd paragraph on p. 114.
and represent t1 and f(t) respectively. In their notation,
we prove f(t) t1 = q t1.
(Contributed by NM,
8-Oct-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cdleme10tN 35723 |
Part of proof of Lemma E in [Crawley] p. 113,
2nd paragraph on p. 114.
 represents
t2. In their notation, we prove t t2 = t
r.
(Contributed by NM, 8-Oct-2012.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdleme16aN 35724 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
showing, in their notation, s u t u.
(Contributed
by NM, 9-Oct-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cdleme11a 35725 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 12-Jun-2012.) |
|
| ||
| Theorem | cdleme11c 35726 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme11dN 35727 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme11e 35728 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme11fN 35729 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme11g 35730 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11h 35731 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11j 35732 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11k 35733 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | cdleme11l 35734 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35735. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | cdleme11 35735 |
Part of proof of Lemma E in [Crawley] p. 113,
1st sentence of 3rd
paragraph on p. 114. and
represent f(s) and f(t)
respectively. Their proof provides no details of our cdleme11a 35725
through cdleme11 35735, so there may be a simpler proof that we
have
overlooked. (Contributed by NM, 15-Jun-2012.)
|
|
| ||
| Theorem | cdleme12 35736 |
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. (Contributed by NM, 16-Jun-2012.)
|
|
| ||
| Theorem | cdleme13 35737 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
"<s,t,p> and <f(s),f(t),q> are centrally
perspective."
and
represent f(s) and f(t) respectively. (Contributed by NM,
7-Oct-2012.)
|
|
| ||
| Theorem | cdleme14 35738 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
"<s,t,p> and <f(s),f(t),q> ... are axially
perspective." We apply
dalaw 35350 to cdleme13 35737. and
represent f(s) and f(t)
respectively. (Contributed by NM, 8-Oct-2012.)
|
|
| ||
| Theorem | cdleme15a 35739 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
showing, in their notation, ((s p) (f(s)
q))
((t p) (f(t) q))=((p s1) (q
s1)) ((p t1) (q t1)). We
represent f(s), f(t), s1, and
t1 with , ,
, and
respectively. The order of our operations is slightly
different. (Contributed by NM, 9-Oct-2012.)
|
|
| ||
| Theorem | cdleme15b 35740 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
showing, in their notation, (p s1) (q s1)=s1.
We represent s1 with . (Contributed by NM,
10-Oct-2012.)
|
|
| ||
| Theorem | cdleme15c 35741 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
showing, in their notation, ((p s1) (q s1))
((p t1) (q
t1))=s1
t1.
and
represent s1 and t1 respectively. The order of our
operations is slightly different. (Contributed by NM,
10-Oct-2012.)
|
|
| ||
| Theorem | cdleme15d 35742 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
showing, in their notation, s1 t1 w. and
represent s1 and t1 respectively. The order of our operations is
slightly different. (Contributed by NM, 10-Oct-2012.)
|
|
| ||
| Theorem | cdleme15 35743 |
Part of proof of Lemma E in [Crawley] p. 113,
3rd paragraph on p. 114,
showing, in their notation, (s t) (f(s)
f(t))
w. We
use , for f(s), f(t)
respectively.
(Contributed by NM, 10-Oct-2012.)
|
|
| ||
| Theorem | cdleme16b 35744 |
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.)
|
|
| ||
| Theorem | cdleme16c 35745 |
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 35746 |
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 35747 |
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 35748 |
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 35749 |
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 35750 |
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 35751 |
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 35752 | Lemma leading to cdleme17c 35753. (Contributed by NM, 11-Oct-2012.) |
|
| ||
| Theorem | cdleme17c 35753 |
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 35754 |
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 35755* |
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 35676- which is under w, so the only 2
left
not under w are p and q themselves.) Note that by cvlsupr2 34808, 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 35756 |
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 35757 |
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 35758* |
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 35759 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
|
| ||
| Theorem | cdleme18d 35760* |
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 35761 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
|
| ||
| Theorem | cdlemedb 35762 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
20-Nov-2012.)
|
|
| ||
| Theorem | cdlemeda 35763 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
13-Nov-2012.)
|
|
| ||
| Theorem | cdlemednpq 35764 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
18-Nov-2012.)
|
|
| ||
| Theorem | cdlemednuN 35765 |
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 35766 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme20y 35767 | 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 35768 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) Obsolete version of cdleme20y 35767 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | cdleme19a 35769 |
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 35770 |
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 35771 |
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 35772 |
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 35773 |
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 35774 |
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 35775 |
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 35776 |
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 35777 |
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 35778 |
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 35779 |
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 35780 |
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 35781 |
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 35782 |
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 35783 |
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 35784 |
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 | |