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

 Color key: Metamath Proof Explorer (1-22423) Hilbert Space Explorer (22424-23946) Users' Mathboxes (23947-32824)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremcdlemk53a 31814* Lemma for cdlemk53 31816. (Contributed by NM, 26-Jul-2013.)

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

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

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

Theoremcdlemk55a 31818* Lemma for cdlemk55 31820. (Contributed by NM, 26-Jul-2013.)

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

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

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

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

Theoremcdlemk35u 31823* Substitution version of cdlemk35 31771. (Contributed by NM, 31-Jul-2013.)

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

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

Theoremcdlemk39u1 31826* Lemma for cdlemk39u 31827. (Contributed by NM, 31-Jul-2013.)

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

Theoremcdlemk19u1 31828* cdlemk19 31728 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.)

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

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

Theoremcdlemk19w 31831* Use a fixed element to eliminate in cdlemk19u 31829. (Contributed by NM, 1-Aug-2013.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Syntaxcdveca 31861 Extend class notation with constructed vector space A.

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

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

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

Theoremdvasca 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

Theoremdvabase 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

Theoremdvafplusg 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

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

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

Theoremdvafmulr 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

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

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

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

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

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

Theoremdvavsca 31876 Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)

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

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

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

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