Home | Metamath
Proof Explorer Theorem List (p. 312 of 328) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21514) |
Hilbert Space Explorer
(21515-23037) |
Users' Mathboxes
(23038-32776) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme0nex 31101* | 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 31022- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 30155, 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 31102 | 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 31103 | 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 31104* | 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 31105 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
Theorem | cdleme18d 31106* | 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 31107 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemedb 31108 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdlemeda 31109 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemednpq 31110 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdlemednuN 31111 | 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 31112 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20y 31113 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme19a 31114 | 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 31115 | 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 31116 | 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 31117 | 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 31118 | 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 31119 | 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 31120 | 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 31121 | 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 31122 | 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 31123 | 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 31124 | 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 31125 | 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 31126 | 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 31127 | 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 31128 | 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 31129 | 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 31130 | 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 31131 | 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 31132 | 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 31133 | 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 31134 | 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 31135 | Combine cdleme19f 31119 and cdleme20m 31134 to eliminate condition. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21a 31136 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21b 31137 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21c 31138 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21at 31139 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21ct 31140 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21d 31141 | 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 31142 | 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 31143 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21g 31144 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21h 31145* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21i 31146* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21j 31147* | Combine cdleme20 31135 and cdleme21i 31146 to eliminate condition. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21 31148 | 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 31106 and cdleme21j 31147 to eliminate existence condition, proving f_{s}(r) = f_{t}(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21k 31149 | Eliminate condition in cdleme21 31148. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme22aa 31150 | 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 31151 | 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 31152 | 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 31153 | 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 31154 | 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 31155 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. (Contributed by NM, 6-Dec-2012.) |
Theorem | cdleme22eALTN 31156 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.) |
Theorem | cdleme22f 31157 | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), f_{t}(s) respectively. If s t v, then f_{t}(s) f(t) v. (Contributed by NM, 6-Dec-2012.) |
Theorem | cdleme22f2 31158 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 31157 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) f_{s}(t) v. (Contributed by NM, 7-Dec-2012.) |
Theorem | cdleme22g 31159 | 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 31160 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme23b 31161 | 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 31162 | 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 31163* | Quantified version of cdleme21k 31149. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme25a 31164* | Lemma for cdleme25b 31165. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25b 31165* | Transform cdleme24 31163. TODO get rid of $d's on , (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25c 31166* | Transform cdleme25b 31165. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25dN 31167* | Transform cdleme25c 31166. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
Theorem | cdleme25cl 31168* | Show closure of the unique element in cdleme25c 31166. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme25cv 31169* | Change bound variables in cdleme25c 31166. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26e 31170* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26ee 31171* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26eALTN 31172* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), f_{z}(s), f_{z}(t) respectively. When t v = p q, f_{z}(s) f_{z}(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme26fALTN 31173* | Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), f_{t}(s) respectively. If t t v, then f_{t}(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.) |