P. 338 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33701-33800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lautcnv 33701	The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013.)
|- I = ( LAut ` K )   =>    |- ( ( K e. V /\ F e. I ) -> `' F e. I )
Theorem	lautlt 33702	Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X .< Y <-> ( F ` X ) .< ( F ` Y ) ) )
Theorem	lautcvr 33703	Covering property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- C = ( <o ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( K e. A /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )
Theorem	lautj 33704	Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )
Theorem	lautm 33705	Meet property of a lattice automorphism. (Contributed by NM, 19-May-2012.)
|- B = ( Base ` K )   &    |- ./\ = ( meet ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( K e. Lat /\ ( F e. I /\ X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) = ( ( F ` X ) ./\ ( F ` Y ) ) )
Theorem	lauteq 33706*	A lattice automorphism argument is equal to its value if all atoms are equal to their values. (Contributed by NM, 24-May-2012.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( ( K e. HL /\ F e. I /\ X e. B ) /\ A. p e. A ( F ` p ) = p ) -> ( F ` X ) = X )
Theorem	idlaut 33707	The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012.)
|- B = ( Base ` K )   &    |- I = ( LAut ` K )   =>    |- ( K e. A -> ( _I |` B ) e. I )
Theorem	lautco 33708	The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
|- I = ( LAut ` K )   =>    |- ( ( K e. V /\ F e. I /\ G e. I ) -> ( F o. G ) e. I )
Theorem	pautsetN 33709*	The set of projective automorphisms. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- M = ( PAut ` K )   =>    |- ( K e. B -> M = { f | ( f : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )
Theorem	ispautN 33710*	The predictate "is a projective automorphism." (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- M = ( PAut ` K )   =>    |- ( K e. B -> ( F e. M <-> ( F : S -1-1-onto-> S /\ A. x e. S A. y e. S ( x C_ y <-> ( F ` x ) C_ ( F ` y ) ) ) ) )
Syntax	cldil 33711	Extend class notation with set of all lattice dilations.
class LDil
Syntax	cltrn 33712	Extend class notation with set of all lattice translations.
class LTrn
Syntax	cdilN 33713	Extend class notation with set of all dilations.
class Dil
Syntax	ctrnN 33714	Extend class notation with set of all translations.
class Trn
Definition	df-ldil 33715*	Define set of all lattice dilations. Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
|- LDil = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( LAut ` k ) | A. x e. ( Base ` k ) ( x ( le ` k ) w -> ( f ` x ) = x ) } ) )
Definition	df-ltrn 33716*	Define set of all lattice translations. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
|- LTrn = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> { f e. ( ( LDil ` k ) ` w ) | A. p e. ( Atoms ` k ) A. q e. ( Atoms ` k ) ( ( -. p ( le ` k ) w /\ -. q ( le ` k ) w ) -> ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) = ( ( q ( join ` k ) ( f ` q ) ) ( meet ` k ) w ) ) } ) )
Definition	df-dilN 33717*	Define set of all dilations. Definition of dilation in [Crawley] p. 111. (Contributed by NM, 30-Jan-2012.)
|- Dil = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( PAut ` k ) | A. x e. ( PSubSp ` k ) ( x C_ ( ( WAtoms ` k ) ` d ) -> ( f ` x ) = x ) } ) )
Definition	df-trnN 33718*	Define set of all translations. Definition of translation in [Crawley] p. 111. (Contributed by NM, 4-Feb-2012.)
|- Trn = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> { f e. ( ( Dil ` k ) ` d ) | A. q e. ( ( WAtoms ` k ) ` d ) A. r e. ( ( WAtoms ` k ) ` d ) ( ( q ( +P ` k ) ( f ` q ) ) i^i ( ( _|_P ` k ) ` { d } ) ) = ( ( r ( +P ` k ) ( f ` r ) ) i^i ( ( _|_P ` k ) ` { d } ) ) } ) )
Theorem	ldilfset 33719*	The mapping from fiducial co-atom w to its set of lattice dilations. (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( LAut ` K )   =>    |- ( K e. C -> ( LDil ` K ) = ( w e. H |-> { f e. I | A. x e. B ( x .<_ w -> ( f ` x ) = x ) } ) )
Theorem	ldilset 33720*	The set of lattice dilations for a fiducial co-atom W. (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( LAut ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( K e. C /\ W e. H ) -> D = { f e. I | A. x e. B ( x .<_ W -> ( f ` x ) = x ) } )
Theorem	isldil 33721*	The predicate "is a lattice dilation". Similar to definition of dilation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- I = ( LAut ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( K e. C /\ W e. H ) -> ( F e. D <-> ( F e. I /\ A. x e. B ( x .<_ W -> ( F ` x ) = x ) ) ) )
Theorem	ldillaut 33722	A lattice dilation is an automorphism. (Contributed by NM, 20-May-2012.)
|- H = ( LHyp ` K )   &    |- I = ( LAut ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F e. I )
Theorem	ldil1o 33723	A lattice dilation is a one-to-one onto function. (Contributed by NM, 19-Apr-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. D ) -> F : B -1-1-onto-> B )
Theorem	ldilval 33724	Value of a lattice dilation under its co-atom. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. D /\ ( X e. B /\ X .<_ W ) ) -> ( F ` X ) = X )
Theorem	idldil 33725	The identity function is a lattice dilation. (Contributed by NM, 18-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( K e. A /\ W e. H ) -> ( _I |` B ) e. D )
Theorem	ldilcnv 33726	The converse of a lattice dilation is a lattice dilation. (Contributed by NM, 10-May-2013.)
|- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. D ) -> `' F e. D )
Theorem	ldilco 33727	The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.)
|- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. D /\ G e. D ) -> ( F o. G ) e. D )
Theorem	ltrnfset 33728*	The set of all lattice translations for a lattice K. (Contributed by NM, 11-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. C -> ( LTrn ` K ) = ( w e. H |-> { f e. ( ( LDil ` K ) ` w ) | A. p e. A A. q e. A ( ( -. p .<_ w /\ -. q .<_ w ) -> ( ( p .\/ ( f ` p ) ) ./\ w ) = ( ( q .\/ ( f ` q ) ) ./\ w ) ) } ) )
Theorem	ltrnset 33729*	The set of lattice translations for a fiducial co-atom W. (Contributed by NM, 11-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( K e. B /\ W e. H ) -> T = { f e. D | A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( f ` p ) ) ./\ W ) = ( ( q .\/ ( f ` q ) ) ./\ W ) ) } )
Theorem	isltrn 33730*	The predicate "is a lattice translation". Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 11-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( K e. B /\ W e. H ) -> ( F e. T <-> ( F e. D /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) ) )
Theorem	isltrn2N 33731*	The predicate "is a lattice translation". Version of isltrn 33730 that considers only different p and q. TODO: Can this eliminate some separate proofs for the p = q case? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( K e. B /\ W e. H ) -> ( F e. T <-> ( F e. D /\ A. p e. A A. q e. A ( ( -. p .<_ W /\ -. q .<_ W /\ p =/= q ) -> ( ( p .\/ ( F ` p ) ) ./\ W ) = ( ( q .\/ ( F ` q ) ) ./\ W ) ) ) ) )
Theorem	ltrnu 33732	Uniqueness property of a lattice translation value for atoms not under the fiducial co-atom W. Similar to definition of translation in [Crawley] p. 111. (Contributed by NM, 20-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( ( K e. V /\ W e. H ) /\ F e. T ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) -> ( ( P .\/ ( F ` P ) ) ./\ W ) = ( ( Q .\/ ( F ` Q ) ) ./\ W ) )
Theorem	ltrnldil 33733	A lattice translation is a lattice dilation. (Contributed by NM, 20-May-2012.)
|- H = ( LHyp ` K )   &    |- D = ( ( LDil ` K ) ` W )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. D )
Theorem	ltrnlaut 33734	A lattice translation is a lattice automorphism. (Contributed by NM, 20-May-2012.)
|- H = ( LHyp ` K )   &    |- I = ( LAut ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F e. I )
Theorem	ltrn1o 33735	A lattice translation is a one-to-one onto function. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> F : B -1-1-onto-> B )
Theorem	ltrncl 33736	Closure of a lattice translation. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ X e. B ) -> ( F ` X ) e. B )
Theorem	ltrn11 33737	One-to-one property of a lattice translation. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( ( F ` X ) = ( F ` Y ) <-> X = Y ) )
Theorem	ltrncnvnid 33738	If a translation is different from the identity, so is its converse. (Contributed by NM, 17-Jun-2013.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> `' F =/= ( _I |` B ) )
Theorem	ltrncoidN 33739	Two translations are equal if the composition of one with the converse of the other is the zero translation. This is an analogue of vector subtraction. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( ( F o. `' G ) = ( _I |` B ) <-> F = G ) )
Theorem	ltrnle 33740	Less-than or equal property of a lattice translation. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( F ` X ) .<_ ( F ` Y ) ) )
Theorem	ltrncnvleN 33741	Less-than or equal property of lattice translation converse. (Contributed by NM, 10-May-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( `' F ` X ) .<_ ( `' F ` Y ) ) )
Theorem	ltrnm 33742	Lattice translation of a meet. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- ./\ = ( meet ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( F ` ( X ./\ Y ) ) = ( ( F ` X ) ./\ ( F ` Y ) ) )
Theorem	ltrnj 33743	Lattice translation of a meet. TODO: change antecedent to K e. HL (Contributed by NM, 25-May-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( F ` ( X .\/ Y ) ) = ( ( F ` X ) .\/ ( F ` Y ) ) )
Theorem	ltrncvr 33744	Covering property of a lattice translation. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ Y e. B ) ) -> ( X C Y <-> ( F ` X ) C ( F ` Y ) ) )
Theorem	ltrnval1 33745	Value of a lattice translation under its co-atom. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T /\ ( X e. B /\ X .<_ W ) ) -> ( F ` X ) = X )
Theorem	ltrnid 33746*	A lattice translation is the identity function iff all atoms not under the fiducial co-atom W are equal to their values. (Contributed by NM, 24-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( A. p e. A ( -. p .<_ W -> ( F ` p ) = p ) <-> F = ( _I |` B ) ) )
Theorem	ltrnnid 33747*	If a lattice translation is not the identity, then there is an atom not under the fiducial co-atom W and not equal to its translation. (Contributed by NM, 24-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> E. p e. A ( -. p .<_ W /\ ( F ` p ) =/= p ) )
Theorem	ltrnatb 33748	The lattice translation of an atom is an atom. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( F ` P ) e. A ) )
Theorem	ltrncnvatb 33749	The converse of the lattice translation of an atom is an atom. (Contributed by NM, 2-Jun-2012.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. B ) -> ( P e. A <-> ( `' F ` P ) e. A ) )
Theorem	ltrnel 33750	The lattice translation of an atom not under the fiducial co-atom is also an atom not under the fiducial co-atom. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 22-May-2012.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) e. A /\ -. ( F ` P ) .<_ W ) )
Theorem	ltrnat 33751	The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 33750 uses. (Contributed by NM, 25-May-2012.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. A ) -> ( F ` P ) e. A )
Theorem	ltrncnvat 33752	The converse of the lattice translation of an atom is an atom. (Contributed by NM, 9-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ P e. A ) -> ( `' F ` P ) e. A )
Theorem	ltrncnvel 33753	The converse of the lattice translation of an atom not under the fiducial co-atom. (Contributed by NM, 10-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( `' F ` P ) e. A /\ -. ( `' F ` P ) .<_ W ) )
Theorem	ltrncoelN 33754	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 33750 uses. (Contributed by NM, 1-May-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` ( G ` P ) ) e. A /\ -. ( F ` ( G ` P ) ) .<_ W ) )
Theorem	ltrncoat 33755	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 33750, ltrnat 33751 uses. (Contributed by NM, 1-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ P e. A ) -> ( F ` ( G ` P ) ) e. A )
Theorem	ltrncoval 33756	Two ways to express value of translation composition. (Contributed by NM, 31-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ G e. T ) /\ P e. A ) -> ( ( F o. G ) ` P ) = ( F ` ( G ` P ) ) )
Theorem	ltrncnv 33757	The converse of a lattice translation is a lattice translation. (Contributed by NM, 10-May-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> `' F e. T )
Theorem	ltrn11at 33758	Frequently used one-to-one property of lattice translation atoms. (Contributed by NM, 5-May-2013.)
|- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ Q e. A /\ P =/= Q ) ) -> ( F ` P ) =/= ( F ` Q ) )
Theorem	ltrneq2 33759*	The equality of two translations is determined by their equality at atoms. (Contributed by NM, 2-Mar-2014.)
|- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( A. p e. A ( F ` p ) = ( G ` p ) <-> F = G ) )
Theorem	ltrneq 33760*	The equality of two translations is determined by their equality at atoms not under co-atom W. (Contributed by NM, 20-Jun-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ G e. T ) -> ( A. p e. A ( -. p .<_ W -> ( F ` p ) = ( G ` p ) ) <-> F = G ) )
Theorem	idltrn 33761	The identity function is a lattice translation. Remark below Lemma B in [Crawley] p. 112. (Contributed by NM, 18-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> ( _I |` B ) e. T )
Theorem	ltrnmw 33762	Property of lattice translation value. Remark below Lemma B in [Crawley] p. 112. TODO: Can this be used in more places? (Contributed by NM, 20-May-2012.) (Proof shortened by OpenAI, 25-Mar-2020.)
|- .<_ = ( le ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) ./\ W ) = .0. )
Theorem	ltrnmwOLD 33763	Property of lattice translation value. Remark below Lemma B in [Crawley] p. 112. TODO: Can this be used in more places? (Contributed by NM, 20-May-2012.) Obsolete version of ltrnmw 33762 as of 25-Mar-2020. (New usage is discouraged.) (Proof modification is discouraged.)
|- .<_ = ( le ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) ./\ W ) = .0. )
Theorem	dilfsetN 33764*	The mapping from fiducial atom to set of dilations. (Contributed by NM, 30-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- W = ( WAtoms ` K )   &    |- M = ( PAut ` K )   &    |- L = ( Dil ` K )   =>    |- ( K e. B -> L = ( d e. A |-> { f e. M | A. x e. S ( x C_ ( W ` d ) -> ( f ` x ) = x ) } ) )
Theorem	dilsetN 33765*	The set of dilations for a fiducial atom D. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- W = ( WAtoms ` K )   &    |- M = ( PAut ` K )   &    |- L = ( Dil ` K )   =>    |- ( ( K e. B /\ D e. A ) -> ( L ` D ) = { f e. M | A. x e. S ( x C_ ( W ` D ) -> ( f ` x ) = x ) } )
Theorem	isdilN 33766*	The predicate "is a dilation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- W = ( WAtoms ` K )   &    |- M = ( PAut ` K )   &    |- L = ( Dil ` K )   =>    |- ( ( K e. B /\ D e. A ) -> ( F e. ( L ` D ) <-> ( F e. M /\ A. x e. S ( x C_ ( W ` D ) -> ( F ` x ) = x ) ) ) )
Theorem	trnfsetN 33767*	The mapping from fiducial atom to set of translations. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- W = ( WAtoms ` K )   &    |- M = ( PAut ` K )   &    |- L = ( Dil ` K )   &    |- T = ( Trn ` K )   =>    |- ( K e. C -> T = ( d e. A |-> { f e. ( L ` d ) | A. q e. ( W ` d ) A. r e. ( W ` d ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { d } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { d } ) ) } ) )
Theorem	trnsetN 33768*	The set of translations for a fiducial atom D. (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- W = ( WAtoms ` K )   &    |- M = ( PAut ` K )   &    |- L = ( Dil ` K )   &    |- T = ( Trn ` K )   =>    |- ( ( K e. B /\ D e. A ) -> ( T ` D ) = { f e. ( L ` D ) | A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( f ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( f ` r ) ) i^i ( ._|_ ` { D } ) ) } )
Theorem	istrnN 33769*	The predicate "is a translation". (Contributed by NM, 4-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- W = ( WAtoms ` K )   &    |- M = ( PAut ` K )   &    |- L = ( Dil ` K )   &    |- T = ( Trn ` K )   =>    |- ( ( K e. B /\ D e. A ) -> ( F e. ( T ` D ) <-> ( F e. ( L ` D ) /\ A. q e. ( W ` D ) A. r e. ( W ` D ) ( ( q .+ ( F ` q ) ) i^i ( ._|_ ` { D } ) ) = ( ( r .+ ( F ` r ) ) i^i ( ._|_ ` { D } ) ) ) ) )
Syntax	ctrl 33770	Extend class notation with set of all traces of lattice translations.
class trL
Definition	df-trl 33771*	Define trace of a lattice translation. (Contributed by NM, 20-May-2012.)
|- trL = ( k e. _V |-> ( w e. ( LHyp ` k ) |-> ( f e. ( ( LTrn ` k ) ` w ) |-> ( iota_ x e. ( Base ` k ) A. p e. ( Atoms ` k ) ( -. p ( le ` k ) w -> x = ( ( p ( join ` k ) ( f ` p ) ) ( meet ` k ) w ) ) ) ) ) )
Theorem	trlfset 33772*	The set of all traces of lattice translations for a lattice K. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. C -> ( trL ` K ) = ( w e. H |-> ( f e. ( ( LTrn ` K ) ` w ) |-> ( iota_ x e. B A. p e. A ( -. p .<_ w -> x = ( ( p .\/ ( f ` p ) ) ./\ w ) ) ) ) ) )
Theorem	trlset 33773*	The set of traces of lattice translations for a fiducial co-atom W. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( K e. C /\ W e. H ) -> R = ( f e. T |-> ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( f ` p ) ) ./\ W ) ) ) ) )
Theorem	trlval 33774*	The value of the trace of a lattice translation. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. V /\ W e. H ) /\ F e. T ) -> ( R ` F ) = ( iota_ x e. B A. p e. A ( -. p .<_ W -> x = ( ( p .\/ ( F ` p ) ) ./\ W ) ) ) )
Theorem	trlval2 33775	The value of the trace of a lattice translation, given any atom P not under the fiducial co-atom W. Note: this requires only the weaker assumption K e. Lat; we use K e. HL for convenience. (Contributed by NM, 20-May-2012.)
|- .<_ = ( 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 ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ W ) )
Theorem	trlcl 33776	Closure of the trace of a lattice translation. (Contributed by NM, 22-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) e. B )
Theorem	trlcnv 33777	The trace of the converse of a lattice translation. (Contributed by NM, 10-May-2013.)
|- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` `' F ) = ( R ` F ) )
Theorem	trljat1 33778	The value of a translation of an atom P not under the fiducial co-atom W, joined with trace. Equation above Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 33475? (Contributed by NM, 22-May-2012.)
|- .<_ = ( 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 /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` F ) ) = ( P .\/ ( F ` P ) ) )
Theorem	trljat2 33779	The value of a translation of an atom P not under the fiducial co-atom W, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
|- .<_ = ( 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 /\ ( P e. A /\ -. P .<_ W ) ) -> ( ( F ` P ) .\/ ( R ` F ) ) = ( P .\/ ( F ` P ) ) )
Theorem	trljat3 33780	The value of a translation of an atom P not under the fiducial co-atom W, joined with trace. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 22-May-2012.)
|- .<_ = ( 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 /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( R ` F ) ) = ( ( F ` P ) .\/ ( R ` F ) ) )
Theorem	trlat 33781	If an atom differs from its translation, the trace is an atom. Equation above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.)
|- .<_ = ( le ` 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 ) /\ ( F e. T /\ ( F ` P ) =/= P ) ) -> ( R ` F ) e. A )
Theorem	trl0 33782	If an atom not under the fiducial co-atom W equals its lattice translation, the trace of the translation is zero. (Contributed by NM, 24-May-2012.)
|- .<_ = ( le ` K )   &    |- .0. = ( 0. ` 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 ) /\ ( F e. T /\ ( F ` P ) = P ) ) -> ( R ` F ) = .0. )
Theorem	trlator0 33783	The trace of a lattice translation is an atom or zero. (Contributed by NM, 5-May-2013.)
|- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A \/ ( R ` F ) = .0. ) )
Theorem	trlatn0 33784	The trace of a lattice translation is an atom iff it is nonzero. (Contributed by NM, 14-Jun-2013.)
|- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( ( R ` F ) e. A <-> ( R ` F ) =/= .0. ) )
Theorem	trlnidat 33785	The trace of a lattice translation other than the identity is an atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 23-May-2012.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ F =/= ( _I |` B ) ) -> ( R ` F ) e. A )
Theorem	ltrnnidn 33786	If a lattice translation is not the identity, then the translation of any atom not under the fiducial co-atom W is different from the atom. Remark above Lemma C in [Crawley] p. 112. (Contributed by NM, 24-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ F =/= ( _I |` B ) ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( F ` P ) =/= P )
Theorem	ltrnideq 33787	Property of the identity lattice translation. (Contributed by NM, 27-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> ( F = ( _I |` B ) <-> ( F ` P ) = P ) )
Theorem	trlid0 33788	The trace of the identity translation is zero. (Contributed by NM, 11-Jun-2013.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> ( R ` ( _I |` B ) ) = .0. )
Theorem	trlnidatb 33789	A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 33785? Why do both this and ltrnideq 33787 need trlnidat 33785? (Contributed by NM, 4-Jun-2013.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F =/= ( _I |` B ) <-> ( R ` F ) e. A ) )
Theorem	trlid0b 33790	A lattice translation is the identity iff its trace is zero. (Contributed by NM, 14-Jun-2013.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( F = ( _I |` B ) <-> ( R ` F ) = .0. ) )
Theorem	trlnid 33791	Different translations with the same trace cannot be the identity. (Contributed by NM, 26-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 ) /\ ( F =/= G /\ ( R ` F ) = ( R ` G ) ) ) -> F =/= ( _I |` B ) )
Theorem	ltrn2ateq 33792	Property of the equality of a lattice translation with its value. (Contributed by NM, 27-May-2012.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( ( F ` P ) = P <-> ( F ` Q ) = Q ) )
Theorem	ltrnateq 33793	If any atom (under W) is not equal to its translation, so is any other atom. (Contributed by NM, 6-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F ` P ) = P ) -> ( F ` Q ) = Q )
Theorem	ltrnatneq 33794	If any atom (under W) is not equal to its translation, so is any other atom. TODO: -. P .<_ W isn't needed to prove this. Will removing it shorten (and not lengthen) proofs using it? (Contributed by NM, 6-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( F ` P ) =/= P ) -> ( F ` Q ) =/= Q )
Theorem	ltrnatlw 33795	If the value of an atom equals the atom in a non-identity translation, the atom is under the fiducial hyperplane. (Contributed by NM, 15-May-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( F ` P ) =/= P /\ ( F ` Q ) = Q ) ) -> Q .<_ W )
Theorem	trlle 33796	The trace of a lattice translation is less than the fiducial co-atom W. (Contributed by NM, 25-May-2012.)
|- .<_ = ( le ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T ) -> ( R ` F ) .<_ W )
Theorem	trlne 33797	The trace of a lattice translation is not equal to any atom not under the fiducial co-atom W. Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> P =/= ( R ` F ) )
Theorem	trlnle 33798	The atom not under the fiducial co-atom W is not less than the trace of a lattice translation. Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 26-May-2012.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- T = ( ( LTrn ` K ) ` W )   &    |- R = ( ( trL ` K ) ` W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ F e. T /\ ( P e. A /\ -. P .<_ W ) ) -> -. P .<_ ( R ` F ) )
Theorem	trlval3 33799	The value of the trace of a lattice translation in terms of 2 atoms. TODO: Try to shorten proof. (Contributed by NM, 3-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 ) /\ F e. T /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( P .\/ ( F ` P ) ) =/= ( Q .\/ ( F ` Q ) ) ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ ( Q .\/ ( F ` Q ) ) ) )
Theorem	trlval4 33800	The value of the trace of a lattice translation in terms of 2 atoms. (Contributed by NM, 3-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 ) /\ ( F e. T /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( P =/= Q /\ -. ( R ` F ) .<_ ( P .\/ Q ) ) ) -> ( R ` F ) = ( ( P .\/ ( F ` P ) ) ./\ ( Q .\/ ( F ` Q ) ) ) )