HomeTheorem List (p. 356 of 426)
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. 356 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdleme0cp 35501 | Part of proof of Lemma E in [Crawley] p. 113. TODO: Reformat as in cdlemg3a 35885- swap consequent equality; make antecedent use df-3an 1039. (Contributed by NM, 13-Jun-2012.) |
         
 ![./\](_.wedge.gif "./\"){kind=small}
       
    ![/\](wedge.gif "/\"){kind=small} 
| ||
| Theorem | cdleme0cq 35502 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Apr-2013.) |
|
| ||
| Theorem | cdleme0dN 35503 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
 
| ||
| Theorem | cdleme0e 35504 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme0fN 35505 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme0gN 35506 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemeulpq 35507 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Dec-2012.) |
|
| ||
| Theorem | cdleme01N 35508 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme02N 35509 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme0ex1N 35510* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
 
| ||
| Theorem | cdleme0ex2N 35511* |
Part of proof of Lemma E in [Crawley] p. 113.
Note that
is a shorter way to express
. (Contributed by NM,
9-Nov-2012.) (New usage is discouraged.)
|
|
| ||
| Theorem | cdleme0moN 35512* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
 
 | ||
| Theorem | cdleme1b 35513 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma showing
 is a lattice
element. represents
their f(r). (Contributed
by NM, 6-Jun-2012.)
|
 
| ||
| Theorem | cdleme1 35514 |
Part of proof of Lemma E in [Crawley] p. 113.
represents their
f(r). Here we show r f(r) = r u (7th through 5th lines
from bottom on p. 113). (Contributed by NM, 4-Jun-2012.)
|
|
| ||
| Theorem | cdleme2 35515 |
Part of proof of Lemma E in [Crawley] p. 113.
represents f(r).
is the
fiducial co-atom (hyperplane) w. Here we show that (r
f(r)) w = u in their
notation (4th line from bottom on
p. 113). (Contributed by NM, 5-Jun-2012.)
|
|
| ||
| Theorem | cdleme3b 35516 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. (Contributed by NM, 6-Jun-2012.) |
|
| ||
| Theorem | cdleme3c 35517 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. (Contributed by NM, 6-Jun-2012.) |
  | ||
| Theorem | cdleme3d 35518 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. (Contributed by NM, 6-Jun-2012.) |
|
| ||
| Theorem | cdleme3e 35519 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. (Contributed by NM, 6-Jun-2012.) |
|
| ||
| Theorem | cdleme3fN 35520 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. TODO: Delete - duplicates cdleme0e 35504. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme3g 35521 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme3h 35522 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 35523 and cdleme3 35524. (Contributed by NM, 6-Jun-2012.) |
|
| ||
| Theorem | cdleme3fa 35523 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 35524. (Contributed by NM, 6-Oct-2012.) |
|
| ||
| Theorem | cdleme3 35524 |
Part of proof of Lemma E in [Crawley] p. 113.
represents f(r).
is the
fiducial co-atom (hyperplane) w. Here and in cdleme3fa 35523
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 35516 through cdleme3 35524, so there may be a simpler
proof that we have overlooked. (Contributed by NM, 7-Jun-2012.)
|
|
| ||
| Theorem | cdleme4 35525 |
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 35526 |
Part of proof of Lemma E in [Crawley] p. 114
top. represents
fs(r). Auxiliary lemma derived from
cdleme5 35527. We show fs(r) 
p q.
(Contributed by NM, 10-Nov-2012.)
|
| ||
| Theorem | cdleme5 35527 |
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 35528 |
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 35529 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35535 and cdleme7 35536. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7a 35530 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35535 and cdleme7 35536. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7b 35531 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35535 and cdleme7 35536. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7c 35532 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35535 and cdleme7 35536. (Contributed by NM, 7-Jun-2012.) |
|
| ||
| Theorem | cdleme7d 35533 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35535 and cdleme7 35536. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7e 35534 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 35535 and cdleme7 35536. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7ga 35535 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 35536. (Contributed by NM, 8-Jun-2012.) |
|
| ||
| Theorem | cdleme7 35536 |
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 35535 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 35529 through cdleme7 35536, so there may be a simpler proof that
we have overlooked. (Contributed by NM, 9-Jun-2012.)
|
|
| ||
| Theorem | cdleme8 35537 |
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 35538 |
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 35539 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
|
| ||
| Theorem | cdleme9 35540 |
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 35541 |
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 35542 |
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 35543 |
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 35544 |
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 35545 |
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 35546 |
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 35547 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 12-Jun-2012.) |
|
| ||
| Theorem | cdleme11c 35548 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme11dN 35549 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme11e 35550 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 13-Jun-2012.) |
|
| ||
| Theorem | cdleme11fN 35551 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme11g 35552 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11h 35553 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11j 35554 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 14-Jun-2012.) |
|
| ||
| Theorem | cdleme11k 35555 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | cdleme11l 35556 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 35557. (Contributed by NM, 15-Jun-2012.) |
|
| ||
| Theorem | cdleme11 35557 |
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 35547
through cdleme11 35557, so there may be a simpler proof that we
have
overlooked. (Contributed by NM, 15-Jun-2012.)
|
|
| ||
| Theorem | cdleme12 35558 |
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 35559 |
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 35560 |
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 35172 to cdleme13 35559. and
represent f(s) and f(t)
respectively. (Contributed by NM, 8-Oct-2012.)
|
|
| ||
| Theorem | cdleme15a 35561 |
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 35562 |
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 35563 |
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 35564 |
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 35565 |
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 35566 |
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 35567 |
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 35568 |
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 35569 |
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 35570 |
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 35571 |
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 35572 |
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 35573 |
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 35574 | Lemma leading to cdleme17c 35575. (Contributed by NM, 11-Oct-2012.) |
|
| ||
| Theorem | cdleme17c 35575 |
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 35576 |
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 35577* |
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 35498- which is under w, so the only 2 left not
under w are p and
q themselves.) Note that by cvlsupr2 34630, 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 35578 |
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 35579 |
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 35580* |
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 35581 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
|
| ||
| Theorem | cdleme18d 35582* |
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 35583 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
|
| ||
| Theorem | cdlemedb 35584 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
20-Nov-2012.)
|
|
| ||
| Theorem | cdlemeda 35585 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
13-Nov-2012.)
|
|
| ||
| Theorem | cdlemednpq 35586 |
Part of proof of Lemma E in [Crawley] p. 113.
Utility lemma.
represents s2. (Contributed by NM,
18-Nov-2012.)
|
|
| ||
| Theorem | cdlemednuN 35587 |
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 35588 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
|
| ||
| Theorem | cdleme20y 35589 | 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 35590 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) Obsolete version of cdleme20y 35589 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.) |
|
| ||
| Theorem | cdleme19a 35591 |
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 35592 |
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 35593 |
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 35594 |
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 35595 |
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 35596 |
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 35597 |
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 35598 |
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 35599 |
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 35600 |
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.)
|
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |