P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	trlcone 35401	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 35402	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 35403	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 35404	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 35405	Eliminate ( F ` P ) =/= P, ( G ` P ) =/= P from cdlemg44a 35404. (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 35406	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 35407	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 35408*	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 35409*	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 35410	Elmininate h from cdlemg47 35409. (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 35411	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 35412	Rearrange a composition of 4 translations, analogous to an4 821. (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 35413	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 35414	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 35415	Extend class notation with translation group.
class TGrp
Definition	df-tgrp 35416*	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 35417*	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 35418*	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 35419	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 35420*	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 35421	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 35422	Lemma for tgrpgrp 35423. (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 35423	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 35424	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 35425	Extend class notation with translation group endomorphisms.
class TEndo
Syntax	cedring 35426	Extend class notation with division ring on trace-preserving endomorphisms.
class EDRing
Syntax	cedring-rN 35427	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 35428*	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 35429*	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 35430*	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 35431*	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 35432*	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 35433*	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 35434	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 35435*	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 35436	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 35437*	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 35438	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 35439	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 35440	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 35441	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 35442	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 35443	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 35444	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 35445	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 35446	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 35447*	Condition determining equality of two trace-preserving endomorphisms, showing it is unnecessary to consider the identity translation. In tendocan 35497, 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 35448*	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 35449*	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 35450*	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 35451*	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 35452*	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 35453*	Trace-preserving property of endomorphism sum operation P, based on theorem trlco 35400. Part of remark in [Crawley] p. 118, 2nd line, "it is clear from the second part of G (our trlco 35400) 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 35454*	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 35455*	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 35456*	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 35457*	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 35458*	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 35459*	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 35460*	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 35461*	The additive identity trace-perserving endormorphism preserves composition of translations. TODO: why isn't this a special case of tendospdi1 35694? (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 35462*	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 35463*	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 35464*	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 35465*	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 35466*	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 35467*	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 35468*	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 35469*	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 35470*	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 35471*	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 35472*	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 35473*	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 35474	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 35475*	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 35476*	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 35477	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 35478*	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 35479	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 35480*	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 35481*	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 35482	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 35483*	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 35484*	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 35485	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 35486*	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 35487	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 35488	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 35489	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 35490	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 35491	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 35492	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 35493	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 35494	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 35495	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 35496	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 35497	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 35498*	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 35499*	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 35500*	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 )