Home | Metamath
Proof Explorer Theorem List (p. 311 of 327) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-22413) |
Hilbert Space Explorer
(22414-23936) |
Users' Mathboxes
(23937-32699) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme11j 31001 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31004. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11k 31002 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31004. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme11l 31003 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31004. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme11 31004 | 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 30994 through cdleme11 31004, so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme12 31005 | 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 31006 | 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 31007 | 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 30620 to cdleme13 31006. and represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.) |
Theorem | cdleme15a 31008 | 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 s_{1}) (q s_{1})) ((p t_{1}) (q t_{1})). We represent f(s), f(t), s_{1}, and t_{1} with , , , and respectively. The order of our operations is slightly different. (Contributed by NM, 9-Oct-2012.) |
Theorem | cdleme15b 31009 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, (p s_{1}) (q s_{1})=s_{1}. We represent s_{1} with . (Contributed by NM, 10-Oct-2012.) |
Theorem | cdleme15c 31010 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, ((p s_{1}) (q s_{1})) ((p t_{1}) (q t_{1}))=s_{1} t_{1}. and represent s_{1} and t_{1} respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.) |
Theorem | cdleme15d 31011 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph on p. 114, showing, in their notation, s_{1} t_{1} w. and represent s_{1} and t_{1} respectively. The order of our operations is slightly different. (Contributed by NM, 10-Oct-2012.) |
Theorem | cdleme15 31012 | 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 31013 | 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 31014 | 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 31015 | 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 31016 | 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 31017 | 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 31018 | 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 31019 | 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 31020 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , , and represent f(s), f_{s}(p), and s_{1} respectively. We show, in their notation, f_{s}(p)=(p q) (q s_{1}). (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17b 31021 | Lemma leading to cdleme17c 31022. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17c 31022 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. represents s_{1}. We show, in their notation, (p q) (q s_{1})=q. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17d1 31023 | Part of proof of Lemma E in [Crawley] p. 114, first part of 4th paragraph. , represent f(s), f_{s}(p) respectively. We show, in their notation, f_{s}(p)=q. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme0nex 31024* | 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 30945- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 30078, 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 31025 | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), f_{s}(q) respectively. We show f_{s}(q) w. (Contributed by NM, 12-Oct-2012.) |
Theorem | cdleme18b 31026 | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), f_{s}(q) respectively. We show f_{s}(q) q. (Contributed by NM, 12-Oct-2012.) |
Theorem | cdleme18c 31027* | Part of proof of Lemma E in [Crawley] p. 114, 2nd sentence of 4th paragraph. , represent f(s), f_{s}(q) respectively. We show f_{s}(q) = p whenever p q has three atoms under it (implied by the negated existential condition). (Contributed by NM, 10-Nov-2012.) |
Theorem | cdleme22gb 31028 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
Theorem | cdleme18d 31029* | Part of proof of Lemma E in [Crawley] p. 114, 4th sentence of 4th paragraph. , , , represent f(s), f_{s}(r), f(t), f_{t}(r) respectively. We show f_{s}(r)=f_{t}(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 31030 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemedb 31031 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdlemeda 31032 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemednpq 31033 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdlemednuN 31034 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20zN 31035 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20y 31036 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme19a 31037 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. represents s_{2}. In their notation, we prove that if r s t, then s_{2=}(s t) w. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdleme19b 31038 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. , , represent s_{2}, f(s), f(t). In their notation, we prove that if r s t, then s_{2} f(s) f(t). (Contributed by NM, 13-Nov-2012.) |
Theorem | cdleme19c 31039 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, 1st line. , represent s_{2}, f(s). We prove f(s) s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdleme19d 31040 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114. , , represent s_{2}, f(s), f(t). We prove f(s) s_{2} = f(s) f(t). (Contributed by NM, 14-Nov-2012.) |
Theorem | cdleme19e 31041 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 2. , , , represent s_{2}, f(s), t_{2}, f(t). We prove f(s) s_{2=f}(t) t_{2}. (Contributed by NM, 14-Nov-2012.) |
Theorem | cdleme19f 31042 | Part of proof of Lemma E in [Crawley] p. 113, 5th paragraph on p. 114, line 3. , , , , , represent s_{2}, f(s), f_{s}(r), t_{2}, f(t), f_{t}(r). We prove that if r s t, then f_{t}(r) = f_{t}(r). (Contributed by NM, 14-Nov-2012.) |
Theorem | cdleme20aN 31043 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 14-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20bN 31044 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. , , , represent s_{2}, f(s), t_{2}, f(t). We show v s_{2} = v t_{2}. (Contributed by NM, 15-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20c 31045 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 15-Nov-2012.) |
Theorem | cdleme20d 31046 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, second line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme20e 31047 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line. , , , represent s_{2}, f(s), t_{2}, f(t). We show <f(s),s_{2},s> and <f(t),t_{2},t> are centrally perspective. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme20f 31048 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, 4th line. , , , represent s_{2}, f(s), t_{2}, f(t). We show <f(s),s_{2},s> and <f(t),t_{2},t> are axially perspective. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme20g 31049 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20h 31050 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20i 31051 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). We show (f(s) s_{2}) (f(t) t_{2}) p q. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20j 31052 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114. , , , represent s_{2}, f(s), t_{2}, f(t). We show s_{2} t_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdleme20k 31053 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, antepenultimate line. , , , represent s_{2}, f(s), t_{2}, f(t). (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20l1 31054 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s_{2}, f(s), t_{2}, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20l2 31055 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s_{2}, f(s), t_{2}, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20l 31056 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s_{2}, f(s), t_{2}, f(t) respectively. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20m 31057 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , , , represent s_{2}, f(s), f_{s}(r), t_{2}, f(t), f_{t}(r) respectively. We prove that if r s t and u s t, then f_{s}(r) = f_{t}(r). (Contributed by NM, 20-Nov-2012.) |
Theorem | cdleme20 31058 | Combine cdleme19f 31042 and cdleme20m 31057 to eliminate condition. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21a 31059 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21b 31060 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21c 31061 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21at 31062 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21ct 31063 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21d 31064 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s_{2}, f(s), f_{s}(r), z_{2}, f(z), f_{z}(r) respectively. We prove f_{s}(r) = f_{z}(r). (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21e 31065 | Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s_{2}, f(s), f_{s}(r), z_{2}, f(z), f_{z}(r) respectively. We prove that if u s z, then f_{t}(r) = f_{z}(r). (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21f 31066 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21g 31067 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21h 31068* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21i 31069* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21j 31070* | Combine cdleme20 31058 and cdleme21i 31069 to eliminate condition. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21 31071 | Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. , , , , , represent s_{2}, f(s), f_{s}(r), t_{2}, f(t), f_{t}(r) respectively. Combine cdleme18d 31029 and cdleme21j 31070 to eliminate existence condition, proving f_{s}(r) = f_{t}(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21k 31072 | Eliminate condition in cdleme21 31071. (Contributed by NM, 26-Dec-2012.) |