Home Metamath Proof ExplorerTheorem List (p. 312 of 328) < Previous  Next > Browser slow? Try the Unicode version.

 Color key: Metamath Proof Explorer (1-22421) Hilbert Space Explorer (22422-23944) Users' Mathboxes (23945-32762)

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

Theoremcdleme19b 31101 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 31102 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 31103 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 31104 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 31105 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 31106 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 31107 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 31108 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 31109 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 31110 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 31111 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 31112 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 31113 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 31114 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 31115 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 31116 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 31117 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 31118 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 31119 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 31120 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 31121 Combine cdleme19f 31105 and cdleme20m 31120 to eliminate condition. (Contributed by NM, 28-Nov-2012.)

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

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

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

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

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

Theoremcdleme21d 31127 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 31128 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 31129 Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.)

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

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

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

Theoremcdleme21j 31133* Combine cdleme20 31121 and cdleme21i 31132 to eliminate condition. (Contributed by NM, 29-Nov-2012.)

Theoremcdleme21 31134 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 31092 and cdleme21j 31133 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.)

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

Theoremcdleme22aa 31136 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.)

Theoremcdleme22a 31137 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.)

Theoremcdleme22b 31138 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.)

Theoremcdleme22cN 31139 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.)

Theoremcdleme22d 31140 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 9th line on p. 115. (Contributed by NM, 4-Dec-2012.)

Theoremcdleme22e 31141 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. (Contributed by NM, 6-Dec-2012.)

Theoremcdleme22eALTN 31142 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. (Contributed by NM, 6-Dec-2012.) (New usage is discouraged.)

Theoremcdleme22f 31143 Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), ft(s) respectively. If s t v, then ft(s) f(t) v. (Contributed by NM, 6-Dec-2012.)

Theoremcdleme22f2 31144 Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 31143 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) fs(t) v. (Contributed by NM, 7-Dec-2012.)

Theoremcdleme22g 31145 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.)

Theoremcdleme23a 31146 Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.)

Theoremcdleme23b 31147 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)

Theoremcdleme23c 31148 Part of proof of Lemma E in [Crawley] p. 113, 4th paragraph, 6th line on p. 115. (Contributed by NM, 8-Dec-2012.)

Theoremcdleme24 31149* Quantified version of cdleme21k 31135. (Contributed by NM, 26-Dec-2012.)

Theoremcdleme25a 31150* Lemma for cdleme25b 31151. (Contributed by NM, 1-Jan-2013.)

Theoremcdleme25b 31151* Transform cdleme24 31149. TODO get rid of \$d's on , (Contributed by NM, 1-Jan-2013.)

Theoremcdleme25c 31152* Transform cdleme25b 31151. (Contributed by NM, 1-Jan-2013.)

Theoremcdleme25dN 31153* Transform cdleme25c 31152. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.)

Theoremcdleme25cl 31154* Show closure of the unique element in cdleme25c 31152. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme25cv 31155* Change bound variables in cdleme25c 31152. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme26e 31156* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme26ee 31157* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. TODO: FIX COMMENT. (Contributed by NM, 2-Feb-2013.)

Theoremcdleme26eALTN 31158* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 4th line on p. 115. , , represent f(z), fz(s), fz(t) respectively. When t v = p q, fz(s) fz(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)

Theoremcdleme26fALTN 31159* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), ft(s) respectively. If t t v, then ft(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)

Theoremcdleme26f 31160* Part of proof of Lemma E in [Crawley] p. 113, 3rd paragraph, 6th and 7th lines on p. 115. , represent f(t), ft(s) respectively. If t t v, then ft(s) f(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)

Theoremcdleme26f2ALTN 31161* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 31159 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) fs(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.) (New usage is discouraged.)

Theoremcdleme26f2 31162* Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 31159 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) fs(t) v. TODO: FIX COMMENT. (Contributed by NM, 1-Feb-2013.)

Theoremcdleme27cl 31163* Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.)

Theoremcdleme27a 31164* Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 31160 with s and t swapped (this case is not mentioned by them). If s t v, then f(s) fs(t) v. TODO: FIX COMMENT. (Contributed by NM, 3-Feb-2013.)

Theoremcdleme27b 31165* Lemma for cdleme27N 31166. (Contributed by NM, 3-Feb-2013.)

Theoremcdleme27N 31166* Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme27a 31164. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.)