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

Color key: | Metamath Proof Explorer
(1-21444) |
Hilbert Space Explorer
(21445-22967) |
Users' Mathboxes
(22968-31305) |

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

Statement | ||

Theorem | dib11N 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.) |

Theorem | dibf11N 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.) |

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

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

Theorem | dib0 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.) |

Theorem | dib1dim 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.) |

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

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

Theorem | dib1dim2 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.) |

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

Theorem | diblss 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.) |

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

Syntax | cdic 30513 | Extend class notation with isomorphism C. |

Definition | df-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.) |

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theorem | dicvscacl 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.) |

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

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

Theorem | diclspsn 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.) |

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

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

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

Theorem | cdlemn4 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.) |

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

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

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

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

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

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

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

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

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

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

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

Theorem | cdlemn11pre 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.) |

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

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

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

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

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

Theorem | dihjustlem 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.) |

Theorem | dihjust 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.) |

Theorem | dihord1 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.) |

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

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

Theorem | dihord2cN 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.) |

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

Theorem | dihord10 30564* | |

Theorem | dihord11c 30565* | |

Theorem | dihord2pre 30566* | |

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

Theorem | dihord2 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.) |

Syntax | cdih 30569 | Extend class notation with isomorphism H. |

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

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

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

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

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

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

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

Theorem | dihvalcq 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.) |

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

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

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

Theorem | dih1dimb 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.) |

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

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

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

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

Theorem | dih2dimbALTN 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.) |

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

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

Theorem | dihopelvalcpre 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.) |

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

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

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

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

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

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

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

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