HomeTheorem List (p. 353 of 360)
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. 353 of 360) | < 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-24492) |
Hilbert Space Explorer
(24493-26017) |
Users' Mathboxes
(26018-35975) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemn4 35201* | 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.) |
                         
   
        ![/\](wedge.gif "/\"){kind=small}      | ||
| Theorem | cdlemn4a 35202* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 24-Feb-2014.) |
   
  | ||
| Theorem | cdlemn5pre 35203* | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
      
| ||
| Theorem | cdlemn5 35204 | Part of proof of Lemma N of [Crawley] p. 121 line 32. (Contributed by NM, 25-Feb-2014.) |
|
| ||
| Theorem | cdlemn6 35205* | Part of proof of Lemma N of [Crawley] p. 121 line 35. (Contributed by NM, 26-Feb-2014.) |
   | ||
| Theorem | cdlemn7 35206* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
|
| ||
| Theorem | cdlemn8 35207* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 26-Feb-2014.) |
 | ||
| Theorem | cdlemn9 35208* | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn10 35209 | Part of proof of Lemma N of [Crawley] p. 121 line 36. (Contributed by NM, 27-Feb-2014.) |
| ||
| Theorem | cdlemn11a 35210* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11b 35211* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11c 35212* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
 
| ||
| Theorem | cdlemn11pre 35213* | Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 35210, cdlemn11b 35211, cdlemn11c 35212, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11 35214 | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn 35215 | Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.) |
 | ||
| Theorem | dihordlem6 35216* | Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihordlem7 35217* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
| ||
| Theorem | dihordlem7b 35218* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihjustlem 35219 | 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 35220 | 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 35221 |
Part of proof after Lemma N of [Crawley] p.
122. Forward ordering
property. TODO: change to
using lhpmcvr3 34027, here and all theorems below. (Contributed
by NM,
2-Mar-2014.)
|
| ||
| Theorem | dihord2a 35222 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2b 35223 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2cN 35224* | 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 35225* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord10 35226* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord11c 35227* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre 35228* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre2 35229* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
|
| ||
| Theorem | dihord2 35230 |
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 35231 | Extend class notation with isomorphism H. |
  | ||
| Definition | df-dih 35232* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
    
   
| ||
| Theorem | dihffval 35233* |
The isomorphism H for a lattice . Definition of isomorphism map
in [Crawley] p. 122 line 3.
(Contributed by NM, 28-Jan-2014.)
|
| ||
| Theorem | dihfval 35234* |
Isomorphism H for a lattice . Definition of isomorphism map in
[Crawley] p. 122 line 3. (Contributed
by NM, 28-Jan-2014.)
|
 
| ||
| Theorem | dihval 35235* |
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 35236* |
Value of isomorphism H for a lattice when .
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihlsscpre 35237 |
Closure of isomorphism H for a lattice when .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcqpre 35238 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcq 35239 |
Value of isomorphism H for a lattice when , given
auxiliary atom . TODO: Use dihvalcq2 35250 (with lhpmcvr3 34027 for
simplification) that
changes and
to and make this obsolete. Do
to other theorems as well.
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalb 35240 |
Value of isomorphism H for a lattice when
.
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihopelvalbN 35241* |
Ordered pair member of the partial isomorphism H for argument under
. (Contributed
by NM, 21-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihvalcqat 35242 |
Value of isomorphism H for a lattice at an atom not under .
(Contributed by NM, 27-Mar-2014.)
|
|
| ||
| Theorem | dih1dimb 35243* |
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 35244* |
Isomorphism H at an atom under . (Contributed by NM,
27-Apr-2014.)
|
 | ||
| Theorem | dih1dimc 35245* |
Isomorphism H at an atom not under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dib2dim 35246 | Extend dia2dim 35080 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
| ||
| Theorem | dih2dimb 35247 | Extend dib2dim 35246 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
|
| ||
| Theorem | dih2dimbALTN 35248 | Extend dia2dim 35080 to isomorphism H. (This version combines dib2dim 35246 and dih2dimb 35247 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 35249* |
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 35250 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 26-Sep-2014.)
|
|
| ||
| Theorem | dihopelvalcpre 35251* |
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 35252* |
Member of value of isomorphism H for a lattice when
, given auxiliary atom . (Contributed by NM,
13-Mar-2014.)
|
|
| ||
| Theorem | dihlss 35253 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
|
| ||
| Theorem | dihss 35254 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihssxp 35255 |
An isomorphism H value is included in the vector space (expressed as
 ). (Contributed by NM, 26-Sep-2014.)
|
| | ||
| Theorem | dihopcl 35256 | Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.) |
|
| ||
| Theorem | xihopellsmN 35257* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihopellsm 35258* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) |
| ||
| Theorem | dihord6apre 35259* | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
| | ||
| Theorem | dihord3 35260 |
The isomorphism H for a lattice is order-preserving in the region
under co-atom .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihord4 35261 |
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 35262 | 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 35263 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord6a 35264 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5apre 35265 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5a 35266 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord 35267 | 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 35268 | 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 35269 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
  | ||
| Theorem | dihf11 35270 |
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 35271 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dihdm 35272 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dihcl 35273 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
 | ||
| Theorem | dihcnvcl 35274 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
|
| ||
| Theorem | dihcnvid1 35275 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvid2 35276 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvord 35277 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihcnv11 35278 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihsslss 35279 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
| | ||
| Theorem | dihrnlss 35280 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihrnss 35281 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihvalrel 35282 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dih0 35283 | 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.) |
   | ||
| Theorem | dih0bN 35284 | A lattice element is zero iff its isomorphism is the zero subspace. (Contributed by NM, 16-Aug-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dih0vbN 35285 | A vector is zero iff its span is the isomorphism of lattice zero. (Contributed by NM, 16-Aug-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dih0cnv 35286 | The isomorphism H converse value of the zero subspace is the lattice zero. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dih0rn 35287 | The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.) |
|
| ||
| Theorem | dih0sb 35288 | A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dih1 35289 | The value of isomorphism H at the lattice unit is the set of all vectors. (Contributed by NM, 13-Mar-2014.) |
  | ||
| Theorem | dih1rn 35290 | The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dih1cnv 35291 | The isomorphism H converse value of the full vector space is the lattice one. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dihwN 35292* |
Value of isomorphism H at the fiducial hyperplane . (Contributed
by NM, 25-Aug-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dihmeetlem1N 35293* | Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
 | ||
| Theorem | dihglblem5apreN 35294* | A conjunction property of isomorphism H. TODO: reduce antecedent size; general review for shorter proof. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem5aN 35295 | A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem2aN 35296* | Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.) |
 
 | ||
| Theorem | dihglblem2N 35297* |
The GLB of a set of lattice elements is the same as that of the
set with
elements of cut down
to be under .
(Contributed by NM, 19-Mar-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dihglblem3N 35298* | Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihglblem3aN 35299* | Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem4 35300* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
|
| ||
| < Previous Next > |