P. 352 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35101-35200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lautcnvclN 35101	Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( ( K e. V /\ F e. I ) /\ X e. B ) -> ( `' F ` X ) e. B )
Theorem	lautcnvle 35102	Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( ( K e. V /\ F e. I ) /\ ( X e. B /\ Y e. B ) ) -> ( X .<_ Y <-> ( `' F ` X ) .<_ ( `' F ` Y ) ) )
Theorem	lautcnv 35103	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 35104	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 35105	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 35106	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 35107	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 35108*	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 35109	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 35110	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 35111*	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 35112*	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 35113	Extend class notation with set of all lattice dilations.
class LDil
Syntax	cltrn 35114	Extend class notation with set of all lattice translations.
class LTrn
Syntax	cdilN 35115	Extend class notation with set of all dilations.
class Dil
Syntax	ctrnN 35116	Extend class notation with set of all translations.
class Trn
Definition	df-ldil 35117*	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 35118*	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 35119*	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 35120*	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 35121*	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 35122*	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 35123*	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 35124	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 35125	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 35126	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 35127	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 35128	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 35129	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 35130*	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 35131*	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 35132*	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 35133*	The predicate "is a lattice translation". Version of isltrn 35132 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 35134	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 35135	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 35136	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 35137	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 35138	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 35139	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 35140	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 35141	Two translations are equal if the composition of one with the converse of the other is the zero translation. This is an analog 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 35142	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 35143	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 35144	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 35145	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 35146	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 35147	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 35148*	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 35149*	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 35150	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 35151	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 35152	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 35153	The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 35152 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 35154	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 35155	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 35156	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 35152 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 35157	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 35152, ltrnat 35153 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 35158	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 35159	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 35160	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 35161*	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 35162*	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 35163	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 35164	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.)
|- .<_ = ( 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 35165*	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 35166*	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 35167*	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 35168*	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 35169*	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 35170*	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 35171	Extend class notation with set of all traces of lattice translations.
class trL
Definition	df-trl 35172*	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 35173*	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 35174*	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 35175*	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 35176	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 35177	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 35178	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 35179	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 34877? (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 35180	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 35181	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 35182	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 35183	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 35184	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 35185	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 35186	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 35187	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 35188	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 35189	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 35190	A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 35186? Why do both this and ltrnideq 35188 need trlnidat 35186? (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 35191	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 35192	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 35193	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 35194	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 35195	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 35196	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 35197	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 35198	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 35199	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 35200	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 ) ) ) )