P. 342 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34101-34200   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lautm 34101	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 34102*	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 34103	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 34104	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 34105*	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 34106*	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 34107	Extend class notation with set of all lattice dilations.
class LDil
Syntax	cltrn 34108	Extend class notation with set of all lattice translations.
class LTrn
Syntax	cdilN 34109	Extend class notation with set of all dilations.
class Dil
Syntax	ctrnN 34110	Extend class notation with set of all translations.
class Trn
Definition	df-ldil 34111*	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 34112*	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 34113*	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 34114*	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 34115*	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 34116*	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 34117*	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 34118	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 34119	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 34120	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 34121	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 34122	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 34123	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 34124*	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 34125*	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 34126*	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 34127*	The predicate "is a lattice translation". Version of isltrn 34126 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 34128	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 34129	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 34130	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 34131	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 34132	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 34133	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 34134	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 34135	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 34136	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 34137	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 34138	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 34139	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 34140	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 34141	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 34142*	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 34143*	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 34144	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 34145	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 34146	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 34147	The lattice translation of an atom is also an atom. TODO: See if this can shorten some ltrnel 34146 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 34148	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 34149	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 34150	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 34146 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 34151	Composition of lattice translations of an atom. TODO: See if this can shorten some ltrnel 34146, ltrnat 34147 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 34152	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 34153	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 34154	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 34155*	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 34156*	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 34157	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 34158	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 34159*	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 34160*	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 34161*	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 34162*	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 34163*	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 34164*	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 34165	Extend class notation with set of all traces of lattice translations.
class trL
Definition	df-trl 34166*	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 34167*	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 34168*	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 34169*	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 34170	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 34171	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 34172	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 34173	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 33871? (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 34174	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 34175	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 34176	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 34177	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 34178	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 34179	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 34180	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 34181	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 34182	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 34183	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 34184	A lattice translation is not the identity iff its trace is an atom. TODO: Can proofs be reorganized so this goes with trlnidat 34180? Why do both this and ltrnideq 34182 need trlnidat 34180? (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 34185	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 34186	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 34187	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 34188	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 34189	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 34190	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 34191	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 34192	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 34193	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 34194	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 34195	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 ) ) ) )
Theorem	trlval5 34196	The value of the trace of a lattice translation in terms of itself. (Contributed by NM, 19-Jul-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 ) ) -> ( R ` F ) = ( ( P .\/ ( R ` F ) ) ./\ W ) )
Theorem	arglem1N 34197	Lemma for Desargues' law. Theorem 13.3 of [Crawley] p. 110, 3rd and 4th lines from bottom. In these lemmas, P, Q, R, S, T, U, C, D, E, F, and G represent Crawley's a0, a1, a2, b0, b1, b2, c, z0, z1, z2, and p respectively. (Contributed by NM, 28-Jun-2012.) (New usage is discouraged.)
|- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- F = ( ( P .\/ Q ) ./\ ( S .\/ T ) )   &    |- G = ( ( P .\/ S ) ./\ ( Q .\/ T ) )   =>    |- ( ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ ( S e. A /\ T e. A /\ P =/= Q ) /\ ( P =/= S /\ Q =/= T /\ S =/= T ) ) /\ G e. A ) -> F e. A )
Theorem	cdlemc1 34198	Part of proof of Lemma C in [Crawley] p. 112. TODO: shorten with atmod3i1 33871? (Contributed by NM, 29-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ X e. B /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ ( ( P .\/ X ) ./\ W ) ) = ( P .\/ X ) )
Theorem	cdlemc2 34199	Part of proof of Lemma C in [Crawley] p. 112. (Contributed by NM, 25-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` 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 ` Q ) .<_ ( ( F ` P ) .\/ ( ( P .\/ Q ) ./\ W ) ) )
Theorem	cdlemc3 34200	Part of proof of Lemma C in [Crawley] p. 113. (Contributed by NM, 26-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 ) /\ ( Q e. A /\ -. Q .<_ W ) ) ) -> ( ( F ` P ) .<_ ( Q .\/ ( R ` F ) ) -> Q .<_ ( P .\/ ( F ` P ) ) ) )