HomeTheorem List (p. 374 of 386)
Unicode version.
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List
| Home |
Metamath
Proof Explorer Theorem List (p. 374 of 386) | < 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-26036) |
Hilbert Space Explorer
(26037-27561) |
Users' Mathboxes
(27562-38552) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dibeldmN 37301 | Member of domain of the partial isomorphism B. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
                   ![/\](wedge.gif "/\"){kind=small}     | ||
| Theorem | dibord 37302 |
The isomorphism B for a lattice is order-preserving in the region
under co-atom .
(Contributed by NM, 24-Feb-2014.)
|
| ||
| Theorem | dib11N 37303 |
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 37304 |
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 37305 |
Closure of partial isomorphism B for a lattice . (Contributed by
NM, 8-Mar-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dibvalrel 37306 | The value of partial isomorphism B is a relation. (Contributed by NM, 8-Mar-2014.) |
 | ||
| Theorem | dib0 37307 | 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 37308* | 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 37309* | Partial isomorphism B of a lattice glb. (Contributed by NM, 9-Mar-2014.) (New usage is discouraged.) |
  
    | ||
| Theorem | dibintclN 37310 | The intersection of partial isomorphism B closed subspaces is a closed subspace. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
 | ||
| Theorem | dib1dim2 37311* |
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 37312 | The partial isomorphism B maps to a set of vectors in full vector space H. (Contributed by NM, 1-Jan-2014.) |
|
| ||
| Theorem | diblss 37313 | 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 37314* | Membership in subspace sum for partial isomorphism B. (Contributed by NM, 21-Sep-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
   
  
| ||
| Syntax | cdic 37315 | Extend class notation with isomorphism C. |
  | ||
| Definition | df-dic 37316* |
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 37317* |
The partial isomorphism C for a lattice . (Contributed by NM,
15-Dec-2013.)
|
| ||
| Theorem | dicfval 37318* |
The partial isomorphism C for a lattice . (Contributed by NM,
15-Dec-2013.)
|
| ||
| Theorem | dicval 37319* |
The partial isomorphism C for a lattice . (Contributed by NM,
15-Dec-2013.) (Revised by Mario Carneiro, 22-Sep-2015.)
|
| ||
| Theorem | dicopelval 37320* |
Membership in value of the partial isomorphism C for a lattice
.
(Contributed by NM, 15-Feb-2014.)
|
|
| ||
| Theorem | dicelvalN 37321* |
Membership in value of the partial isomorphism C for a lattice
.
(Contributed by NM, 25-Feb-2014.)
(New usage is discouraged.)
|
| ||
| Theorem | dicval2 37322* |
The partial isomorphism C for a lattice . (Contributed by NM,
20-Feb-2014.)
|
|
| ||
| Theorem | dicelval3 37323* | Member of the partial isomorphism C. (Contributed by NM, 26-Feb-2014.) |
|
| ||
| Theorem | dicopelval2 37324* |
Membership in value of the partial isomorphism C for a lattice
.
(Contributed by NM, 20-Feb-2014.)
|
|
| ||
| Theorem | dicelval2N 37325* |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dicfnN 37326* | Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
  | ||
| Theorem | dicdmN 37327* | Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
| | ||
| Theorem | dicvalrelN 37328 | The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
| | ||
| Theorem | dicssdvh 37329 | The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014.) |
| | ||
| Theorem | dicelval1sta 37330* |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 16-Feb-2014.)
|
|
| ||
| Theorem | dicelval1stN 37331 |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 16-Feb-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dicelval2nd 37332 |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 16-Feb-2014.)
|
|
| ||
| Theorem | dicvaddcl 37333 | Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014.) |
 
| ||
| Theorem | dicvscacl 37334 | 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 37335 | The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.) |
|
| ||
| Theorem | diclss 37336 | The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014.) |
| | ||
| Theorem | diclspsn 37337* |
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 37338* | Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.) |
| ||
| Theorem | cdlemn2a 37339* | Part of proof of Lemma N of [Crawley] p. 121. (Contributed by NM, 24-Feb-2014.) |
|
| ||
| Theorem | cdlemn3 37340* | Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) |
 | ||
| Theorem | cdlemn4 37341* | 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 37342* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.) |
|
| ||
| Theorem | cdlemn5pre 37343* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
| ||
| Theorem | cdlemn5 37344 | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
|
| ||
| Theorem | cdlemn6 37345* | Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.) |
|
| ||
| Theorem | cdlemn7 37346* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
|
| ||
| Theorem | cdlemn8 37347* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
 | ||
| Theorem | cdlemn9 37348* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn10 37349 | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11a 37350* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11b 37351* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11c 37352* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
| ||
| Theorem | cdlemn11pre 37353* | Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 37350, cdlemn11b 37351, cdlemn11c 37352, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11 37354 | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn 37355 | Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | dihordlem6 37356* | Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihordlem7 37357* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihordlem7b 37358* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihjustlem 37359 | 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.) |
![./\](_.wedge.gif "./\"){kind=small}
| ||
| Theorem | dihjust 37360 | 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 37361 |
Part of proof after Lemma N of [Crawley] p.
122. Forward ordering
property. TODO: change to
using lhpmcvr3 36165, here and all theorems below. (Contributed
by NM,
2-Mar-2014.)
|
|
| ||
| Theorem | dihord2a 37362 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2b 37363 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2cN 37364* | 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 37365* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord10 37366* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord11c 37367* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre 37368* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre2 37369* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
|
| ||
| Theorem | dihord2 37370 |
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 37371 | Extend class notation with isomorphism H. |
 | ||
| Definition | df-dih 37372* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
 
| ||
| Theorem | dihffval 37373* |
The isomorphism H for a lattice . Definition of isomorphism map
in [Crawley] p. 122 line 3.
(Contributed by NM, 28-Jan-2014.)
|
|
| ||
| Theorem | dihfval 37374* |
Isomorphism H for a lattice . Definition of isomorphism map in
[Crawley] p. 122 line 3. (Contributed
by NM, 28-Jan-2014.)
|
 
| ||
| Theorem | dihval 37375* |
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 37376* |
Value of isomorphism H for a lattice when .
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihlsscpre 37377 |
Closure of isomorphism H for a lattice when .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcqpre 37378 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcq 37379 |
Value of isomorphism H for a lattice when , given
auxiliary atom . TODO: Use dihvalcq2 37390 (with lhpmcvr3 36165 for
simplification) that
changes and
to and make this obsolete. Do
to other theorems as well.
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalb 37380 |
Value of isomorphism H for a lattice when
.
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihopelvalbN 37381* |
Ordered pair member of the partial isomorphism H for argument under
. (Contributed
by NM, 21-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihvalcqat 37382 |
Value of isomorphism H for a lattice at an atom not under .
(Contributed by NM, 27-Mar-2014.)
|
|
| ||
| Theorem | dih1dimb 37383* |
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 37384* |
Isomorphism H at an atom under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dih1dimc 37385* |
Isomorphism H at an atom not under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dib2dim 37386 | Extend dia2dim 37220 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
|
| ||
| Theorem | dih2dimb 37387 | Extend dib2dim 37386 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
|
| ||
| Theorem | dih2dimbALTN 37388 | Extend dia2dim 37220 to isomorphism H. (This version combines dib2dim 37386 and dih2dimb 37387 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 37389* |
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 37390 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 26-Sep-2014.)
|
|
| ||
| Theorem | dihopelvalcpre 37391* |
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 37392* |
Member of value of isomorphism H for a lattice when
, given auxiliary atom . (Contributed by NM,
13-Mar-2014.)
|
|
| ||
| Theorem | dihlss 37393 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
|
| ||
| Theorem | dihss 37394 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihssxp 37395 |
An isomorphism H value is included in the vector space (expressed as
). (Contributed by NM, 26-Sep-2014.)
|
| | ||
| Theorem | dihopcl 37396 | Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.) |
|
| ||
| Theorem | xihopellsmN 37397* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihopellsm 37398* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) |
| ||
| Theorem | dihord6apre 37399* | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
| | ||