P. 367 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 36601-36700   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cdlemg44b 36601	Eliminate ( F ` P ) =/= P, ( G ` P ) =/= P from cdlemg44a 36600. (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 36602	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 36603	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 36604*	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 36605*	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 36606	Elmininate h from cdlemg47 36605. (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 36607	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 36608	Rearrange a composition of 4 translations, analogous to an4 824. (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 36609	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 36610	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 36611	Extend class notation with translation group.
class TGrp
Definition	df-tgrp 36612*	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 36613*	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 36614*	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 36615	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 36616*	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 36617	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 36618	Lemma for tgrpgrp 36619. (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 36619	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 36620	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 36621	Extend class notation with translation group endomorphisms.
class TEndo
Syntax	cedring 36622	Extend class notation with division ring on trace-preserving endomorphisms.
class EDRing
Syntax	cedring-rN 36623	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 36624*	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 36625*	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 36626*	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 36627*	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 36628*	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 36629*	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 36630	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 36631*	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 36632	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 36633*	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 36634	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 36635	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 36636	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 36637	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 36638	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 36639	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 36640	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 36641	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 36642	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 36643*	Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 36693, 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 36644*	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 36645*	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 36646*	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 36647*	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 36648*	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 36649*	Trace-preserving property of endomorphism sum operation P, based on theorem trlco 36596. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 36596) 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 36650*	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 36651*	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 36652*	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 36653*	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 36654*	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 36655*	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 36656*	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 36657*	The additive identity trace-perserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 36890? (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 36658*	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 36659*	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 36660*	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 36661*	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 36662*	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 36663*	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 36664*	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 36665*	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 36666*	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 36667*	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 36668*	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 36669*	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 36670	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 36671*	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 36672*	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 36673	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 36674*	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 36675	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 36676*	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 36677*	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 36678	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 36679*	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 36680*	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 36681	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 36682*	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 36683	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 ) )
Theorem	cdlemh1 36684	Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- S = ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( P e. A /\ Q e. A ) /\ ( Q .<_ ( P .\/ ( R ` F ) ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( S .\/ ( R ` ( G o. `' F ) ) ) = ( Q .\/ ( R ` ( G o. `' F ) ) ) )
Theorem	cdlemh2 36685	Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- S = ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) )   &    |- .0. = ( 0. ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( S ./\ W ) = .0. )
Theorem	cdlemh 36686	Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- S = ( ( P .\/ ( R ` G ) ) ./\ ( Q .\/ ( R ` ( G o. `' F ) ) ) )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ Q .<_ ( P .\/ ( R ` F ) ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( S e. A /\ -. S .<_ W ) )
Theorem	cdlemi1 36687	Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( U ` G ) ` P ) .<_ ( P .\/ ( R ` G ) ) )
Theorem	cdlemi2 36688	Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( U ` G ) ` P ) .<_ ( ( ( U ` F ) ` P ) .\/ ( R ` ( G o. `' F ) ) ) )
Theorem	cdlemi 36689	Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- S = ( ( P .\/ ( R ` G ) ) ./\ ( ( ( U ` F ) ` P ) .\/ ( R ` ( G o. `' F ) ) ) )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) /\ ( U e. E /\ ( P e. A /\ -. P .<_ W ) ) /\ ( F =/= ( _I |` B ) /\ G =/= ( _I |` B ) /\ ( R ` F ) =/= ( R ` G ) ) ) -> ( ( U ` G ) ` P ) = S )
Theorem	cdlemj1 36690	Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) /\ ( p e. A /\ -. p .<_ W ) ) ) -> ( ( U ` h ) ` p ) = ( ( V ` h ) ` p ) )
Theorem	cdlemj2 36691	Part of proof of Lemma J of [Crawley] p. 118. Eliminate p. (Contributed by NM, 20-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ ( h =/= ( _I |` B ) /\ g e. T /\ g =/= ( _I |` B ) ) /\ ( ( R ` F ) =/= ( R ` g ) /\ ( R ` g ) =/= ( R ` h ) ) ) -> ( U ` h ) = ( V ` h ) )
Theorem	cdlemj3 36692	Part of proof of Lemma J of [Crawley] p. 118. Eliminate g. (Contributed by NM, 20-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ V e. E /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) /\ h e. T ) ) /\ h =/= ( _I |` B ) ) -> ( U ` h ) = ( V ` h ) )
Theorem	tendocan 36693	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.)
|- 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 /\ ( U ` F ) = ( V ` F ) ) /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> U = V )
Theorem	tendoid0 36694*	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.)
|- 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 ) /\ U e. E /\ ( F e. T /\ F =/= ( _I |` B ) ) ) -> ( ( U ` F ) = ( _I |` B ) <-> U = O ) )
Theorem	tendo0mul 36695*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-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 ) /\ U e. E ) -> ( O o. U ) = O )
Theorem	tendo0mulr 36696*	Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.)
|- 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 ) /\ U e. E ) -> ( U o. O ) = O )
Theorem	tendo1ne0 36697*	The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-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 ) -> ( _I |` T ) =/= O )
Theorem	tendoconid 36698*	The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-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 ) /\ ( U e. E /\ U =/= O ) /\ ( V e. E /\ V =/= O ) ) -> ( U o. V ) =/= O )
Theorem	tendotr 36699*	The trace of the value of a non-zero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   &    |- E = ( ( TEndo ` K ) ` W )   &    |- O = ( f e. T |-> ( _I |` B ) )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( U e. E /\ U =/= O ) /\ F e. T ) -> ( R ` ( U ` F ) ) = ( R ` F ) )
Theorem	cdlemk1 36700	Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( 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 /\ N e. T ) /\ ( ( R ` F ) = ( R ` N ) /\ ( P e. A /\ -. P .<_ W ) ) ) -> ( P .\/ ( N ` P ) ) = ( ( F ` P ) .\/ ( R ` F ) ) )