HomeTheorem List (p. 357 of 370)
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. 357 of 370) | < 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-25511) |
Hilbert Space Explorer
(25512-27036) |
Users' Mathboxes
(27037-36923) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | erngfmul 35601* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
                     ![/\](wedge.gif "/\"){kind=small} 
  
  | ||
| Theorem | erngmul 35602 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
 
| ||
| Theorem | erngfset-rN 35603* |
The division rings on trace-preserving endomorphisms for a lattice
. (Contributed
by NM, 8-Jun-2013.)
(New usage is discouraged.)
|
     
  
 | ||
| Theorem | erngset-rN 35604* |
The division ring on trace-preserving endomorphisms for a fiducial
co-atom .
(Contributed by NM, 5-Jun-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | erngbase-rN 35605 |
The base set of the division ring on trace-preserving endomorphisms is
the set of all trace-preserving endomorphisms (for a fiducial co-atom
).
(Contributed by NM, 9-Jun-2013.)
(New usage is discouraged.)
|
 | ||
| Theorem | erngfplus-rN 35606* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
| ||
| Theorem | erngplus-rN 35607* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
| ||
| Theorem | erngplus2-rN 35608 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
| ||
| Theorem | erngfmul-rN 35609* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | erngmul-rN 35610 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemh1 35611 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
   
 ![./\](_.wedge.gif "./\"){kind=small}
       
 
 | ||
| Theorem | cdlemh2 35612 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.) |
 
  
| ||
| Theorem | cdlemh 35613 | Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
|
| ||
| Theorem | cdlemi1 35614 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
|
| ||
| Theorem | cdlemi2 35615 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
|
| ||
| Theorem | cdlemi 35616 | Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
|
| ||
| Theorem | cdlemj1 35617 | Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
| ||
| Theorem | cdlemj2 35618 |
Part of proof of Lemma J of [Crawley] p. 118.
Eliminate .
(Contributed by NM, 20-Jun-2013.)
|
|
| ||
| Theorem | cdlemj3 35619 |
Part of proof of Lemma J of [Crawley] p. 118.
Eliminate .
(Contributed by NM, 20-Jun-2013.)
|
|
| ||
| Theorem | tendocan 35620 | Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of [Crawley] p. 118. (Contributed by NM, 21-Jun-2013.) |
|
| ||
| Theorem | tendoid0 35621* | A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013.) |
| ||
| Theorem | tendo0mul 35622* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
|
| ||
| Theorem | tendo0mulr 35623* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
|
| ||
| Theorem | tendo1ne0 35624* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
|
| ||
| Theorem | tendoconid 35625* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
|
| ||
| Theorem | tendotr 35626* | The trace of the value of a non-zero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.) |
|
| ||
| Theorem | cdlemk1 35627 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
| ||
| Theorem | cdlemk2 35628 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
|
| ||
| Theorem | cdlemk3 35629 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
|
| ||
| Theorem | cdlemk4 35630 |
Part of proof of Lemma K of [Crawley] p. 118,
last line. We use
for their h, since is already used. (Contributed by NM,
24-Jun-2013.)
|
|
| ||
| Theorem | cdlemk5a 35631 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
|
| ||
| Theorem | cdlemk5 35632 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
|
| ||
| Theorem | cdlemk6 35633 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 34682. (Contributed by NM, 25-Jun-2013.) |
|
| ||
| Theorem | cdlemk8 35634 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
|
| ||
| Theorem | cdlemk9 35635 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
|
| ||
| Theorem | cdlemk9bN 35636 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 35635 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemki 35637* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 35641. (Contributed by NM, 25-Jun-2013.) |
  
| ||
| Theorem | cdlemkvcl 35638 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
|
| ||
| Theorem | cdlemk10 35639 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
|
| ||
| Theorem | cdlemksv 35640* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.) |
|
| ||
| Theorem | cdlemksel 35641* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 35637? (Contributed by NM, 26-Jun-2013.) |
|
| ||
| Theorem | cdlemksat 35642* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
|
| ||
| Theorem | cdlemksv2 35643* |
Part of proof of Lemma K of [Crawley] p. 118.
Value of the sigma(p)
function at
the fixed parameter.
(Contributed by NM,
26-Jun-2013.)
|
|
| ||
| Theorem | cdlemk7 35644* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.) |
|
| ||
| Theorem | cdlemk11 35645* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.) |
|
| ||
| Theorem | cdlemk12 35646* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.) |
|
| ||
| Theorem | cdlemkoatnle 35647* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
|
| ||
| Theorem | cdlemk13 35648* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 13 on p. 119.
, are k1, f1. (Contributed
by NM, 1-Jul-2013.)
|
|
| ||
| Theorem | cdlemkole 35649* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
|
| ||
| Theorem | cdlemk14 35650* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 19 on p. 119.
, are k1, f1. (Contributed
by NM, 1-Jul-2013.)
|
|
| ||
| Theorem | cdlemk15 35651* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 21 on p. 119.
, are k1, f1. (Contributed
by NM, 1-Jul-2013.)
|
|
| ||
| Theorem | cdlemk16a 35652* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
|
| ||
| Theorem | cdlemk16 35653* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
|
| ||
| Theorem | cdlemk17 35654* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 21 on p. 119.
, are k1, f1. (Contributed
by NM, 1-Jul-2013.)
|
|
| ||
| Theorem | cdlemk1u 35655* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
|
| ||
| Theorem | cdlemk5auN 35656* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemk5u 35657* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
|
| ||
| Theorem | cdlemk6u 35658* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 34682. (Contributed by NM, 4-Jul-2013.) |
|
| ||
| Theorem | cdlemkj 35659* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
 
| ||
| Theorem | cdlemkuvN 35660* |
Part of proof of Lemma K of [Crawley] p. 118.
Value of the sigma1 (p)
function .
(Contributed by NM, 2-Jul-2013.)
(New usage is discouraged.)
|
| ||
| Theorem | cdlemkuel 35661* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 35659? (Contributed by NM, 2-Jul-2013.) |
|
| ||
| Theorem | cdlemkuat 35662* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
|
| ||
| Theorem | cdlemkuv2 35663* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 16 on p. 119 for i =
1, where sigma1 (p) is , f1 is , and k1 is .
(Contributed by NM, 2-Jul-2013.)
|
|
| ||
| Theorem | cdlemk18 35664* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 22 on p. 119.
, , , are k, sigma1 (p),
k1, f1.
(Contributed by NM, 2-Jul-2013.)
|
|
| ||
| Theorem | cdlemk19 35665* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 22 on p. 119.
, , , are k, sigma1 (p),
k1, f1.
(Contributed by NM, 2-Jul-2013.)
|
|
| ||
| Theorem | cdlemk7u 35666* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma1 case. (Contributed by NM, 3-Jul-2013.) |
|
| ||
| Theorem | cdlemk11u 35667* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 17, p. 119,
showing Eq. 3 (line 8, p. 119) for the sigma1 () case.
(Contributed by NM, 4-Jul-2013.)
|
|
| ||
| Theorem | cdlemk12u 35668* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 18, p. 119, showing
Eq. 4 (line 10, p. 119) for the sigma1
() case. (Contributed
by
NM, 4-Jul-2013.)
|
|
| ||
| Theorem | cdlemk21N 35669* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemk20 35670* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 22, p. 119 for the
i=2, j=1 case. Note typo on line 22: f should be fi. Our ,
, , , ,
represent their f1, f2, k1,
k2, sigma1, sigma2.
(Contributed by NM, 5-Jul-2013.)
|
|
| ||
| Theorem | cdlemkoatnle-2N 35671* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemk13-2N 35672* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 13 on p. 119.
, are k2, f2. (Contributed
by NM, 1-Jul-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdlemkole-2N 35673* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemk14-2N 35674* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 19 on p. 119.
, are k2, f2. (Contributed
by NM, 1-Jul-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdlemk15-2N 35675* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 21 on p. 119.
, are k2, f2. (Contributed
by NM, 1-Jul-2013.)
(New usage is discouraged.)
|
|
| ||
| Theorem | cdlemk16-2N 35676* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
|
| ||
| Theorem | cdlemk17-2N 35677* |
Part of proof of Lemma K of [Crawley] p. 118.
Line 21 on p. 119.
, are k2, f2. (Contributed
by NM, 1-Jul-2013.)
(New usage is discouraged.)
|
|
| ||