P. 365 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 365 of 377)	< 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-25707)

Hilbert Space Explorer
(25708-27232)

Users' Mathboxes
(27233-37662)

**Theorem List for Metamath Proof Explorer -** 36401-36500 *Has distinct variable group(s)
Type	Label	Description
Statement

Theorem	cdlemkid5 36401*	Lemma for cdlemkid 36402. (Contributed by NM, 25-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemkid 36402*	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 36403*	Substitution version of cdlemk35 36378. (Contributed by NM, 22-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk35s-id 36404*	Substitution version of cdlemk35 36378. (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk39s 36405*	Substitution version of cdlemk39 36382. TODO: Can any commonality with cdlemk35s 36403 be exploited? (Contributed by NM, 23-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk39s-id 36406*	Substitution version of cdlemk39 36382 with non-identity requirement on removed. TODO: Can any commonality with cdlemk35s 36403 be exploited? (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemk19xlem 36408*	Lemma for cdlemk19x 36409. (Contributed by NM, 30-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk19x 36409*	cdlemk19 36335 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk42yN 36410*	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 36411*	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 36412*	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 36413*	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 36414*	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 36415*	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 36416*	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 36417*	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 36418*	Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 36420? (Contributed by NM, 23-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

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

Theorem	cdlemk52 36420*	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 36421*	Lemma for cdlemk53 36423. (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk53b 36422*	Lemma for cdlemk53 36423. (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk53 36423*	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 36424*	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 36425*	Lemma for cdlemk55 36427. (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk55b 36426*	Lemma for cdlemk55 36427. (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk55 36427*	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 36428*	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 36429*	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 36430*	Substitution version of cdlemk35 36378. (Contributed by NM, 31-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk55u1 36431*	Lemma for cdlemk55u 36432. (Contributed by NM, 31-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk55u 36432*	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 36433*	Lemma for cdlemk39u 36434. (Contributed by NM, 31-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk39u 36434*	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 36435*	cdlemk19 36335 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk19u 36436*	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 36437*	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 36438*	Use a fixed element to eliminate in cdlemk19u 36436. (Contributed by NM, 1-Aug-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	cdlemk56w 36439*	Use a fixed element to eliminate in cdlemk56 36437. (Contributed by NM, 1-Aug-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

Theorem	cdleml5N 36446*	Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$

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

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

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

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

Theorem	dva1dim 36451*	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 36029. is the division ring base by erngdv 36459, and is the scalar product by dvavsca 36483. 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 36452*	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 36453	Value of the endomorphism division ring unit. (Contributed by NM, 12-Oct-2013.)
$/\$ $/\$

Theorem	erngdvlem1 36454*	Lemma for eringring 36458. (Contributed by NM, 4-Aug-2013.)
$/\$

Theorem	erngdvlem2N 36455*	Lemma for eringring 36458. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
$/\$

Theorem	erngdvlem3 36456*	Lemma for eringring 36458. (Contributed by NM, 6-Aug-2013.)
$/\$

Theorem	erngdvlem4 36457*	Lemma for erngdv 36459. (Contributed by NM, 11-Aug-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$

Theorem	eringring 36458	An endomorphism ring is a ring. Todo: fix comment. (Contributed by NM, 4-Aug-2013.)
$/\$

Theorem	erngdv 36459	An endomorphism ring is a division ring. Todo: fix comment. (Contributed by NM, 11-Aug-2013.)
$/\$

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

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

Theorem	erngdvlem1-rN 36462*	Lemma for eringring 36458. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.)
$/\$

Theorem	erngdvlem2-rN 36463*	Lemma for eringring 36458. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
$/\$

Theorem	erngdvlem3-rN 36464*	Lemma for eringring 36458. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
$/\$

Theorem	erngdvlem4-rN 36465*	Lemma for erngdv 36459. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$