Home | Metamath
Proof ExplorerTheorem List
(p. 299 of 309)
| < Previous Next > |

Browser slow? Try the
Unicode version. |

Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs

Color key: | Metamath Proof Explorer
(1-21328) |
Hilbert Space Explorer
(21329-22851) |
Users' Mathboxes
(22852-30843) |

Type | Label | Description |
---|---|---|

Statement | ||

Theorem | cdlemkfid2N 29801 | Lemma for cdlemkfid3N 29803. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |

Theorem | cdlemkid2 29802* | Lemma for cdlemkid 29814. (Contributed by NM, 24-Jul-2013.) |

Theorem | cdlemkfid3N 29803* | TODO: is this useful or should it be deleted? (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |

Theorem | cdlemky 29804* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up stuff. represents in cdlemk31 29774. (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemkyu 29805* | Convert between function and explicit forms. represents in cdlemkuu 29773. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemkyuu 29806* | cdlemkyu 29805 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemk11ta 29807* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemk19ylem 29808* | Lemma for cdlemk19y 29810. (Contributed by NM, 30-Jul-2013.) |

Theorem | cdlemk11tb 29809* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. cdlemk11ta 29807 with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemk19y 29810* | cdlemk19 29747 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |

Theorem | cdlemkid3N 29811* | Lemma for cdlemkid 29814. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.) |

Theorem | cdlemkid4 29812* | Lemma for cdlemkid 29814. (Contributed by NM, 25-Jul-2013.) |

Theorem | cdlemkid5 29813* | Lemma for cdlemkid 29814. (Contributed by NM, 25-Jul-2013.) |

Theorem | cdlemkid 29814* | The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.) |

Theorem | cdlemk35s 29815* | Substitution version of cdlemk35 29790. (Contributed by NM, 22-Jul-2013.) |

Theorem | cdlemk35s-id 29816* | Substitution version of cdlemk35 29790. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk39s 29817* | Substitution version of cdlemk39 29794. TODO: Can any commonality with cdlemk35s 29815 be exploited? (Contributed by NM, 23-Jul-2013.) |

Theorem | cdlemk39s-id 29818* | Substitution version of cdlemk39 29794 with non-identity requirement on removed. TODO: Can any commonality with cdlemk35s 29815 be exploited? (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk42 29819* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) |

Theorem | cdlemk19xlem 29820* | Lemma for cdlemk19x 29821. (Contributed by NM, 30-Jul-2013.) |

Theorem | cdlemk19x 29821* | cdlemk19 29747 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |

Theorem | cdlemk42yN 29822* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) (New usage is discouraged.) |

Theorem | cdlemk11tc 29823* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. , stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemk11t 29824* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119. , stand for g, h. represents tau. (Contributed by NM, 21-Jul-2013.) |

Theorem | cdlemk45 29825* | Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119. , stand for g, h. represents tau. They do not explicitly mention the requirement . (Contributed by NM, 22-Jul-2013.) |

Theorem | cdlemk46 29826* | Part of proof of Lemma K of [Crawley] p. 118. Line 38 (last line), p. 119. , stand for g, h. represents tau. (Contributed by NM, 22-Jul-2013.) |

Theorem | cdlemk47 29827* | Part of proof of Lemma K of [Crawley] p. 118. Line 2, p. 120. , stand for g, h. represents tau. (Contributed by NM, 22-Jul-2013.) |

Theorem | cdlemk48 29828* | Part of proof of Lemma K of [Crawley] p. 118. Line 4, p. 120. , stand for g, h. represents tau. (Contributed by NM, 22-Jul-2013.) |

Theorem | cdlemk49 29829* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 120. , stand for g, h. represents tau. (Contributed by NM, 23-Jul-2013.) |

Theorem | cdlemk50 29830* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 29832? (Contributed by NM, 23-Jul-2013.) |

Theorem | cdlemk51 29831* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 29832? (Contributed by NM, 23-Jul-2013.) |

Theorem | cdlemk52 29832* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. (Contributed by NM, 23-Jul-2013.) |

Theorem | cdlemk53a 29833* | Lemma for cdlemk53 29835. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk53b 29834* | Lemma for cdlemk53 29835. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk53 29835* | Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120. , stand for g, h. represents tau. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk54 29836* | Part of proof of Lemma K of [Crawley] p. 118. Line 10, p. 120. , stand for g, h. represents tau. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk55a 29837* | Lemma for cdlemk55 29839. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk55b 29838* | Lemma for cdlemk55 29839. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemk55 29839* | Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. , stand for g, h. represents tau. (Contributed by NM, 26-Jul-2013.) |

Theorem | cdlemkyyN 29840* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up stuff. (Contributed by NM, 21-Jul-2013.) (New usage is discouraged.) |

Theorem | cdlemk43N 29841* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 31-Jul-2013.) (New usage is discouraged.) |

Theorem | cdlemk35u 29842* | Substitution version of cdlemk35 29790. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk55u1 29843* | Lemma for cdlemk55u 29844. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk55u 29844* | Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. , stand for g, h. represents tau. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk39u1 29845* | Lemma for cdlemk39u 29846. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk39u 29846* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by . (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk19u1 29847* | cdlemk19 29747 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk19u 29848* | Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with , , . (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk56 29849* | Part of Lemma K of [Crawley] p. 118. Line 11, p. 120, "tau is in Delta" i.e. is a trace-preserving endormorphism. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk19w 29850* | Use a fixed element to eliminate in cdlemk19u 29848. (Contributed by NM, 1-Aug-2013.) |

Theorem | cdlemk56w 29851* | Use a fixed element to eliminate in cdlemk56 29849. (Contributed by NM, 1-Aug-2013.) |

Theorem | cdlemk 29852* | Lemma K of [Crawley] p. 118. Final result, lines 11 and 12 on p. 120: given two translations f and k with the same trace, there exists a trace-preserving endomorphism tau whose value at f is k. We use , , and to represent f, k, and tau. (Contributed by NM, 1-Aug-2013.) |

Theorem | tendoex 29853* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 29852. TODO: can this be used to shorten uses of cdlemk 29852? (Contributed by NM, 15-Oct-2013.) |

Theorem | cdleml1N 29854 | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |

Theorem | cdleml2N 29855* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |