HomeTheorem List (p. 366 of 426)
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. 366 of 426) | < 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-27775) |
Hilbert Space Explorer
(27776-29300) |
Users' Mathboxes
(29301-42551) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | cdlemn 36501 | Lemma N of [Crawley] p. 121 line 27. (Contributed by NM, 27-Feb-2014.) |
           
                 ![/\](wedge.gif "/\"){kind=small}
   
  | ||
| Theorem | dihordlem6 36502* | Part of proof of Lemma N of [Crawley] p. 122 line 35. (Contributed by NM, 3-Mar-2014.) |
              
      | ||
| Theorem | dihordlem7 36503* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
| ||
| Theorem | dihordlem7b 36504* | Part of proof of Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihjustlem 36505 | 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 36506 | 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 36507 |
Part of proof after Lemma N of [Crawley] p.
122. Forward ordering
property. TODO: change to
using lhpmcvr3 35311, here and all theorems below. (Contributed
by NM,
2-Mar-2014.)
|
| ||
| Theorem | dihord2a 36508 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2b 36509 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2cN 36510* | 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 36511* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
| ||
| Theorem | dihord10 36512* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord11c 36513* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
 
| ||
| Theorem | dihord2pre 36514* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 3-Mar-2014.) |
|
| ||
| Theorem | dihord2pre2 36515* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
|
| ||
| Theorem | dihord2 36516 |
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 36517 | Extend class notation with isomorphism H. |
  | ||
| Definition | df-dih 36518* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
    
   
| ||
| Theorem | dihffval 36519* |
The isomorphism H for a lattice . Definition of isomorphism map
in [Crawley] p. 122 line 3.
(Contributed by NM, 28-Jan-2014.)
|
| ||
| Theorem | dihfval 36520* |
Isomorphism H for a lattice . Definition of isomorphism map in
[Crawley] p. 122 line 3. (Contributed
by NM, 28-Jan-2014.)
|
  
| ||
| Theorem | dihval 36521* |
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 36522* |
Value of isomorphism H for a lattice when .
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihlsscpre 36523 |
Closure of isomorphism H for a lattice when .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcqpre 36524 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalcq 36525 |
Value of isomorphism H for a lattice when , given
auxiliary atom . TODO: Use dihvalcq2 36536 (with lhpmcvr3 35311 for
simplification) that
changes and
to and make this obsolete. Do
to other theorems as well.
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihvalb 36526 |
Value of isomorphism H for a lattice when
.
(Contributed by NM, 4-Mar-2014.)
|
|
| ||
| Theorem | dihopelvalbN 36527* |
Ordered pair member of the partial isomorphism H for argument under
. (Contributed
by NM, 21-Mar-2014.)
(New usage is discouraged.)
|
| ||
| Theorem | dihvalcqat 36528 |
Value of isomorphism H for a lattice at an atom not under .
(Contributed by NM, 27-Mar-2014.)
|
|
| ||
| Theorem | dih1dimb 36529* |
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 36530* |
Isomorphism H at an atom under . (Contributed by NM,
27-Apr-2014.)
|
 | ||
| Theorem | dih1dimc 36531* |
Isomorphism H at an atom not under . (Contributed by NM,
27-Apr-2014.)
|
|
| ||
| Theorem | dib2dim 36532 | Extend dia2dim 36366 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
| ||
| Theorem | dih2dimb 36533 | Extend dib2dim 36532 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
|
| ||
| Theorem | dih2dimbALTN 36534 | Extend dia2dim 36366 to isomorphism H. (This version combines dib2dim 36532 and dih2dimb 36533 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 36535* |
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 36536 |
Value of isomorphism H for a lattice when , given
auxiliary atom . (Contributed by NM, 26-Sep-2014.)
|
|
| ||
| Theorem | dihopelvalcpre 36537* |
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 36538* |
Member of value of isomorphism H for a lattice when
, given auxiliary atom . (Contributed by NM,
13-Mar-2014.)
|
|
| ||
| Theorem | dihlss 36539 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
|
| ||
| Theorem | dihss 36540 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihssxp 36541 |
An isomorphism H value is included in the vector space (expressed as
 ). (Contributed by NM, 26-Sep-2014.)
|
| | ||
| Theorem | dihopcl 36542 | Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.) |
|
| ||
| Theorem | xihopellsmN 36543* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihopellsm 36544* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) |
| ||
| Theorem | dihord6apre 36545* | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
| | ||
| Theorem | dihord3 36546 |
The isomorphism H for a lattice is order-preserving in the region
under co-atom .
(Contributed by NM, 6-Mar-2014.)
|
|
| ||
| Theorem | dihord4 36547 |
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 36548 | 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 36549 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord6a 36550 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5apre 36551 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord5a 36552 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
|
| ||
| Theorem | dihord 36553 | 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 36554 | 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 36555 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
  | ||
| Theorem | dihf11 36556 |
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 36557 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dihdm 36558 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dihcl 36559 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
 | ||
| Theorem | dihcnvcl 36560 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
|
| ||
| Theorem | dihcnvid1 36561 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvid2 36562 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
|
| ||
| Theorem | dihcnvord 36563 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihcnv11 36564 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dihsslss 36565 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
| | ||
| Theorem | dihrnlss 36566 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihrnss 36567 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
|
| ||
| Theorem | dihvalrel 36568 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
 | ||
| Theorem | dih0 36569 | 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 36570 | A lattice element is zero iff its isomorphism is the zero subspace. (Contributed by NM, 16-Aug-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dih0vbN 36571 | 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 36572 | The isomorphism H converse value of the zero subspace is the lattice zero. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dih0rn 36573 | The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.) |
|
| ||
| Theorem | dih0sb 36574 | A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014.) |
|
| ||
| Theorem | dih1 36575 | The value of isomorphism H at the lattice unit is the set of all vectors. (Contributed by NM, 13-Mar-2014.) |
  | ||
| Theorem | dih1rn 36576 | The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dih1cnv 36577 | The isomorphism H converse value of the full vector space is the lattice one. (Contributed by NM, 19-Jun-2014.) |
| | ||
| Theorem | dihwN 36578* |
Value of isomorphism H at the fiducial hyperplane . (Contributed
by NM, 25-Aug-2014.) (New usage is discouraged.)
|
|
| ||
| Theorem | dihmeetlem1N 36579* | Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
 | ||
| Theorem | dihglblem5apreN 36580* | 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 36581 | A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem2aN 36582* | Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.) |
 
 | ||
| Theorem | dihglblem2N 36583* |
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 36584* | Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.) |
| ||
| Theorem | dihglblem3aN 36585* | Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglblem4 36586* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
|
| ||
| Theorem | dihglblem5 36587* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
|
| ||
| Theorem | dihmeetlem2N 36588 | Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihglbcpreN 36589* |
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 36590* |
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 36591 |
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 36592 |
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 36593 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem3N 36594 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem4preN 36595* | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem4N 36596 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
|
| ||
| Theorem | dihmeetlem5 36597 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014.) |
|
| ||
| Theorem | dihmeetlem6 36598 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) |
|
| ||
| Theorem | dihmeetlem7N 36599 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
 | ||
| Theorem | dihjatc1 36600 |
Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we
change
order of here and down?
(Contributed by NM, 6-Apr-2014.)
|
|
| ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |