Home | Metamath
Proof Explorer Theorem List (p. 292 of 309) | < Previous Next > |
Browser slow? Try the
Unicode version. |
Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme0ex1N 29101* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme0ex2N 29102* | 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 29103* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme1b 29104 | 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 29105 | 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 29106 | 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 29107 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3c 29108 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3d 29109 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3e 29110 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3fN 29111 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. TODO: Delete - duplicates cdleme0e 29095. (Contributed by NM, 6-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme3g 29112 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme3h 29113 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme3fa 29114 and cdleme3 29115. (Contributed by NM, 6-Jun-2012.) |
Theorem | cdleme3fa 29114 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme3 29115. (Contributed by NM, 6-Oct-2012.) |
Theorem | cdleme3 29115 | Part of proof of Lemma E in [Crawley] p. 113. represents f(r). is the fiducial co-atom (hyperplane) w. Here and in cdleme3fa 29114 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 29107 through cdleme3 29115, so there may be a simpler proof that we have overlooked. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme4 29116 | Part of proof of Lemma E in [Crawley] p. 113. and represent f(s) and f_{s}(r). Here show p q = r u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme4a 29117 | Part of proof of Lemma E in [Crawley] p. 114 top. represents f_{s}(r). Auxiliary lemma derived from cdleme5 29118. We show f_{s}(r) p q. (Contributed by NM, 10-Nov-2012.) |
Theorem | cdleme5 29118 | Part of proof of Lemma E in [Crawley] p. 113. represents f_{s}(r). We show r f_{s}(r)) = p q at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme6 29119 | Part of proof of Lemma E in [Crawley] p. 113. This expresses (r f_{s}(r)) w = u at the top of p. 114. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7aa 29120 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29126 and cdleme7 29127. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7a 29121 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29126 and cdleme7 29127. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7b 29122 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29126 and cdleme7 29127. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7c 29123 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29126 and cdleme7 29127. (Contributed by NM, 7-Jun-2012.) |
Theorem | cdleme7d 29124 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29126 and cdleme7 29127. (Contributed by NM, 8-Jun-2012.) |
Theorem | cdleme7e 29125 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme7ga 29126 and cdleme7 29127. (Contributed by NM, 8-Jun-2012.) |
Theorem | cdleme7ga 29126 | Part of proof of Lemma E in [Crawley] p. 113. See cdleme7 29127. (Contributed by NM, 8-Jun-2012.) |
Theorem | cdleme7 29127 | Part of proof of Lemma E in [Crawley] p. 113. and represent f_{s}(r) and f(s) respectively. is the fiducial co-atom (hyperplane) that they call w. Here and in cdleme7ga 29126 above, we show that f_{s}(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 29120 through cdleme7 29127, so there may be a simpler proof that we have overlooked. (Contributed by NM, 9-Jun-2012.) |
Theorem | cdleme8 29128 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents s_{1}. In their notation, we prove p s_{1} = p s. (Contributed by NM, 9-Jun-2012.) |
Theorem | cdleme9a 29129 | Part of proof of Lemma E in [Crawley] p. 113. represents s_{1}, which we prove is an atom. (Contributed by NM, 10-Jun-2012.) |
Theorem | cdleme9b 29130 | Utility lemma for Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Oct-2012.) |
Theorem | cdleme9 29131 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. and represent s_{1} and f(s) respectively. In their notation, we prove f(s) s_{1} = q s_{1}. (Contributed by NM, 10-Jun-2012.) |
Theorem | cdleme10 29132 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents s_{2}. In their notation, we prove s s_{2} = s r. (Contributed by NM, 9-Jun-2012.) |
Theorem | cdleme8tN 29133 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents t_{1}. In their notation, we prove p t_{1} = p t. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme9taN 29134 | Part of proof of Lemma E in [Crawley] p. 113. represents t_{1}, which we prove is an atom. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme9tN 29135 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. and represent t_{1} and f(t) respectively. In their notation, we prove f(t) t_{1} = q t_{1}. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme10tN 29136 | Part of proof of Lemma E in [Crawley] p. 113, 2nd paragraph on p. 114. represents t_{2}. In their notation, we prove t t_{2} = t r. (Contributed by NM, 8-Oct-2012.) (New usage is discouraged.) |
Theorem | cdleme16aN 29137 | 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 29138 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 12-Jun-2012.) |
Theorem | cdleme11c 29139 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme11dN 29140 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme11e 29141 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 13-Jun-2012.) |
Theorem | cdleme11fN 29142 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 14-Jun-2012.) (New usage is discouraged.) |
Theorem | cdleme11g 29143 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11h 29144 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11j 29145 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 14-Jun-2012.) |
Theorem | cdleme11k 29146 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme11l 29147 | Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 29148. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme11 29148 | 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 29138 through cdleme11 29148, so there may be a simpler proof that we have overlooked. (Contributed by NM, 15-Jun-2012.) |
Theorem | cdleme12 29149 | 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 29150 | 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 29151 | 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 28764 to cdleme13 29150. and represent f(s) and f(t) respectively. (Contributed by NM, 8-Oct-2012.) |
Theorem | cdleme15a 29152 | 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 29153 | 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 29154 | 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 29155 | 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 29156 | 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 29157 | 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 29158 | 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 29159 | 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 29160 | 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 29161 | 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 29162 | 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 29163 | 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 29164 | 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 29165 | Lemma leading to cdleme17c 29166. (Contributed by NM, 11-Oct-2012.) |
Theorem | cdleme17c 29166 | 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 29167 | 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 29168* | 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 29089- which is under w, so the only 2 left not under w are p and q themselves.) Note that by cvlsupr2 28222, 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 29169 | 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 29170 | 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 29171* | 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 29172 | Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.) |
Theorem | cdleme18d 29173* | 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 29174 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemedb 29175 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 20-Nov-2012.) |
Theorem | cdlemeda 29176 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 13-Nov-2012.) |
Theorem | cdlemednpq 29177 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s_{2}. (Contributed by NM, 18-Nov-2012.) |
Theorem | cdlemednuN 29178 | 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 29179 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.) |
Theorem | cdleme20y 29180 | Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) |
Theorem | cdleme19a 29181 | 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 29182 | 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 29183 | 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 29184 | 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 29185 | 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 29186 | 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 29187 | 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 29188 | 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 29189 | 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 29190 | 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.) |