P. 343 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34201-34300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cdlemg38 34201	Use cdlemg37 34175 to eliminate E. r e. A from cdlemg36 34200. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) /\ ( ( ( F ` P ) =/= P /\ ( G ` P ) =/= P ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )
Theorem	cdlemg39 34202	Eliminate =/= conditions from cdlemg38 34201. TODO: Would this better be done at cdlemg35 34199? TODO: Fix comment. (Contributed by NM, 31-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T /\ P =/= Q ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )
Theorem	cdlemg40 34203	Eliminate P =/= Q conditions from cdlemg39 34202. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) ) -> ( ( P .\/ ( F ` ( G ` P ) ) ) ./\ W ) = ( ( Q .\/ ( F ` ( G ` Q ) ) ) ./\ W ) )
Theorem	cdlemg41 34204	Convert cdlemg40 34203 to function composition. TODO: Fix comment. (Contributed by NM, 31-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F e. T /\ G e. T ) ) -> ( ( P .\/ ( ( F o. G ) ` P ) ) ./\ W ) = ( ( Q .\/ ( ( F o. G ) ` Q ) ) ./\ W ) )
Theorem	ltrnco 34205	The composition of two translations is a translation. Part of proof of Lemma G of [Crawley] p. 116, line 15 on p. 117. (Contributed by NM, 31-May-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) e. T )
Theorem	trlcocnv 34206	Swap the arguments of the trace of a composition with converse. (Contributed by NM, 1-Jul-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( R ` ( F o. `' G ) ) = ( R ` ( G o. `' F ) ) )
Theorem	trlcoabs 34207	Absorption into a composition by joining with trace. (Contributed by NM, 22-Jul-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( ( F o. G ) ` P ) .\/ ( R ` F ) ) = ( ( G ` P ) .\/ ( R ` F ) ) )
Theorem	trlcoabs2N 34208	Absorption of the trace of a composition. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( R ` ( G o. `' F ) ) ) = ( ( F ` P ) .\/ ( G ` P ) ) )
Theorem	trlcoat 34209	The trace of a composition of two translations is an atom if their traces are different. (Contributed by NM, 15-Jun-2013.)
|- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. G ) ) e. A )
Theorem	trlcocnvat 34210	Commonly used special case of trlcoat 34209. (Contributed by NM, 1-Jul-2013.)
|- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( R ` ( F o. `' G ) ) e. A )
Theorem	trlconid 34211	The composition of two different translations is not the identity translation. (Contributed by NM, 22-Jul-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) =/= ( _I |` B ) )
Theorem	trlcolem 34212	Lemma for trlco 34213. (Contributed by NM, 1-Jun-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )
Theorem	trlco 34213	The trace of a composition of translations is less than or equal to the join of their traces. Part of proof of Lemma G of [Crawley] p. 116, second paragraph on p. 117. (Contributed by NM, 2-Jun-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( R ` ( F o. G ) ) .<_ ( ( R ` F ) .\/ ( R ` G ) ) )
Theorem	trlcone 34214	If two translations have different traces, the trace of their composition is also different. (Contributed by NM, 14-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( R ` F ) =/= ( R ` G ) /\ G =/= ( _I |` B ) ) ) -> ( R ` F ) =/= ( R ` ( F o. G ) ) )
Theorem	cdlemg42 34215	Part of proof of Lemma G of [Crawley] p. 116, first line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> -. ( G ` P ) .<_ ( P .\/ ( F ` P ) ) )
Theorem	cdlemg43 34216	Part of proof of Lemma G of [Crawley] p. 116, third line of third paragraph on p. 117. (Contributed by NM, 3-Jun-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- ./\ = ( meet ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( F ` ( G ` P ) ) = ( ( ( G ` P ) .\/ ( R ` F ) ) ./\ ( ( F ` P ) .\/ ( R ` G ) ) ) )
Theorem	cdlemg44a 34217	Part of proof of Lemma G of [Crawley] p. 116, fourth line of third paragraph on p. 117: "so fg(p) = gf(p)." (Contributed by NM, 3-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( ( F ` P ) =/= P /\ ( G ` P ) =/= P /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )
Theorem	cdlemg44b 34218	Eliminate ( F ` P ) =/= P, ( G ` P ) =/= P from cdlemg44a 34217. (Contributed by NM, 3-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T /\ ( P e. A /\ -. P .<_ W ) ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F ` ( G ` P ) ) = ( G ` ( F ` P ) ) )
Theorem	cdlemg44 34219	Part of proof of Lemma G of [Crawley] p. 116, fifth line of third paragraph on p. 117: "and hence fg = gf." (Contributed by NM, 3-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( R ` F ) =/= ( R ` G ) ) -> ( F o. G ) = ( G o. F ) )
Theorem	cdlemg47a 34220	TODO: fix comment. TODO: Use this above in place of ( F ` P ) = P antecedents? (Contributed by NM, 5-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ F = ( _I |` B ) ) -> ( F o. G ) = ( G o. F ) )
Theorem	cdlemg46 34221*	Part of proof of Lemma G of [Crawley] p. 116, seventh line of third paragraph on p. 117: "hf and f have different traces." (Contributed by NM, 5-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ h e. T ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( R ` ( h o. F ) ) =/= ( R ` F ) )
Theorem	cdlemg47 34222*	Part of proof of Lemma G of [Crawley] p. 116, ninth line of third paragraph on p. 117: "we conclude that gf = fg." (Contributed by NM, 5-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( h e. T /\ ( R ` F ) = ( R ` G ) ) /\ ( F =/= ( _I |` B ) /\ h =/= ( _I |` B ) /\ ( R ` h ) =/= ( R ` F ) ) ) -> ( F o. G ) = ( G o. F ) )
Theorem	cdlemg48 34223	Elmininate h from cdlemg47 34222. (Contributed by NM, 5-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( F =/= ( _I |` B ) /\ ( R ` F ) = ( R ` G ) ) ) -> ( F o. G ) = ( G o. F ) )
Theorem	ltrncom 34224	Composition is commutative for translations. Part of proof of Lemma G of [Crawley] p. 116 (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( F o. G ) = ( G o. F ) )
Theorem	ltrnco4 34225	Rearrange a composition of 4 translations, analogous to an4 831. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ E e. T /\ F e. T ) -> ( ( D o. E ) o. ( F o. G ) ) = ( ( D o. F ) o. ( E o. G ) ) )
Theorem	trljco 34226	Trace joined with trace of composition. (Contributed by NM, 15-Jun-2013.)
|- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( ( R ` F ) .\/ ( R ` ( F o. G ) ) ) = ( ( R ` F ) .\/ ( R ` G ) ) )
Theorem	trljco2 34227	Trace joined with trace of composition. (Contributed by NM, 16-Jun-2013.)
|- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( ( R ` F ) .\/ ( R ` ( F o. G ) ) ) = ( ( R ` G ) .\/ ( R ` ( F o. G ) ) ) )
Syntax	ctgrp 34228	Extend class notation with translation group.
class TGrp
Definition	df-tgrp 34229*	Define the class of all translation groups. k is normally a member of HL. Each base set is the set of all lattice translations with respect to a hyperplane w, and the operation is function composition. Similar to definition of G in [Crawley] p. 116, third paragraph (which defines this for geomodular lattices). (Contributed by NM, 5-Jun-2013.)
|- TGrp = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { <. ( Base ` ndx ) , ( ( LTrn ` k ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` k ) ` w ) , g e. ( ( LTrn ` k ) ` w ) |-> ( f o. g ) ) >. } ) )
Theorem	tgrpfset 34230*	The translation group maps for a lattice K. (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   =>    |- ( K e. V -> ( TGrp ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( LTrn ` K ) ` w ) >. , <. ( +g ` ndx ) , ( f e. ( ( LTrn ` K ) ` w ) , g e. ( ( LTrn ` K ) ` w ) |-> ( f o. g ) ) >. } ) )
Theorem	tgrpset 34231*	The translation group for a fiducial co-atom W. (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- G = ( ( TGrp ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> G = { <. ( Base ` ndx ) , T >. , <. ( +g ` ndx ) , ( f e. T , g e. T |-> ( f o. g ) ) >. } )
Theorem	tgrpbase 34232	The base set of the translation group is the set of all translations (for a fiducial co-atom W). (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- G = ( ( TGrp ` K ) ` W )   &    |- C = ( Base ` G )   =>    |- ( ( K e. V /\ W e. H ) -> C = T )
Theorem	tgrpopr 34233*	The group operation of the translation group is function composition. (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- G = ( ( TGrp ` K ) ` W )   &    |- .+ = ( +g ` G )   =>    |- ( ( K e. V /\ W e. H ) -> .+ = ( f e. T , g e. T |-> ( f o. g ) ) )
Theorem	tgrpov 34234	The group operation value of the translation group is the composition of translations. (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- G = ( ( TGrp ` K ) ` W )   &    |- .+ = ( +g ` G )   =>    |- ( ( K e. V /\ W e. H /\ ( X e. T /\ Y e. T ) ) -> ( X .+ Y ) = ( X o. Y ) )
Theorem	tgrpgrplem 34235	Lemma for tgrpgrp 34236. (Contributed by NM, 6-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- G = ( ( TGrp ` K ) ` W )   &    |- .+ = ( +g ` G )   &    |- B = ( Base ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> G e. Grp )
Theorem	tgrpgrp 34236	The translation group is a group. (Contributed by NM, 6-Jun-2013.)
|- H = ( LHyp ` K )   &    |- G = ( ( TGrp ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> G e. Grp )
Theorem	tgrpabl 34237	The translation group is an Abelian group. Lemma G of [Crawley] p. 116. (Contributed by NM, 6-Jun-2013.)
|- H = ( LHyp ` K )   &    |- G = ( ( TGrp ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> G e. Abel )
Syntax	ctendo 34238	Extend class notation with translation group endomorphisms.
class TEndo
Syntax	cedring 34239	Extend class notation with division ring on trace-preserving endomorphisms.
class EDRing
Syntax	cedring-rN 34240	Extend class notation with division ring on trace-preserving endomorphisms, with multiplication reversed. TODO: remove EDRingR theorems if not used.
class EDRingR
Definition	df-tendo 34241*	Define trace-preserving endomorphisms on the set of translations. (Contributed by NM, 8-Jun-2013.)
|- TEndo = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f | ( f : ( ( LTrn ` k ) ` w ) --> ( ( LTrn ` k ) ` w ) /\ A. x e. ( ( LTrn ` k ) ` w ) A. y e. ( ( LTrn ` k ) ` w ) ( f ` ( x o. y ) ) = ( ( f ` x ) o. ( f ` y ) ) /\ A. x e. ( ( LTrn ` k ) ` w ) ( ( ( trL ` k ) ` w ) ` ( f ` x ) ) ( le ` k ) ( ( ( trL ` k ) ` w ) ` x ) ) } ) )
Definition	df-edring-rN 34242*	Define division ring on trace-preserving endomorphisms. Definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)
|- EDRingR = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( t o. s ) ) >. } ) )
Definition	df-edring 34243*	Define division ring on trace-preserving endomorphisms. The multiplication operation is reversed composition, per the definition of E of [Crawley] p. 117, 4th line from bottom. (Contributed by NM, 8-Jun-2013.)
|- EDRing = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { <. ( Base ` ndx ) , ( ( TEndo ` k ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` k ) ` w ) , t e. ( ( TEndo ` k ) ` w ) |-> ( s o. t ) ) >. } ) )
Theorem	tendofset 34244*	The set of all trace-preserving endomorphisms on the set of translations for a lattice K. (Contributed by NM, 8-Jun-2013.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. V -> ( TEndo ` K ) = ( w e. H |-> { s | ( s : ( ( LTrn ` K ) ` w ) --> ( ( LTrn ` K ) ` w ) /\ A. f e. ( ( LTrn ` K ) ` w ) A. g e. ( ( LTrn ` K ) ` w ) ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. ( ( LTrn ` K ) ` w ) ( ( ( trL ` K ) ` w ) ` ( s ` f ) ) .<_ ( ( ( trL ` K ) ` w ) ` f ) ) } ) )
Theorem	tendoset 34245*	The set of trace-preserving endomorphisms on the set of translations for a fiducial co-atom W. (Contributed by NM, 8-Jun-2013.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> E = { s | ( s : T --> T /\ A. f e. T A. g e. T ( s ` ( f o. g ) ) = ( ( s ` f ) o. ( s ` g ) ) /\ A. f e. T ( R ` ( s ` f ) ) .<_ ( R ` f ) ) } )
Theorem	istendo 34246*	The predicate "is a trace-preserving endomorphism". Similar to definition of trace-preserving endomorphism in [Crawley] p. 117, penultimate line. (Contributed by NM, 8-Jun-2013.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> ( S e. E <-> ( S : T --> T /\ A. f e. T A. g e. T ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) /\ A. f e. T ( R ` ( S ` f ) ) .<_ ( R ` f ) ) ) )
Theorem	tendotp 34247	Trace-preserving property of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ S e. E /\ F e. T ) -> ( R ` ( S ` F ) ) .<_ ( R ` F ) )
Theorem	istendod 34248*	Deduce the predicate "is a trace-preserving endomorphism". (Contributed by NM, 9-Jun-2013.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- ( ph -> ( K e. V /\ W e. H ) )   &    |- ( ph -> S : T --> T )   &    |- ( ( ph /\ f e. T /\ g e. T ) -> ( S ` ( f o. g ) ) = ( ( S ` f ) o. ( S ` g ) ) )   &    |- ( ( ph /\ f e. T ) -> ( R ` ( S ` f ) ) .<_ ( R ` f ) )   =>    |- ( ph -> S e. E )
Theorem	tendof 34249	Functionality of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ S e. E ) -> S : T --> T )
Theorem	tendoeq1 34250*	Condition determining equality of two trace-preserving endomorphisms. (Contributed by NM, 11-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( U ` f ) = ( V ` f ) ) -> U = V )
Theorem	tendovalco 34251	Value of composition of translations in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H /\ S e. E ) /\ ( F e. T /\ G e. T ) ) -> ( S ` ( F o. G ) ) = ( ( S ` F ) o. ( S ` G ) ) )
Theorem	tendocoval 34252	Value of composition of endomorphisms in a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U o. V ) ` F ) = ( U ` ( V ` F ) ) )
Theorem	tendocl 34253	Closure of a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ S e. E /\ F e. T ) -> ( S ` F ) e. T )
Theorem	tendoco2 34254	Distribution of compositions in preparation for endomorphism sum definition. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( F e. T /\ G e. T ) ) -> ( ( U ` ( F o. G ) ) o. ( V ` ( F o. G ) ) ) = ( ( ( U ` F ) o. ( V ` F ) ) o. ( ( U ` G ) o. ( V ` G ) ) ) )
Theorem	tendoidcl 34255	The identity is a trace-preserving endomorphism. (Contributed by NM, 30-Jul-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> ( _I |` T ) e. E )
Theorem	tendo1mul 34256	Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( ( _I |` T ) o. U ) = U )
Theorem	tendo1mulr 34257	Multiplicative identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 20-Nov-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ U e. E ) -> ( U o. ( _I |` T ) ) = U )
Theorem	tendococl 34258	The composition of two trace-preserving endomorphisms (multiplication in the endormorphism ring) is a trace-preserving endomorphism. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E /\ T e. E ) -> ( S o. T ) e. E )
Theorem	tendoid 34259	The identity value of a trace-preserving endomorphism. (Contributed by NM, 21-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S ` ( _I |` B ) ) = ( _I |` B ) )
Theorem	tendoeq2 34260*	Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 34310, we show that we only need to consider a single non-identity translation. (Contributed by NM, 21-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ A. f e. T ( f =/= ( _I |` B ) -> ( U ` f ) = ( V ` f ) ) ) -> U = V )
Theorem	tendoplcbv 34261*	Define sum operation for trace-perserving endomorphisms. Change bound variables to isolate them later. (Contributed by NM, 11-Jun-2013.)
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- P = ( u e. E , v e. E |-> ( g e. T |-> ( ( u ` g ) o. ( v ` g ) ) ) )
Theorem	tendopl 34262*	Value of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.)
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( U e. E /\ V e. E ) -> ( U P V ) = ( g e. T |-> ( ( U ` g ) o. ( V ` g ) ) ) )
Theorem	tendopl2 34263*	Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.)
|- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( U e. E /\ V e. E /\ F e. T ) -> ( ( U P V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
Theorem	tendoplcl2 34264*	Value of result of endomorphism sum operation. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( ( U P V ) ` F ) e. T )
Theorem	tendoplco2 34265*	Value of result of endomorphism sum operation on a translation composition. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ ( F e. T /\ G e. T ) ) -> ( ( U P V ) ` ( F o. G ) ) = ( ( ( U P V ) ` F ) o. ( ( U P V ) ` G ) ) )
Theorem	tendopltp 34266*	Trace-preserving property of endomorphism sum operation P, based on theorem trlco 34213. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 34213) that Delta is a subring of E." (In our development, we will bypass their E and go directly to their Delta, whose base set is our ( TEndo ` K ) ` W.) (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- .<_ = ( le ` K )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) /\ F e. T ) -> ( R ` ( ( U P V ) ` F ) ) .<_ ( R ` F ) )
Theorem	tendoplcl 34267*	Endomorphism sum is a trace-preserving endomorphism. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) e. E )
Theorem	tendoplcom 34268*	The endomorphism sum operation is commutative. (Contributed by NM, 11-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ U e. E /\ V e. E ) -> ( U P V ) = ( V P U ) )
Theorem	tendoplass 34269*	The endomorphism sum operation is associative. (Contributed by NM, 11-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) P V ) = ( S P ( U P V ) ) )
Theorem	tendodi1 34270*	Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( S o. ( U P V ) ) = ( ( S o. U ) P ( S o. V ) ) )
Theorem	tendodi2 34271*	Endomorphism composition distributes over sum. (Contributed by NM, 13-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( S e. E /\ U e. E /\ V e. E ) ) -> ( ( S P U ) o. V ) = ( ( S o. V ) P ( U o. V ) ) )
Theorem	tendo0cbv 34272*	Define additive identity for trace-perserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 11-Jun-2013.)
|- O = ( f e. T |-> ( _I |` B ) )   =>    |- O = ( g e. T |-> ( _I |` B ) )
Theorem	tendo02 34273*	Value of additive identity endomorphism. (Contributed by NM, 11-Jun-2013.)
|- O = ( f e. T |-> ( _I |` B ) )   &    |- B = ( Base ` K )   =>    |- ( F e. T -> ( O ` F ) = ( _I |` B ) )
Theorem	tendo0co2 34274*	The additive identity trace-perserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 34507? (Contributed by NM, 11-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( O ` ( F o. G ) ) = ( ( O ` F ) o. ( O ` G ) ) )
Theorem	tendo0tp 34275*	Trace-preserving property of endomorphism additive identity. (Contributed by NM, 11-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   &    |- .<_ = ( le ` K )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` ( O ` F ) ) .<_ ( R ` F ) )
Theorem	tendo0cl 34276*	The additive identity is a trace-perserving endormorphism. (Contributed by NM, 12-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( K e. HL /\ W e. H ) -> O e. E )
Theorem	tendo0pl 34277*	Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( O P S ) = S )
Theorem	tendo0plr 34278*	Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S P O ) = S )
Theorem	tendoicbv 34279*	Define inverse function for trace-perserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.)
|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )   =>    |- I = ( u e. E |-> ( g e. T |-> `' ( u ` g ) ) )
Theorem	tendoi 34280*	Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( S e. E -> ( I ` S ) = ( g e. T |-> `' ( S ` g ) ) )
Theorem	tendoi2 34281*	Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
|- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( S e. E /\ F e. T ) -> ( ( I ` S ) ` F ) = `' ( S ` F ) )
Theorem	tendoicl 34282*	Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( I ` S ) e. E )
Theorem	tendoipl 34283*	Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )   &    |- B = ( Base ` K )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( ( I ` S ) P S ) = O )
Theorem	tendoipl2 34284*	Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- I = ( s e. E |-> ( f e. T |-> `' ( s ` f ) ) )   &    |- B = ( Base ` K )   &    |- P = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ S e. E ) -> ( S P ( I ` S ) ) = O )
Theorem	erngfset 34285*	The division rings on trace-preserving endomorphisms for a lattice K. (Contributed by NM, 8-Jun-2013.)
|- H = ( LHyp ` K )   =>    |- ( K e. V -> ( EDRing ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( s o. t ) ) >. } ) )
Theorem	erngset 34286*	The division ring on trace-preserving endomorphisms for a fiducial co-atom W. (Contributed by NM, 5-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> D = { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( s o. t ) ) >. } )
Theorem	erngbase 34287	The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom W). TODO: the .t hypothesis isn't used. (Also look at others.) (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- C = ( Base ` D )   =>    |- ( ( K e. V /\ W e. H ) -> C = E )
Theorem	erngfplus 34288*	Ring addition operation. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- .+ = ( +g ` D )   =>    |- ( ( K e. V /\ W e. H ) -> .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )
Theorem	erngplus 34289*	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- .+ = ( +g ` D )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .+ V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )
Theorem	erngplus2 34290	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- .+ = ( +g ` D )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> ( ( U .+ V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
Theorem	erngfmul 34291*	Ring multiplication operation. (Contributed by NM, 9-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- .x. = ( .r ` D )   =>    |- ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , t e. E |-> ( s o. t ) ) )
Theorem	erngmul 34292	Ring addition operation. (Contributed by NM, 10-Jun-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRing ` K ) ` W )   &    |- .x. = ( .r ` D )   =>    |- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .x. V ) = ( U o. V ) )
Theorem	erngfset-rN 34293*	The division rings on trace-preserving endomorphisms for a lattice K. (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   =>    |- ( K e. V -> ( EDRingR ` K ) = ( w e. H |-> { <. ( Base ` ndx ) , ( ( TEndo ` K ) ` w ) >. , <. ( +g ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. ( ( TEndo ` K ) ` w ) , t e. ( ( TEndo ` K ) ` w ) |-> ( t o. s ) ) >. } ) )
Theorem	erngset-rN 34294*	The division ring on trace-preserving endomorphisms for a fiducial co-atom W. (Contributed by NM, 5-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   =>    |- ( ( K e. V /\ W e. H ) -> D = { <. ( Base ` ndx ) , E >. , <. ( +g ` ndx ) , ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) >. , <. ( .r ` ndx ) , ( s e. E , t e. E |-> ( t o. s ) ) >. } )
Theorem	erngbase-rN 34295	The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom W). (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   &    |- C = ( Base ` D )   =>    |- ( ( K e. V /\ W e. H ) -> C = E )
Theorem	erngfplus-rN 34296*	Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   &    |- .+ = ( +g ` D )   =>    |- ( ( K e. V /\ W e. H ) -> .+ = ( s e. E , t e. E |-> ( f e. T |-> ( ( s ` f ) o. ( t ` f ) ) ) ) )
Theorem	erngplus-rN 34297*	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   &    |- .+ = ( +g ` D )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .+ V ) = ( f e. T |-> ( ( U ` f ) o. ( V ` f ) ) ) )
Theorem	erngplus2-rN 34298	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   &    |- .+ = ( +g ` D )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ F e. T ) ) -> ( ( U .+ V ) ` F ) = ( ( U ` F ) o. ( V ` F ) ) )
Theorem	erngfmul-rN 34299*	Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   &    |- .x. = ( .r ` D )   =>    |- ( ( K e. V /\ W e. H ) -> .x. = ( s e. E , t e. E |-> ( t o. s ) ) )
Theorem	erngmul-rN 34300	Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- D = ( ( EDRingR ` K ) ` W )   &    |- .x. = ( .r ` D )   =>    |- ( ( ( K e. X /\ W e. H ) /\ ( U e. E /\ V e. E ) ) -> ( U .x. V ) = ( V o. U ) )