HomeTheorem List (p. 348 of 399)
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. 348 of 399) | < 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-26563) |
Hilbert Space Explorer
(26564-28086) |
Users' Mathboxes
(28087-39846) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemn11b 34701* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
           
                                     ![/\](wedge.gif "/\"){kind=small}
 
     | ||
| Theorem | cdlemn11c 34702* | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
 
| ||
| Theorem | cdlemn11pre 34703* | Part of proof of Lemma N of [Crawley] p. 121 line 37. TODO: combine cdlemn11a 34700, cdlemn11b 34701, cdlemn11c 34702, cdlemn11pre into one? (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn11 34704 | Part of proof of Lemma N of [Crawley] p. 121 line 37. (Contributed by NM, 27-Feb-2014.) |
|
| ||
| Theorem | cdlemn 34705 | Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.) |
 | ||
| Theorem | dihordlem6 34706* | Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.) |
   | ||
| Theorem | dihordlem7 34707* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
| ||
| Theorem | dihordlem7b 34708* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihjustlem 34709 | 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 34710 | 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 34711 |
Part of proof after Lemma N of [Crawley] p.
122. Forward ordering
property. TODO: change to
using lhpmcvr3 33515, here and all theorems below. (Contributed
by NM,
2-Mar-2014.)
|
| ||
| Theorem | dihord2a 34712 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2b 34713 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2cN 34714* | 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 34715* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord10 34716* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord11c 34717* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre 34718* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre2 34719* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
|
| ||
| Theorem | dihord2 34720 |
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 34721 | Extend class notation with isomorphism H. |
  | ||
| Definition | df-dih 34722* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
    
   
| ||
| Theorem | dihffval 34723* |
The isomorphism H for a lattice . Definition of isomorphism map
in [Crawley] p. 122 line 3.
(Contributed by NM, 28-Jan-2014.)
|
| ||
| Theorem | dihfval 34724* |
Isomorphism H for a lattice . Definition of isomorphism map in
[Crawley] p. 122 line 3. (Contributed
by NM, 28-Jan-2014.)
|
  
| ||
| Theorem | dihval 34725* |
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 34726* |
Value of isomorphism H for a lattice when .
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihlsscpre 34727 |
Closure of isomorphism H for a lattice when .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcqpre 34728 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcq 34729 |
Value of isomorphism H for a lattice when , given
auxiliary atom . TODO: Use dihvalcq2 34740 (with lhpmcvr3 33515 for
simplification) that
changes and
to and make this obsolete. Do
to other theorems as well.
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalb 34730 |
Value of isomorphism H for a lattice when
.
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihopelvalbN 34731* |
Ordered pair member of the partial isomorphism H for argument under
. (Contributed
by NM, 21-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihvalcqat 34732 |
Value of isomorphism H for a lattice at an atom not under .
(Contributed by NM, 27-Mar-2014.)
|
|
| ||
| Theorem | dih1dimb 34733* |
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 34734* |
Isomorphism H at an atom under . (Contributed by NM,
27-Apr-2014.)
|
 | ||
| Theorem | dih1dimc 34735* |
Isomorphism H at an atom not under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dib2dim 34736 | Extend dia2dim 34570 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
| ||
| Theorem | dih2dimb 34737 | Extend dib2dim 34736 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
|
| ||
| Theorem | dih2dimbALTN 34738 | Extend dia2dim 34570 to isomorphism H. (This version combines dib2dim 34736 and dih2dimb 34737 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 34739* |
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 34740 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 26-Sep-2014.)
|
|
| ||
| Theorem | dihopelvalcpre 34741* |
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 34742* |
Member of value of isomorphism H for a lattice when
, given auxiliary atom . (Contributed by NM,
13-Mar-2014.)
|
|
| ||
| Theorem | dihlss 34743 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
|
| ||
| Theorem | dihss 34744 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihssxp 34745 |
An isomorphism H value is included in the vector space (expressed as
 ). (Contributed by NM, 26-Sep-2014.)
|
| | ||
| Theorem | dihopcl 34746 | Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.) |
|
| ||
| Theorem | xihopellsmN 34747* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihopellsm 34748* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) |
| ||
| Theorem | dihord6apre 34749* | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
| | ||
| Theorem | dihord3 34750 |
The isomorphism H for a lattice is order-preserving in the region
under co-atom .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihord4 34751 |
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 34752 | 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 34753 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord6a 34754 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5apre 34755 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5a 34756 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord 34757 | 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 34758 | 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 34759 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
  | ||
| Theorem | dihf11 34760 |
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 34761 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dihdm 34762 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dihcl 34763 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
 | ||
| Theorem | dihcnvcl 34764 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
|
| ||
| Theorem | dihcnvid1 34765 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvid2 34766 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvord 34767 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihcnv11 34768 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihsslss 34769 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
| | ||
| Theorem | dihrnlss 34770 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihrnss 34771 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihvalrel 34772 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dih0 34773 | 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 34774 | A lattice element is zero iff its isomorphism is the zero subspace. (Contributed by NM, 16-Aug-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dih0vbN 34775 | 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 34776 | The isomorphism H converse value of the zero subspace is the lattice zero. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dih0rn 34777 | The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.) |
|
| ||
| Theorem | dih0sb 34778 | A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dih1 34779 | The value of isomorphism H at the lattice unit is the set of all vectors. (Contributed by NM, 13-Mar-2014.) |
  | ||
| Theorem | dih1rn 34780 | The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dih1cnv 34781 | The isomorphism H converse value of the full vector space is the lattice one. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dihwN 34782* |
Value of isomorphism H at the fiducial hyperplane . (Contributed
by NM, 25-Aug-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dihmeetlem1N 34783* | Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
 | ||
| Theorem | dihglblem5apreN 34784* | 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 34785 | A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem2aN 34786* | Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.) |
 
 | ||
| Theorem | dihglblem2N 34787* |
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 34788* | Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihglblem3aN 34789* | Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem4 34790* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
|
| ||
| Theorem | dihglblem5 34791* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
|
| ||
| Theorem | dihmeetlem2N 34792 | Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglbcpreN 34793* |
Isomorphism H of a lattice glb when the glb is not under the fiducial
hyperplane .
(Contributed by NM, 20-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihglbcN 34794* |
Isomorphism H of a lattice glb when the glb is not under the fiducial
hyperplane .
(Contributed by NM, 26-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihmeetcN 34795 |
Isomorphism H of a lattice meet when the meet is not under the fiducial
hyperplane .
(Contributed by NM, 26-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihmeetbN 34796 |
Isomorphism H of a lattice meet when one element is under the fiducial
hyperplane .
(Contributed by NM, 26-Mar-2014.)
(New usage is discouraged.)
|
|
| ||
| Theorem | dihmeetbclemN 34797 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem3N 34798 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem4preN 34799* | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem4N 34800 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |