Home | Metamath
Proof ExplorerTheorem List
(p. 319 of 329)
| < 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-22423) |
Hilbert Space Explorer
(22424-23946) |
Users' Mathboxes
(23947-32824) |

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

Statement | ||

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

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

Theorem | cdlemk42yN 31803* | 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 31804* | 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 31805* | 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 31806* | 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 31807* | 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 31808* | 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 31809* | 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 31810* | 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 31811* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 31813? (Contributed by NM, 23-Jul-2013.) |

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

Theorem | cdlemk52 31813* | 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 31814* | Lemma for cdlemk53 31816. (Contributed by NM, 26-Jul-2013.) |

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

Theorem | cdlemk53 31816* | 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 31817* | 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 31818* | Lemma for cdlemk55 31820. (Contributed by NM, 26-Jul-2013.) |

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

Theorem | cdlemk55 31820* | 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 31821* | 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 31822* | 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 31823* | Substitution version of cdlemk35 31771. (Contributed by NM, 31-Jul-2013.) |

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

Theorem | cdlemk55u 31825* | 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 31826* | Lemma for cdlemk39u 31827. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk39u 31827* | 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 31828* | cdlemk19 31728 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.) |

Theorem | cdlemk19u 31829* | 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 31830* | 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 31831* | Use a fixed element to eliminate in cdlemk19u 31829. (Contributed by NM, 1-Aug-2013.) |

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

Theorem | cdlemk 31833* | 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 31834* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 31833. TODO: can this be used to shorten uses of cdlemk 31833? (Contributed by NM, 15-Oct-2013.) |

Theorem | cdleml1N 31835 | 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 31836* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |

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

Theorem | cdleml4N 31838* | |

Theorem | cdleml5N 31839* | |

Theorem | cdleml6 31840* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |

Theorem | cdleml7 31841* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |

Theorem | cdleml8 31842* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |

Theorem | cdleml9 31843* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |

Theorem | dva1dim 31844* | Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in [Crawley] p. 120 line 21, but using a non-identity translation (nonzero vector) whose trace is rather than itself; exists by cdlemf 31422. is the division ring base by erngdv 31852, and is the scalar product by dvavsca 31876. must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013.) |

Theorem | dvhb1dimN 31845* | Two expressions for the 1-dimensional subspaces of vector space H, in the isomorphism B case where the 2nd vector component is zero. (Contributed by NM, 23-Feb-2014.) (New usage is discouraged.) |

Theorem | erng1lem 31846 | Value of the endomorphism division ring unit. (Contributed by NM, 12-Oct-2013.) |

Theorem | erngdvlem1 31847* | Lemma for erngrng 31851. (Contributed by NM, 4-Aug-2013.) |

Theorem | erngdvlem2N 31848* | Lemma for erngrng 31851. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |

Theorem | erngdvlem3 31849* | Lemma for erngrng 31851. (Contributed by NM, 6-Aug-2013.) |

Theorem | erngdvlem4 31850* | Lemma for erngdv 31852. (Contributed by NM, 11-Aug-2013.) |

Theorem | erngrng 31851 | An endomorphism ring is a ring. Todo: fix comment. (Contributed by NM, 4-Aug-2013.) |

Theorem | erngdv 31852 | An endomorphism ring is a division ring. Todo: fix comment. (Contributed by NM, 11-Aug-2013.) |

Theorem | erng0g 31853* | The division ring zero of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |

Theorem | erng1r 31854 | The division ring unit of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |

Theorem | erngdvlem1-rN 31855* | Lemma for erngrng 31851. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |

Theorem | erngdvlem2-rN 31856* | Lemma for erngrng 31851. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |

Theorem | erngdvlem3-rN 31857* | Lemma for erngrng 31851. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |

Theorem | erngdvlem4-rN 31858* | Lemma for erngdv 31852. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.) |

Theorem | erngrng-rN 31859 | An endomorphism ring is a ring. Todo: fix comment. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |

Theorem | erngdv-rN 31860 | An endomorphism ring is a division ring. Todo: fix comment. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.) |

Syntax | cdveca 31861 | Extend class notation with constructed vector space A. |

Definition | df-dveca 31862* | Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.) |

Scalar | ||

Theorem | dvafset 31863* | The constructed partial vector space A for a lattice . (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Scalar | ||

Theorem | dvaset 31864* | The constructed partial vector space A for a lattice . (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Scalar | ||

Theorem | dvasca 31865 | The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom ). (Contributed by NM, 22-Jun-2014.) |

Scalar | ||

Theorem | dvabase 31866 | The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom ). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Scalar | ||

Theorem | dvafplusg 31867* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Scalar | ||

Theorem | dvaplusg 31868* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |

Scalar | ||

Theorem | dvaplusgv 31869 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |

Scalar | ||

Theorem | dvafmulr 31870* | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Scalar | ||

Theorem | dvamulr 31871 | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |

Scalar | ||

Theorem | dvavbase 31872 | The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom ). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Theorem | dvafvadd 31873* | The vector sum operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Theorem | dvavadd 31874 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |

Theorem | dvafvsca 31875* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |

Theorem | dvavsca 31876 | |

Theorem | tendospid 31877 | Identity property of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |

Theorem | tendospcl 31878 | Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |

Theorem | tendospass 31879 | Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |

Theorem | tendospdi1 31880 | Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |