HomeTheorem List (p. 336 of 393)
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. 336 of 393) | < 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-26397) |
Hilbert Space Explorer
(26398-27920) |
Users' Mathboxes
(27921-39291) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdleme3fa 33501 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 33502. (Contributed by NM, 6-Oct-2012.) |
         
 ![./\](_.wedge.gif "./\"){kind=small}
       
  
   ![/\](wedge.gif "/\"){kind=small}  
 | ||
| Theorem | cdleme3 33502 |
Part of proof of Lemma E in [Crawley] p. 113.
represents f(r).
is the
fiducial co-atom (hyperplane) w. Here and in cdleme3fa 33501
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 33494 through cdleme3 33502, so there may be a simpler
proof that we have overlooked. (Contributed by NM, 7-Jun-2012.)
|
|
| ||
| Theorem | cdleme4 33503 |
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 33504 |
Part of proof of Lemma E in [Crawley] p. 114
top. represents
fs(r). Auxiliary lemma derived from
cdleme5 33505. We show fs(r) 
p q.
(Contributed by NM, 10-Nov-2012.)
|
| ||
| Theorem | cdleme5 33505 |
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 33506 |
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 33507 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33513 and cdleme7 33514. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7a 33508 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33513 and cdleme7 33514. (Contributed by NM, 7-Jun-2012.) |
 | ||
| Theorem | cdleme7b 33509 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33513 and cdleme7 33514. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7c 33510 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33513 and cdleme7 33514. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7d 33511 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33513 and cdleme7 33514. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7e 33512 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 33513 and cdleme7 33514. (Contributed by NM, 8-Jun-2012.) |
 | ||
| Theorem | cdleme7ga 33513 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 33514. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7 33514 |
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 33513 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 33507 through cdleme7 33514, so there may be a simpler proof that
we have overlooked. (Contributed by NM, 9-Jun-2012.)
|
|
| ||
| Theorem | cdleme8 33515 |
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 33516 |
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 33517 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
 
| ||
| Theorem | cdleme9 33518 |
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 33519 |
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 33520 |
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 33521 |
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 33522 |
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 33523 |
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 33524 |
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 33525 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 12-Jun-2012.) |
|
| ||
| Theorem | cdleme11c 33526 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme11dN 33527 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme11e 33528 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme11fN 33529 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme11g 33530 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11h 33531 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11j 33532 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11k 33533 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | cdleme11l 33534 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 33535. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | cdleme11 33535 |
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 33525
through cdleme11 33535, so there may be a simpler proof that we
have
overlooked. (Contributed by NM, 15-Jun-2012.)
|
|
| ||
| Theorem | cdleme12 33536 |
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 33537 |
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 33538 |
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 33150 to cdleme13 33537. and
represent f(s) and f(t)
respectively. (Contributed by NM, 8-Oct-2012.)
|
|
| ||
| Theorem | cdleme15a 33539 |
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 33540 |
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 33541 |
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 33542 |
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 33543 |
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 33544 |
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 33545 |
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 33546 |
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 33547 |
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 33548 |
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 33549 |
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 33550 |
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 33551 |
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 33552 | Lemma leading to cdleme17c 33553. (Contributed by NM, 11-Oct-2012.) |
|
| ||
| Theorem | cdleme17c 33553 |
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 33554 |
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 33555* |
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 33476- which is under w, so the only 2
left
not under w are p and q themselves.) Note that by cvlsupr2 32608, 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 33556 |
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 33557 |
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 33558* |
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 33559 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
|
| ||
| Theorem | cdleme18d 33560* |
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 33561 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
|
| ||
| Theorem | cdlemedb 33562 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
20-Nov-2012.)
|
|
| ||
| Theorem | cdlemeda 33563 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
13-Nov-2012.)
|
|
| ||
| Theorem | cdlemednpq 33564 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
18-Nov-2012.)
|
|
| ||
| Theorem | cdlemednuN 33565 |
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 33566 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme20y 33567 | 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 33568 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) Obsolete version of cdleme20y 33567 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | cdleme19a 33569 |
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 33570 |
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 33571 |
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 33572 |
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 33573 |
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 33574 |
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 33575 |
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 33576 |
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 33577 |
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 33578 |
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 33579 |
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 33580 |
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 33581 |
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 33582 |
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 33583 |
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 33584 |
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 | |