HomeTheorem List (p. 343 of 389)
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. 343 of 389) | < 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-26249) |
Hilbert Space Explorer
(26250-27773) |
Users' Mathboxes
(27774-38860) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | dicopelval2 34201* |
Membership in value of the partial isomorphism C for a lattice
 .
(Contributed by NM, 20-Feb-2014.)
|
                       
      ![/\](wedge.gif "/\"){kind=small}       | ||
| Theorem | dicelval2N 34202* |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 25-Feb-2014.) (New usage is discouraged.)
|
 
| ||
| Theorem | dicfnN 34203* | Functionality and domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
     | ||
| Theorem | dicdmN 34204* | Domain of the partial isomorphism C. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
 | ||
| Theorem | dicvalrelN 34205 | The value of partial isomorphism C is a relation. (Contributed by NM, 8-Mar-2014.) (New usage is discouraged.) |
  | ||
| Theorem | dicssdvh 34206 | The partial isomorphism C maps to a set of vectors in full vector space H. (Contributed by NM, 19-Jan-2014.) |
     | ||
| Theorem | dicelval1sta 34207* |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 16-Feb-2014.)
|
|
| ||
| Theorem | dicelval1stN 34208 |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 16-Feb-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dicelval2nd 34209 |
Membership in value of the partial isomorphism C for a lattice .
(Contributed by NM, 16-Feb-2014.)
|
|
| ||
| Theorem | dicvaddcl 34210 | Membership in value of the partial isomorphism C is closed under vector sum. (Contributed by NM, 16-Feb-2014.) |
 
| ||
| Theorem | dicvscacl 34211 | 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 34212 | The value of the partial isomorphism C is not empty. (Contributed by NM, 15-Feb-2014.) |
  | ||
| Theorem | diclss 34213 | The value of partial isomorphism C is a subspace of partial vector space H. (Contributed by NM, 16-Feb-2014.) |
 | ||
| Theorem | diclspsn 34214* |
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 34215* | Part of proof of Lemma N of [Crawley] p. 121 line 30. (Contributed by NM, 21-Feb-2014.) |
 
   
| ||
| Theorem | cdlemn2a 34216* | Part of proof of Lemma N of [Crawley] p. 121. (Contributed by NM, 24-Feb-2014.) |
 
| ||
| Theorem | cdlemn3 34217* | Part of proof of Lemma N of [Crawley] p. 121 line 31. (Contributed by NM, 21-Feb-2014.) |
 | ||
| Theorem | cdlemn4 34218* | 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 34219* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.) |
 
| ||
| Theorem | cdlemn5pre 34220* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
| ||
| Theorem | cdlemn5 34221 | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
|
| ||
| Theorem | cdlemn6 34222* | Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.) |
 | ||
| Theorem | cdlemn7 34223* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
|
| ||
| Theorem | cdlemn8 34224* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
 | ||
| Theorem | cdlemn9 34225* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn10 34226 | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11a 34227* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11b 34228* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11c 34229* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
 
| ||
| Theorem | cdlemn11pre 34230* | Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 34227, cdlemn11b 34228, cdlemn11c 34229, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11 34231 | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn 34232 | Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | dihordlem6 34233* | Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihordlem7 34234* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihordlem7b 34235* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihjustlem 34236 | 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 34237 | 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 34238 |
Part of proof after Lemma N of [Crawley] p.
122. Forward ordering
property. TODO: change to
using lhpmcvr3 33042, here and all theorems below. (Contributed
by NM,
2-Mar-2014.)
|
|
| ||
| Theorem | dihord2a 34239 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2b 34240 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2cN 34241* | 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 34242* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord10 34243* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord11c 34244* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre 34245* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre2 34246* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
|
| ||
| Theorem | dihord2 34247 |
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 34248 | Extend class notation with isomorphism H. |
  | ||
| Definition | df-dih 34249* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
   
  
| ||
| Theorem | dihffval 34250* |
The isomorphism H for a lattice . Definition of isomorphism map
in [Crawley] p. 122 line 3.
(Contributed by NM, 28-Jan-2014.)
|
|
| ||
| Theorem | dihfval 34251* |
Isomorphism H for a lattice . Definition of isomorphism map in
[Crawley] p. 122 line 3. (Contributed
by NM, 28-Jan-2014.)
|
 
| ||
| Theorem | dihval 34252* |
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 34253* |
Value of isomorphism H for a lattice when .
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihlsscpre 34254 |
Closure of isomorphism H for a lattice when .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcqpre 34255 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcq 34256 |
Value of isomorphism H for a lattice when , given
auxiliary atom . TODO: Use dihvalcq2 34267 (with lhpmcvr3 33042 for
simplification) that
changes and
to and make this obsolete. Do
to other theorems as well.
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalb 34257 |
Value of isomorphism H for a lattice when
.
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihopelvalbN 34258* |
Ordered pair member of the partial isomorphism H for argument under
. (Contributed
by NM, 21-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihvalcqat 34259 |
Value of isomorphism H for a lattice at an atom not under .
(Contributed by NM, 27-Mar-2014.)
|
|
| ||
| Theorem | dih1dimb 34260* |
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 34261* |
Isomorphism H at an atom under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dih1dimc 34262* |
Isomorphism H at an atom not under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dib2dim 34263 | Extend dia2dim 34097 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
| ||
| Theorem | dih2dimb 34264 | Extend dib2dim 34263 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
|
| ||
| Theorem | dih2dimbALTN 34265 | Extend dia2dim 34097 to isomorphism H. (This version combines dib2dim 34263 and dih2dimb 34264 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 34266* |
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 34267 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 26-Sep-2014.)
|
|
| ||
| Theorem | dihopelvalcpre 34268* |
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 34269* |
Member of value of isomorphism H for a lattice when
, given auxiliary atom . (Contributed by NM,
13-Mar-2014.)
|
|
| ||
| Theorem | dihlss 34270 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
|
| ||
| Theorem | dihss 34271 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihssxp 34272 |
An isomorphism H value is included in the vector space (expressed as
). (Contributed by NM, 26-Sep-2014.)
|
| | ||
| Theorem | dihopcl 34273 | Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.) |
|
| ||
| Theorem | xihopellsmN 34274* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihopellsm 34275* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) |
| ||
| Theorem | dihord6apre 34276* | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
| | ||
| Theorem | dihord3 34277 |
The isomorphism H for a lattice is order-preserving in the region
under co-atom .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihord4 34278 |
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.)
|
|
| ||
| Theorem | dihord5b 34279 | 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.) |
|
| ||
| Theorem | dihord6b 34280 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord6a 34281 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5apre 34282 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5a 34283 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord 34284 | The isomorphism H is order-preserving. Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dih11 34285 | 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.) |
|
| ||
| Theorem | dihf11lem 34286 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
  | ||
| Theorem | dihf11 34287 |
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.)
|
 | ||
| Theorem | dihfn 34288 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
| | ||
| Theorem | dihdm 34289 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
| | ||
| Theorem | dihcl 34290 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
 | ||
| Theorem | dihcnvcl 34291 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
|
| ||
| Theorem | dihcnvid1 34292 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvid2 34293 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvord 34294 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihcnv11 34295 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihsslss 34296 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
| | ||
| Theorem | dihrnlss 34297 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihrnss 34298 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihvalrel 34299 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
| | ||
| Theorem | dih0 34300 | The value of isomorphism H at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 9-Mar-2014.) |
   | ||
| < Previous Next > |