Home Metamath Proof ExplorerTheorem 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)

Theorem List for Metamath Proof Explorer - 31001-31100   *Has distinct variable group(s)
TypeLabelDescription
Statement

Theoremcdleme11j 31001 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31004. (Contributed by NM, 14-Jun-2012.)

Theoremcdleme11k 31002 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31004. (Contributed by NM, 15-Jun-2012.)

Theoremcdleme11l 31003 Part of proof of Lemma E in [Crawley] p. 113. Lemma leading to cdleme11 31004. (Contributed by NM, 15-Jun-2012.)

Theoremcdleme11 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.)

Theoremcdleme12 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.)

Theoremcdleme13 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.)

Theoremcdleme14 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.)

Theoremcdleme15a 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 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.)

Theoremcdleme15b 31009 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.)

Theoremcdleme15c 31010 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.)

Theoremcdleme15d 31011 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.)

Theoremcdleme15 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.)

Theoremcdleme16b 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.)

Theoremcdleme16c 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.)

Theoremcdleme16d 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.)

Theoremcdleme16e 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.)

Theoremcdleme16f 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.)

Theoremcdleme16g 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.)

Theoremcdleme16 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.)

Theoremcdleme17a 31020 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.)

Theoremcdleme17b 31021 Lemma leading to cdleme17c 31022. (Contributed by NM, 11-Oct-2012.)

Theoremcdleme17c 31022 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.)

Theoremcdleme17d1 31023 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.)

Theoremcdleme0nex 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.)

Theoremcdleme18a 31025 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.)

Theoremcdleme18b 31026 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.)

Theoremcdleme18c 31027* 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.)

Theoremcdleme22gb 31028 Utility lemma for Lemma E in [Crawley] p. 115. (Contributed by NM, 5-Dec-2012.)

Theoremcdleme18d 31029* 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.)

Theoremcdlemesner 31030 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 13-Nov-2012.)

Theoremcdlemedb 31031 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 20-Nov-2012.)

Theoremcdlemeda 31032 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 13-Nov-2012.)

Theoremcdlemednpq 31033 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 18-Nov-2012.)

TheoremcdlemednuN 31034 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. represents s2. (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.)

Theoremcdleme20zN 31035 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.) (New usage is discouraged.)

Theoremcdleme20y 31036 Part of proof of Lemma E in [Crawley] p. 113. Utility lemma. (Contributed by NM, 17-Nov-2012.)

Theoremcdleme19a 31037 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.)

Theoremcdleme19b 31038 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.)

Theoremcdleme19c 31039 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.)

Theoremcdleme19d 31040 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.)

Theoremcdleme19e 31041 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.)

Theoremcdleme19f 31042 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.)

Theoremcdleme20aN 31043 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.)

Theoremcdleme20bN 31044 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.)

Theoremcdleme20c 31045 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.)

Theoremcdleme20d 31046 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.)

Theoremcdleme20e 31047 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.)

Theoremcdleme20f 31048 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.)

Theoremcdleme20g 31049 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.)

Theoremcdleme20h 31050 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.)

Theoremcdleme20i 31051 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.)

Theoremcdleme20j 31052 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.)

Theoremcdleme20k 31053 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, 20-Nov-2012.)

Theoremcdleme20l1 31054 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20l2 31055 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20l 31056 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , represent s2, f(s), t2, f(t) respectively. (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20m 31057 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 114, penultimate line. , , , , , represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. We prove that if r s t and u s t, then fs(r) = ft(r). (Contributed by NM, 20-Nov-2012.)

Theoremcdleme20 31058 Combine cdleme19f 31042 and cdleme20m 31057 to eliminate condition. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21a 31059 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21b 31060 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21c 31061 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.)

Theoremcdleme21at 31062 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21ct 31063 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21d 31064 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove fs(r) = fz(r). (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21e 31065 Part of proof of Lemma E in [Crawley] p. 113, last paragraph on p. 115, 3rd line. , , , , , represent s2, f(s), fs(r), z2, f(z), fz(r) respectively. We prove that if u s z, then ft(r) = fz(r). (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21f 31066 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21g 31067 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21h 31068* Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21i 31069* Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21j 31070* Combine cdleme20 31058 and cdleme21i 31069 to eliminate condition. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21 31071 Part of proof of Lemma E in [Crawley] p. 113, 3rd line on p. 115. , , , , , represent s2, f(s), fs(r), t2, f(t), ft(r) respectively. Combine cdleme18d 31029 and cdleme21j 31070 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21k 31072 Eliminate condition in cdleme21 31071. (Contributed by NM, 26-Dec-2012.)