Home | Metamath
Proof Explorer Theorem List (p. 357 of 426) | < Previous Next > |
Browser slow? Try the
Unicode version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdleme20e 35601 | 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.) |
Theorem | cdleme20f 35602 | 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.) |
Theorem | cdleme20g 35603 | 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.) |
Theorem | cdleme20h 35604 | 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.) |
Theorem | cdleme20i 35605 | 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.) |
Theorem | cdleme20j 35606 | 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.) |
Theorem | cdleme20k 35607 | 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.) |
Theorem | cdleme20l1 35608 | 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.) |
Theorem | cdleme20l2 35609 | 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.) |
Theorem | cdleme20l 35610 | 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.) |
Theorem | cdleme20m 35611 | 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.) |
Theorem | cdleme20 35612 | Combine cdleme19f 35596 and cdleme20m 35611 to eliminate condition. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21a 35613 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21b 35614 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21c 35615 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 28-Nov-2012.) |
Theorem | cdleme21at 35616 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21ct 35617 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21d 35618 | 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.) |
Theorem | cdleme21e 35619 | 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.) |
Theorem | cdleme21f 35620 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21g 35621 | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21h 35622* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21i 35623* | Part of proof of Lemma E in [Crawley] p. 115. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21j 35624* | Combine cdleme20 35612 and cdleme21i 35623 to eliminate condition. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21 35625 | 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 35582 and cdleme21j 35624 to eliminate existence condition, proving fs(r) = ft(r) with fewer conditions. (Contributed by NM, 29-Nov-2012.) |
Theorem | cdleme21k 35626 | Eliminate condition in cdleme21 35625. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme22aa 35627 | 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 35628 | 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 35629 | 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 35630 | 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 35631 | 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 35632 | 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.) |
Theorem | cdleme22eALTN 35633 | 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.) |
Theorem | cdleme22f 35634 | 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.) |
Theorem | cdleme22f2 35635 | Part of proof of Lemma E in [Crawley] p. 113. cdleme22f 35634 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.) |
Theorem | cdleme22g 35636 | 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 35637 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 8-Dec-2012.) |
Theorem | cdleme23b 35638 | 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 35639 | 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 35640* | Quantified version of cdleme21k 35626. (Contributed by NM, 26-Dec-2012.) |
Theorem | cdleme25a 35641* | Lemma for cdleme25b 35642. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25b 35642* | Transform cdleme24 35640. TODO get rid of $d's on , (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25c 35643* | Transform cdleme25b 35642. (Contributed by NM, 1-Jan-2013.) |
Theorem | cdleme25dN 35644* | Transform cdleme25c 35643. (Contributed by NM, 19-Jan-2013.) (New usage is discouraged.) |
Theorem | cdleme25cl 35645* | Show closure of the unique element in cdleme25c 35643. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme25cv 35646* | Change bound variables in cdleme25c 35643. (Contributed by NM, 2-Feb-2013.) |
Theorem | cdleme26e 35647* | 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.) |
Theorem | cdleme26ee 35648* | 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.) |
Theorem | cdleme26eALTN 35649* | 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.) |
Theorem | cdleme26fALTN 35650* | 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.) |
Theorem | cdleme26f 35651* | 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.) |
Theorem | cdleme26f2ALTN 35652* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 35650 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.) |
Theorem | cdleme26f2 35653* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26fALTN 35650 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.) |
Theorem | cdleme27cl 35654* | Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme27a 35655* | Part of proof of Lemma E in [Crawley] p. 113. cdleme26f 35651 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.) |
Theorem | cdleme27b 35656* | Lemma for cdleme27N 35657. (Contributed by NM, 3-Feb-2013.) |
Theorem | cdleme27N 35657* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme27a 35655. (Contributed by NM, 3-Feb-2013.) (New usage is discouraged.) |
Theorem | cdleme28a 35658* | Lemma for cdleme25b 35642. TODO: FIX COMMENT. (Contributed by NM, 4-Feb-2013.) |
Theorem | cdleme28b 35659* | Lemma for cdleme25b 35642. TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme28c 35660* | Part of proof of Lemma E in [Crawley] p. 113. Eliminate the antecedent in cdleme28b 35659. TODO: FIX COMMENT. (Contributed by NM, 6-Feb-2013.) |
Theorem | cdleme28 35661* | Quantified version of cdleme28c 35660. (Compare cdleme24 35640.) (Contributed by NM, 7-Feb-2013.) |
Theorem | cdleme29ex 35662* | Lemma for cdleme29b 35663. (Compare cdleme25a 35641.) TODO: FIX COMMENT. (Contributed by NM, 7-Feb-2013.) |
Theorem | cdleme29b 35663* | Transform cdleme28 35661. (Compare cdleme25b 35642.) TODO: FIX COMMENT. (Contributed by NM, 7-Feb-2013.) |
Theorem | cdleme29c 35664* | Transform cdleme28b 35659. (Compare cdleme25c 35643.) TODO: FIX COMMENT. (Contributed by NM, 8-Feb-2013.) |
Theorem | cdleme29cl 35665* | Show closure of the unique element in cdleme28c 35660. (Contributed by NM, 8-Feb-2013.) |
Theorem | cdleme30a 35666 | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 9-Feb-2013.) |
Theorem | cdleme31so 35667* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
Theorem | cdleme31sn 35668* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31sn1 35669* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31se 35670* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31se2 35671* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 3-Apr-2013.) |
Theorem | cdleme31sc 35672* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
Theorem | cdleme31sde 35673* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) |
Theorem | cdleme31snd 35674* | Part of proof of Lemma D in [Crawley] p. 113. (Contributed by NM, 1-Apr-2013.) |
Theorem | cdleme31sdnN 35675* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 31-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme31sn1c 35676* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 1-Mar-2013.) |
Theorem | cdleme31sn2 35677* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 26-Feb-2013.) |
Theorem | cdleme31fv 35678* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
Theorem | cdleme31fv1 35679* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 10-Feb-2013.) |
Theorem | cdleme31fv1s 35680* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 25-Feb-2013.) |
Theorem | cdleme31fv2 35681* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 23-Feb-2013.) |
Theorem | cdleme31id 35682* | Part of proof of Lemma E in [Crawley] p. 113. (Contributed by NM, 18-Apr-2013.) |
Theorem | cdlemefrs29pre00 35683 | ***START OF VALUE AT ATOM STUFF TO REPLACE ONES BELOW*** FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 35316. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefrs29bpre0 35684* | TODO fix comment. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefrs29bpre1 35685* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefrs29cpre1 35686* | TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefrs29clN 35687* | TODO: NOT USED? Show closure of the unique element in cdlemefrs29cpre1 35686. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
Theorem | cdlemefrs32fva 35688* | Part of proof of Lemma E in [Crawley] p. 113. Value of at an atom not under . TODO: FIX COMMENT. TODO: consolidate uses of lhpmat 35316 here and elsewhere, and presence/absence of term. Also, why can proof be shortened with cdleme29cl 35665? What is difference from cdlemefs27cl 35701? (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefrs32fva1 35689* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefr29exN 35690* | Lemma for cdlemefs29bpre1N 35705. (Compare cdleme25a 35641.) TODO: FIX COMMENT. TODO: IS THIS NEEDED? (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
Theorem | cdlemefr27cl 35691 | Part of proof of Lemma E in [Crawley] p. 113. Closure of . (Contributed by NM, 23-Mar-2013.) |
Theorem | cdlemefr32sn2aw 35692* | Show that is an atom not under when . (Contributed by NM, 28-Mar-2013.) |
Theorem | cdlemefr32snb 35693* | Show closure of . (Contributed by NM, 28-Mar-2013.) |
Theorem | cdlemefr29bpre0N 35694* | TODO fix comment. (Contributed by NM, 28-Mar-2013.) (New usage is discouraged.) |
Theorem | cdlemefr29clN 35695* | Show closure of the unique element in cdleme29c 35664. TODO fix comment. TODO Not needed? (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
Theorem | cdleme43frv1snN 35696* | Value of when . (Contributed by NM, 30-Mar-2013.) (New usage is discouraged.) |
Theorem | cdlemefr32fvaN 35697* | Part of proof of Lemma E in [Crawley] p. 113. Value of at an atom not under . TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) (New usage is discouraged.) |
Theorem | cdlemefr32fva1 35698* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. (Contributed by NM, 29-Mar-2013.) |
Theorem | cdlemefr31fv1 35699* | Value of when . TODO This may be useful for shortening others that now use riotasv 34245 3d . TODO: FIX COMMENT. (Contributed by NM, 30-Mar-2013.) |
Theorem | cdlemefs29pre00N 35700 | FIX COMMENT. TODO: see if this is the optimal utility theorem using lhpmat 35316. (Contributed by NM, 27-Mar-2013.) (New usage is discouraged.) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |