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

 Color key: Metamath Proof Explorer (1-22341) Hilbert Space Explorer (22342-23864) Users' Mathboxes (23865-32387)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremdicvscacl 31614 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 31615 The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.)

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

Theoremdiclspsn 31617* 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 31618* Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.)

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

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

Theoremcdlemn4 31621* 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 31622* Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Theoremdihjustlem 31639 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 31640 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 31641 Part of proof after Lemma N of [Crawley] p. 122. Forward ordering property. TODO: change to using lhpmcvr3 30447, here and all theorems below. (Contributed by NM, 2-Mar-2014.)

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

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

Theoremdihord2cN 31644* 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 31645* Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.)

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

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

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

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

Theoremdihord2 31650 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 31651 Extend class notation with isomorphism H.

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

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

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

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

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

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

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

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

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

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

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

Theoremdih1dimb 31663* 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 31664* Isomorphism H at an atom under . (Contributed by NM, 27-Apr-2014.)

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

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

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

Theoremdih2dimbALTN 31668 Extend dia2dim 31500 to isomorphism H. (This version combines dib2dim 31666 and dih2dimb 31667 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 31669* Ordered pair member of the partial isomorphism H for atom argument not under . TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014.)

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

Theoremdihopelvalcpre 31671* 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 31672* Member of value of isomorphism H for a lattice when , given auxiliary atom . (Contributed by NM, 13-Mar-2014.)

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

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

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

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

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

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

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

Theoremdihord3 31680 The isomorphism H for a lattice is order-preserving in the region under co-atom . (Contributed by NM, 6-Mar-2014.)

Theoremdihord4 31681 The isomorphism H for a lattice is order-preserving in the region not under co-atom . TODO: reformat q e. A /\ -. q .<_ W to eliminate adant*. (Contributed by NM, 6-Mar-2014.)

Theoremdihord5b 31682 Part of proof that isomorphism H is order-preserving. TODO: eliminate 3ad2ant1; combine w/ other way to have one lhpmcvr2 (Contributed by NM, 7-Mar-2014.)

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

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

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

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

Theoremdihord 31687 The isomorphism H is order-preserving. Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.)

Theoremdih11 31688 The isomorphism H is one-to-one. Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.)

Theoremdihf11lem 31689 Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.)

Theoremdihf11 31690 The isomorphism H for a lattice is a one-to-one function. . Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.)

Theoremdihfn 31691 Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.)

Theoremdihdm 31692 Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.)

Theoremdihcl 31693 Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.)

Theoremdihcnvcl 31694 Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.)

Theoremdihcnvid1 31695 The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.)

Theoremdihcnvid2 31696 The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.)

Theoremdihcnvord 31697 Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.)

Theoremdihcnv11 31698 The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.)

Theoremdihsslss 31699 The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.)

Theoremdihrnlss 31700 The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.)

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-3400 35 3401-3500 36 3501-3600 37 3601-3700 38 3701-3800 39 3801-3900 40 3901-4000 41 4001-4100 42 4101-4200 43 4201-4300 44 4301-4400 45 4401-4500 46 4501-4600 47 4601-4700 48 4701-4800 49 4801-4900 50 4901-5000 51 5001-5100 52 5101-5200 53 5201-5300 54 5301-5400 55 5401-5500 56 5501-5600 57 5601-5700 58 5701-5800 59 5801-5900 60 5901-6000 61 6001-6100 62 6101-6200 63 6201-6300 64 6301-6400 65 6401-6500 66 6501-6600 67 6601-6700 68 6701-6800 69 6801-6900 70 6901-7000