Home Metamath Proof ExplorerTheorem List (p. 306 of 314) < 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-21444) Hilbert Space Explorer (21445-22967) Users' Mathboxes (22968-31305)

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

Theoremdib11N 30501 The isomorphism B for a lattice is one-to-one in the region under co-atom . (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.)

Theoremdibf11N 30502 The partial isomorphism A for a lattice is a one-to-one function. . Part of Lemma M of [Crawley] p. 120 line 27. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.)

TheoremdibclN 30503 Closure of partial isomorphism B for a lattice . (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)

Theoremdibvalrel 30504 The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.)

Theoremdib0 30505 The value of partial isomorphism B at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 27-Mar-2014.)

Theoremdib1dim 30506* Two expressions for the 1-dimensional subspaces of vector space H. (Contributed by NM, 24-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)

TheoremdibglbN 30507* Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.)

TheoremdibintclN 30508 The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)

Theoremdib1dim2 30509* Two expressions for a 1-dimensional subspace of vector space H (when is a nonzero vector i.e. non-identity translation). (Contributed by NM, 24-Feb-2014.)

Theoremdibss 30510 The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014.)

Theoremdiblss 30511 The value of partial isomorphism B is a subspace of partial vector space H. TODO: use dib* specific theorems instead of dia* ones to shorten proof? (Contributed by NM, 11-Feb-2014.)

Theoremdiblsmopel 30512* Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.)

Syntaxcdic 30513 Extend class notation with isomorphism C.

Definitiondf-dic 30514* Isomorphism C has domain of lattice atoms that are not less than or equal to the fiducial co-atom . The value is a one-dimensional subspace generated by the pair consisting of the vector below and the endomorphism ring unit. Definition of phi(q) in [Crawley] p. 121. Note that we use the fixed atom k ) to represent the p in their "Choose an atom p..." on line 21. (Contributed by NM, 15-Dec-2013.)

Theoremdicffval 30515* The partial isomorphism C for a lattice . (Contributed by NM, 15-Dec-2013.)

Theoremdicfval 30516* The partial isomorphism C for a lattice . (Contributed by NM, 15-Dec-2013.)

Theoremdicval 30517* The partial isomorphism C for a lattice . (Contributed by NM, 15-Dec-2013.) (Revised by Mario Carneiro, 22-Sep-2015.)

Theoremdicopelval 30518* Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 15-Feb-2014.)

TheoremdicelvalN 30519* Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)

Theoremdicval2 30520* The partial isomorphism C for a lattice . (Contributed by NM, 20-Feb-2014.)

Theoremdicelval3 30521* Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.)

Theoremdicopelval2 30522* Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 20-Feb-2014.)

Theoremdicelval2N 30523* Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)

TheoremdicfnN 30524* Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)

TheoremdicdmN 30525* Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)

TheoremdicvalrelN 30526 The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.)

Theoremdicssdvh 30527 The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014.)

Theoremdicelval1sta 30528* Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 16-Feb-2014.)

Theoremdicelval1stN 30529 Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 16-Feb-2014.) (New usage is discouraged.)

Theoremdicelval2nd 30530 Membership in value of the partial isomorphism C for a lattice . (Contributed by NM, 16-Feb-2014.)

Theoremdicvaddcl 30531 Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014.)

Theoremdicvscacl 30532 Membership in value of the partial isomorphism C is closed under scalar product. (Contributed by NM, 16-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)

Theoremdicn0 30533 The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.)

Theoremdiclss 30534 The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014.)

Theoremdiclspsn 30535* The value of isomorphism C is spanned by vector . Part of proof of Lemma N of [Crawley] p. 121 line 29. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)

Theoremcdlemn2 30536* Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.)

Theoremcdlemn2a 30537* Part of proof of Lemma N of [Crawley] p. 121. (Contributed by NM, 24-Feb-2014.)

Theoremcdlemn3 30538* Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.)

Theoremcdlemn4 30539* Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 24-Jun-2014.)

Theoremcdlemn4a 30540* Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.)

Theoremcdlemn5pre 30541* Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.)

Theoremcdlemn5 30542 Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.)

Theoremcdlemn6 30543* Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.)

Theoremcdlemn7 30544* Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.)

Theoremcdlemn8 30545* Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.)

Theoremcdlemn9 30546* Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn10 30547 Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn11a 30548* Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn11b 30549* Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn11c 30550* Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn11pre 30551* Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 30548, cdlemn11b 30549, cdlemn11c 30550, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn11 30552 Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.)

Theoremcdlemn 30553 Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.)

Theoremdihordlem6 30554* Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.)

Theoremdihordlem7 30555* Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihordlem7b 30556* Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihjustlem 30557 Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.)

Theoremdihjust 30558 Part of proof after Lemma N of [Crawley] p. 122 line 4, "the definition of phi(x) is independent of the atom q." (Contributed by NM, 2-Mar-2014.)

Theoremdihord1 30559 Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change to using lhpmcvr3 29365, here and all theorems below. (Contributed by NM, 2-Mar-2014.)

Theoremdihord2a 30560 Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihord2b 30561 Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihord2cN 30562* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: needed? shorten other proof with it? (Contributed by NM, 3-Mar-2014.) (New usage is discouraged.)

Theoremdihord11b 30563* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihord10 30564* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihord11c 30565* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihord2pre 30566* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

Theoremdihord2pre2 30567* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.)

Theoremdihord2 30568 Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. Todo: do we need and ? (Contributed by NM, 4-Mar-2014.)

Syntaxcdih 30569 Extend class notation with isomorphism H.

Definitiondf-dih 30570* Define isomorphism H. (Contributed by NM, 28-Jan-2014.)

Theoremdihffval 30571* The isomorphism H for a lattice . Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)

Theoremdihfval 30572* Isomorphism H for a lattice . Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.)

Theoremdihval 30573* Value of isomorphism H for a lattice . Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 3-Feb-2014.)

Theoremdihvalc 30574* Value of isomorphism H for a lattice when . (Contributed by NM, 4-Mar-2014.)

Theoremdihlsscpre 30575 Closure of isomorphism H for a lattice when . (Contributed by NM, 6-Mar-2014.)

Theoremdihvalcqpre 30576 Value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 6-Mar-2014.)

Theoremdihvalcq 30577 Value of isomorphism H for a lattice when , given auxiliary atom . TODO: Use dihvalcq2 30588 (with lhpmcvr3 29365 for simplification) that changes and to and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014.)

Theoremdihvalb 30578 Value of isomorphism H for a lattice when . (Contributed by NM, 4-Mar-2014.)

TheoremdihopelvalbN 30579* Ordered pair member of the partial isomorphism H for argument under . (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.)

Theoremdihvalcqat 30580 Value of isomorphism H for a lattice at an atom not under . (Contributed by NM, 27-Mar-2014.)

Theoremdih1dimb 30581* Two expressions for a 1-dimensional subspace of vector space H (when is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014.)

Theoremdih1dimb2 30582* Isomorphism H at an atom under . (Contributed by NM, 27-Apr-2014.)

Theoremdih1dimc 30583* Isomorphism H at an atom not under . (Contributed by NM, 27-Apr-2014.)

Theoremdib2dim 30584 Extend dia2dim 30418 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.)

Theoremdih2dimb 30585 Extend dib2dim 30584 to isomorphism H. (Contributed by NM, 22-Sep-2014.)

Theoremdih2dimbALTN 30586 Extend dia2dim 30418 to isomorphism H. (This version combines dib2dim 30584 and dih2dimb 30585 for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.)

Theoremdihopelvalcqat 30587* Ordered pair member of the partial isomorphism H for atom argument not under . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014.)

Theoremdihvalcq2 30588 Value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 26-Sep-2014.)

Theoremdihopelvalcpre 30589* Member of value of isomorphism H for a lattice when , given auxiliary atom . TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.)

Theoremdihopelvalc 30590* Member of value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 13-Mar-2014.)

Theoremdihlss 30591 The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.)

Theoremdihss 30592 The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.)

Theoremdihssxp 30593 An isomorphism H value is included in the vector space (expressed as ). (Contributed by NM, 26-Sep-2014.)

Theoremdihopcl 30594 Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.)

TheoremxihopellsmN 30595* Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.)

Theoremdihopellsm 30596* Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.)

Theoremdihord6apre 30597* Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.)