P. 350 of Theorem List - Metamath Proof Explorer

Home	Metamath Proof Explorer Theorem List (p. 350 of 360)	< 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-24457)

Hilbert Space Explorer
(24458-25982)

Users' Mathboxes
(25983-35925)

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

Theorem	cdlemk47 34901*	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 34902*	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 34903*	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 34904*	Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. , stand for g, h. represents tau. TODO: Combine into cdlemk52 34906? (Contributed by NM, 23-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $.\/$ $./\$ $.\/$

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

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

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

Theorem	cdlemk53 34909*	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 34910*	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 34911*	Lemma for cdlemk55 34913. (Contributed by NM, 26-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

Theorem	cdlemk55 34913*	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 34914*	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 34915*	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 34916*	Substitution version of cdlemk35 34864. (Contributed by NM, 31-Jul-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

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

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

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

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

Theorem	cdleml1N 34928	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 34929*	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 34930*	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 34931*	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 34932*	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 34933*	Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.)
$.\/$ $./\$ $.\/$ $./\$ $.\/$ $.\/$ $./\$ $.\/$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

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

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

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

Theorem	dva1dim 34937*	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 34515. is the division ring base by erngdv 34945, and is the scalar product by dvavsca 34969. 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 34938*	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 34939	Value of the endomorphism division ring unit. (Contributed by NM, 12-Oct-2013.)
$/\$ $/\$

Theorem	erngdvlem1 34940*	Lemma for erngrng 34944. (Contributed by NM, 4-Aug-2013.)
$/\$

Theorem	erngdvlem2N 34941*	Lemma for erngrng 34944. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.)
$/\$

Theorem	erngdvlem3 34942*	Lemma for erngrng 34944. (Contributed by NM, 6-Aug-2013.)
$/\$

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

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

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

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

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

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

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

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

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

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

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

Syntax	cdveca 34954	Extend class notation with constructed vector space A.


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

Theorem	dvafset 34956*	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 34957*	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 34958	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 34959	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 34960*	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 34961*	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
Scalar $/\$ $/\$ $/\$

Theorem	dvaplusgv 34962	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
Scalar $/\$ $/\$ $/\$ $/\$

Theorem	dvafmulr 34963*	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 34964	Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
Scalar $/\$ $/\$ $/\$

Theorem	dvavbase 34965	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 34966*	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 34967	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
$/\$ $/\$ $/\$

Theorem	dvafvsca 34968*	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 34969	Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.)
$/\$ $/\$ $/\$

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


Theorem	tendospcl 34971	Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
$/\$ $/\$ $/\$

Theorem	tendospass 34972	Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	tendospdi1 34973	Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	tendocnv 34974	Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.)
$/\$ $/\$ $/\$

Theorem	tendospdi2 34975*	Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.)
$/\$ $/\$

Theorem	tendospcanN 34976*	Cancellation law for trace-perserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
$/\$ $/\$ $/\$ $/\$ $/\$

Theorem	dvaabl 34977	The constructed partial vector space A for a lattice is an abelian group. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
$/\$

Theorem	dvalveclem 34978	Lemma for dvalvec 34979. (Contributed by NM, 11-Oct-2013.) (Proof shortened by Mario Carneiro, 22-Jun-2014.)
Scalar $/\$

Theorem	dvalvec 34979	The constructed partial vector space A for a lattice is a left vector space. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.)
$/\$

Theorem	dva0g 34980	The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014.)
$/\$

Syntax	cdia 34981	Extend class notation with partial isomorphism A.


Definition	df-disoa 34982*	Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.)


Theorem	diaffval 34983*	The partial isomorphism A for a lattice . (Contributed by NM, 15-Oct-2013.)


Theorem	diafval 34984*	The partial isomorphism A for a lattice . (Contributed by NM, 15-Oct-2013.)
$/\$

Theorem	diaval 34985*	The partial isomorphism A for a lattice . Definition of isomorphism map in [Crawley] p. 120 line 24. (Contributed by NM, 15-Oct-2013.)
$/\$ $/\$ $/\$

Theorem	diaelval 34986	Member of the partial isomorphism A for a lattice . (Contributed by NM, 3-Dec-2013.)
$/\$ $/\$ $/\$ $/\$

Theorem	diafn 34987*	Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.)
$/\$

Theorem	diadm 34988*	Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.)
$/\$

Theorem	diaeldm 34989	Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.)
$/\$ $/\$

Theorem	diadmclN 34990	A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
$/\$ $/\$

Theorem	diadmleN 34991	A member of domain of the partial isomorphism A is under the fiducial hyperplane. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
$/\$ $/\$

Theorem	dian0 34992	The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.)
$/\$ $/\$ $/\$

Theorem	dia0eldmN 34993	The lattice zero belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
$/\$

Theorem	dia1eldmN 34994	The fiducial hyperplane (the largest allowed lattice element) belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.)
$/\$

Theorem	diass 34995	The value of the partial isomorphism A is a set of translations i.e. a set of vectors. (Contributed by NM, 26-Nov-2013.)
$/\$ $/\$ $/\$

Theorem	diael 34996	A member of the value of the partial isomorphism A is a translation i.e. a vector. (Contributed by NM, 17-Jan-2014.)
$/\$ $/\$ $/\$ $/\$

Theorem	diatrl 34997	Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.)
$/\$ $/\$ $/\$ $/\$

Theorem	diaelrnN 34998	Any value of the partial isomorphism A is a set of translations i.e. a set of vectors. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.)
$/\$ $/\$

Theorem	dialss 34999	The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of [Crawley] p. 120 line 26. (Contributed by NM, 17-Jan-2014.) (Revised by Mario Carneiro, 23-Jun-2014.)
$/\$ $/\$ $/\$

Theorem	diaord 35000	The partial isomorphism A for a lattice is order-preserving in the region under co-atom . Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 26-Nov-2013.)
$/\$ $/\$ $/\$ $/\$ $/\$

< Previous Next >

Page List Jump to page: Contents 1 1-100 2 101-200 3 201-300 4 301-400 5 401-500 6 501-600 7 601-700 8 701-800 9 801-900 10 901-1000 11 1001-1100 12 1101-1200 13 1201-1300 14 1301-1400 15 1401-1500 16 1501-1600 17 1601-1700 18 1701-1800 19 1801-1900 20 1901-2000 21 2001-2100 22 2101-2200 23 2201-2300 24 2301-2400 25 2401-2500 26 2501-2600 27 2601-2700 28 2701-2800 29 2801-2900 30 2901-3000 31 3001-3100 32 3101-3200 33 3201-3300 34 3301