P. 349 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34801-34900   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cpautN 34801	Extend class notation with set of all projective automorphisms.
class PAut
Definition	df-lhyp 34802*	Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e. all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.)
|- LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) } )
Definition	df-laut 34803*	Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.)
|- LAut = ( k e. _V |-> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } )
Definition	df-watsN 34804*	Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" d. These are all atoms not in the polarity of { d } ), which is the hyperplane determined by d. Definition of set W in [Crawley] p. 111. (Contributed by NM, 26-Jan-2012.)
|- WAtoms = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) )
Definition	df-pautN 34805*	Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.)
|- PAut = ( k e. _V |-> { f | ( f : ( PSubSp ` k ) -1-1-onto-> ( PSubSp ` k ) /\ A. x e. ( PSubSp ` k ) A. y e. ( PSubSp ` k ) ( x C_ y <-> ( f ` x ) C_ ( f ` y ) ) ) } )
Theorem	watfvalN 34806*	The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- P = ( _|_P ` K )   &    |- W = ( WAtoms ` K )   =>    |- ( K e. B -> W = ( d e. A |-> ( A \ ( ( _|_P ` K ) ` { d } ) ) ) )
Theorem	watvalN 34807	Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- P = ( _|_P ` K )   &    |- W = ( WAtoms ` K )   =>    |- ( ( K e. B /\ D e. A ) -> ( W ` D ) = ( A \ ( ( _|_P ` K ) ` { D } ) ) )
Theorem	iswatN 34808	The predicate "is a W atom" (corresponding to fiducial atom D). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- P = ( _|_P ` K )   &    |- W = ( WAtoms ` K )   =>    |- ( ( K e. B /\ D e. A ) -> ( P e. ( W ` D ) <-> ( P e. A /\ -. P e. ( ( _|_P ` K ) ` { D } ) ) ) )
Theorem	lhpset 34809*	The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .1. = ( 1. ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. A -> H = { w e. B | w C .1. } )
Theorem	islhp 34810	The predicate "is a co-atom (lattice hyperplane)." (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .1. = ( 1. ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   =>    |- ( K e. A -> ( W e. H <-> ( W e. B /\ W C .1. ) ) )
Theorem	islhp2 34811	The predicate "is a co-atom (lattice hyperplane)." (Contributed by NM, 18-May-2012.)
|- B = ( Base ` K )   &    |- .1. = ( 1. ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. A /\ W e. B ) -> ( W e. H <-> W C .1. ) )
Theorem	lhpbase 34812	A co-atom is a member of the lattice base set (i.e. a lattice element). (Contributed by NM, 18-May-2012.)
|- B = ( Base ` K )   &    |- H = ( LHyp ` K )   =>    |- ( W e. H -> W e. B )
Theorem	lhp1cvr 34813	The lattice unit covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012.)
|- .1. = ( 1. ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. A /\ W e. H ) -> W C .1. )
Theorem	lhplt 34814	An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
|- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) ) -> P .< W )
Theorem	lhp2lt 34815	The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.)
|- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ P .<_ W ) /\ ( Q e. A /\ Q .<_ W ) ) -> ( P .\/ Q ) .< W )
Theorem	lhpexlt 34816*	There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
|- .< = ( lt ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A p .< W )
Theorem	lhp0lt 34817	A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
|- .< = ( lt ` K )   &    |- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> .0. .< W )
Theorem	lhpn0 34818	A co-atom is nonzero. TODO: is this needed? (Contributed by NM, 26-Apr-2013.)
|- .0. = ( 0. ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> W =/= .0. )
Theorem	lhpexle 34819*	There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A p .<_ W )
Theorem	lhpexnle 34820*	There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A -. p .<_ W )
Theorem	lhpexle1lem 34821*	Lemma for lhpexle1 34822 and others that eliminates restrictions on X. (Contributed by NM, 24-Jul-2013.)
|- ( ph -> E. p e. A ( p .<_ W /\ ps ) )   &    |- ( ( ph /\ ( X e. A /\ X .<_ W ) ) -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )   =>    |- ( ph -> E. p e. A ( p .<_ W /\ ps /\ p =/= X ) )
Theorem	lhpexle1 34822*	There exists an atom under a co-atom different from any given element. (Contributed by NM, 24-Jul-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X ) )
Theorem	lhpexle2lem 34823*	Lemma for lhpexle2 34824. (Contributed by NM, 19-Jun-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ X .<_ W ) /\ ( Y e. A /\ Y .<_ W ) ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
Theorem	lhpexle2 34824*	There exists atom under a co-atom different from any two other elements. (Contributed by NM, 24-Jul-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ p =/= X /\ p =/= Y ) )
Theorem	lhpexle3lem 34825*	There exists atom under a co-atom different from any 3 other atoms. TODO: study if adant*,simp* usage can be improved. (Contributed by NM, 9-Jul-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. A /\ Y e. A /\ Z e. A ) /\ ( X .<_ W /\ Y .<_ W /\ Z .<_ W ) ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
Theorem	lhpexle3 34826*	There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A ( p .<_ W /\ ( p =/= X /\ p =/= Y /\ p =/= Z ) ) )
Theorem	lhpex2leN 34827*	There exist at least two different atoms under a co-atom. This allows us to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> E. p e. A E. q e. A ( p .<_ W /\ q .<_ W /\ p =/= q ) )
Theorem	lhpoc 34828	The orthocomplement of a co-atom (lattice hyperplane) is an atom. (Contributed by NM, 18-May-2012.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. B ) -> ( W e. H <-> ( ._|_ ` W ) e. A ) )
Theorem	lhpoc2N 34829	The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. B ) -> ( W e. A <-> ( ._|_ ` W ) e. H ) )
Theorem	lhpocnle 34830	The orthocomplement of a co-atom is not under it. (Contributed by NM, 22-May-2012.)
|- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> -. ( ._|_ ` W ) .<_ W )
Theorem	lhpocat 34831	The orthocomplement of a co-atom is an atom. (Contributed by NM, 9-Feb-2013.)
|- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> ( ._|_ ` W ) e. A )
Theorem	lhpocnel 34832	The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 25-May-2012.)
|- .<_ = ( le ` K )   &    |- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( K e. HL /\ W e. H ) -> ( ( ._|_ ` W ) e. A /\ -. ( ._|_ ` W ) .<_ W ) )
Theorem	lhpocnel2 34833	The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- P = ( ( oc ` K ) ` W )   =>    |- ( ( K e. HL /\ W e. H ) -> ( P e. A /\ -. P .<_ W ) )
Theorem	lhpjat1 34834	The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 18-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- .1. = ( 1. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( W .\/ P ) = .1. )
Theorem	lhpjat2 34835	The join of a co-atom (hyperplane) and an atom not under it is the lattice unit. (Contributed by NM, 4-Jun-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- .1. = ( 1. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .\/ W ) = .1. )
Theorem	lhpj1 34836	The join of a co-atom (hyperplane) and an element not under it is the lattice unit. (Contributed by NM, 7-Dec-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- .1. = ( 1. ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( W .\/ X ) = .1. )
Theorem	lhpmcvr 34837	The meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 7-Dec-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ./\ = ( meet ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> ( X ./\ W ) C X )
Theorem	lhpmcvr2 34838*	Alternate way to express that the meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 9-Apr-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) ) -> E. p e. A ( -. p .<_ W /\ ( p .\/ ( X ./\ W ) ) = X ) )
Theorem	lhpmcvr3 34839	Specialization of lhpmcvr2 34838. TODO: Use this to simplify many uses of ( P .\/ ( X ./\ W ) ) = X to become P .<_ X. (Contributed by NM, 6-Apr-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P .<_ X <-> ( P .\/ ( X ./\ W ) ) = X ) )
Theorem	lhpmcvr4N 34840	Specialization of lhpmcvr2 34838. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( X e. B /\ -. X .<_ W ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W /\ P .<_ X ) ) -> -. P .<_ Y )
Theorem	lhpmcvr5N 34841*	Specialization of lhpmcvr2 34838. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W ) ) -> E. p e. A ( -. p .<_ W /\ -. p .<_ Y /\ ( p .\/ ( X ./\ W ) ) = X ) )
Theorem	lhpmcvr6N 34842*	Specialization of lhpmcvr2 34838. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ -. X .<_ W ) /\ ( Y e. B /\ ( X ./\ Y ) .<_ W ) ) -> E. p e. A ( -. p .<_ W /\ -. p .<_ Y /\ p .<_ X ) )
Theorem	lhpm0atN 34843	If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ X =/= .0. /\ ( X ./\ W ) = .0. ) ) -> X e. A )
Theorem	lhpmat 34844	An element covered by the lattice unit, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012.)
|- .<_ = ( le ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) -> ( P ./\ W ) = .0. )
Theorem	lhpmatb 34845	An element covered by the lattice unit, when conjoined with an atom, equals zero iff the atom is not under it. (Contributed by NM, 15-Jun-2013.)
|- .<_ = ( le ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ P e. A ) -> ( -. P .<_ W <-> ( P ./\ W ) = .0. ) )
Theorem	lhp2at0 34846	Join and meet with different atoms under co-atom W. (Contributed by NM, 15-Jun-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( U e. A /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> ( ( P .\/ U ) ./\ V ) = .0. )
Theorem	lhp2atnle 34847	Inequality for 2 different atoms under co-atom W. (Contributed by NM, 17-Jun-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( U e. A /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V .<_ ( P .\/ U ) )
Theorem	lhp2atne 34848	Inequality for joins with 2 different atoms under co-atom W. (Contributed by NM, 22-Jul-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( U e. A /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U =/= V ) -> ( P .\/ U ) =/= ( Q .\/ V ) )
Theorem	lhp2at0nle 34849	Inequality for 2 different atoms (or an atom and zero) under co-atom W. (Contributed by NM, 28-Jul-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ U =/= V ) /\ ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) -> -. V .<_ ( P .\/ U ) )
Theorem	lhp2at0ne 34850	Inequality for joins with 2 different atoms (or an atom and zero) under co-atom W. (Contributed by NM, 28-Jul-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ Q e. A ) /\ ( ( ( U e. A \/ U = .0. ) /\ U .<_ W ) /\ ( V e. A /\ V .<_ W ) ) /\ U =/= V ) -> ( P .\/ U ) =/= ( Q .\/ V ) )
Theorem	lhpelim 34851	Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat 34844 to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ X e. B ) -> ( ( P .\/ ( X ./\ W ) ) ./\ W ) = ( X ./\ W ) )
Theorem	lhpmod2i2 34852	Modular law for hyperplanes analogous to atmod2i2 34676 for atoms. (Contributed by NM, 9-Feb-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) /\ Y .<_ X ) -> ( ( X ./\ W ) .\/ Y ) = ( X ./\ ( W .\/ Y ) ) )
Theorem	lhpmod6i1 34853	Modular law for hyperplanes analogous to complement of atmod2i1 34675 for atoms. (Contributed by NM, 1-Jun-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( X e. B /\ Y e. B ) /\ X .<_ W ) -> ( X .\/ ( Y ./\ W ) ) = ( ( X .\/ Y ) ./\ W ) )
Theorem	lhprelat3N 34854*	The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 34226. (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- ./\ = ( meet ` K )   &    |- C = ( <o ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .< Y ) -> E. w e. H ( X .<_ ( Y ./\ w ) /\ ( Y ./\ w ) C Y ) )
Theorem	cdlemb2 34855*	Given two atoms not under the fiducial (reference) co-atom W, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 30-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ P =/= Q ) -> E. r e. A ( -. r .<_ W /\ -. r .<_ ( P .\/ Q ) ) )
Theorem	lhple 34856	Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( X e. B /\ X .<_ W ) ) -> ( ( P .\/ X ) ./\ W ) = X )
Theorem	lhpat 34857	Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 23-May-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> ( ( P .\/ Q ) ./\ W ) e. A )
Theorem	lhpat4N 34858	Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( U e. A /\ U .<_ W ) ) -> ( ( P .\/ U ) ./\ W ) = U )
Theorem	lhpat2 34859	Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 21-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- R = ( ( P .\/ Q ) ./\ W )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ P =/= Q ) ) -> R e. A )
Theorem	lhpat3 34860	There is only one atom under both P .\/ Q and co-atom W. (Contributed by NM, 21-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- R = ( ( P .\/ Q ) ./\ W )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) ) /\ ( Q e. A /\ S e. A ) /\ ( P =/= Q /\ S .<_ ( P .\/ Q ) ) ) -> ( -. S .<_ W <-> S =/= R ) )
Theorem	4atexlemk 34861	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> K e. HL )
Theorem	4atexlemw 34862	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> W e. H )
Theorem	4atexlempw 34863	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> ( P e. A /\ -. P .<_ W ) )
Theorem	4atexlemp 34864	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> P e. A )
Theorem	4atexlemq 34865	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> Q e. A )
Theorem	4atexlems 34866	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> S e. A )
Theorem	4atexlemt 34867	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> T e. A )
Theorem	4atexlemutvt 34868	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> ( U .\/ T ) = ( V .\/ T ) )
Theorem	4atexlempnq 34869	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> P =/= Q )
Theorem	4atexlemnslpq 34870	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> -. S .<_ ( P .\/ Q ) )
Theorem	4atexlemkl 34871	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> K e. Lat )
Theorem	4atexlemkc 34872	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   =>    |- ( ph -> K e. CvLat )
Theorem	4atexlemwb 34873	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- H = ( LHyp ` K )   =>    |- ( ph -> W e. ( Base ` K ) )
Theorem	4atexlempsb 34874	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ph -> ( P .\/ S ) e. ( Base ` K ) )
Theorem	4atexlemqtb 34875	Lemma for 4atexlem7 34889. (Contributed by NM, 24-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ph -> ( Q .\/ T ) e. ( Base ` K ) )
Theorem	4atexlempns 34876	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ph -> P =/= S )
Theorem	4atexlemswapqr 34877	Lemma for 4atexlem7 34889. Swap Q and R, so that theorems involving C can be reused for D. Note that U must be expanded because it involves Q. (Contributed by NM, 25-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   =>    |- ( ph -> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( R e. A /\ -. R .<_ W ) ) /\ ( S e. A /\ ( Q e. A /\ -. Q .<_ W /\ ( P .\/ Q ) = ( R .\/ Q ) ) /\ ( T e. A /\ ( ( ( P .\/ R ) ./\ W ) .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= R /\ -. S .<_ ( P .\/ R ) ) ) )
Theorem	4atexlemu 34878	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   =>    |- ( ph -> U e. A )
Theorem	4atexlemv 34879	Lemma for 4atexlem7 34889. (Contributed by NM, 23-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   =>    |- ( ph -> V e. A )
Theorem	4atexlemunv 34880	Lemma for 4atexlem7 34889. (Contributed by NM, 21-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   =>    |- ( ph -> U =/= V )
Theorem	4atexlemtlw 34881	Lemma for 4atexlem7 34889. (Contributed by NM, 24-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   =>    |- ( ph -> T .<_ W )
Theorem	4atexlemntlpq 34882	Lemma for 4atexlem7 34889. (Contributed by NM, 24-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   =>    |- ( ph -> -. T .<_ ( P .\/ Q ) )
Theorem	4atexlemc 34883	Lemma for 4atexlem7 34889. (Contributed by NM, 24-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   &    |- C = ( ( Q .\/ T ) ./\ ( P .\/ S ) )   =>    |- ( ph -> C e. A )
Theorem	4atexlemnclw 34884	Lemma for 4atexlem7 34889. (Contributed by NM, 24-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   &    |- C = ( ( Q .\/ T ) ./\ ( P .\/ S ) )   =>    |- ( ph -> -. C .<_ W )
Theorem	4atexlemex2 34885*	Lemma for 4atexlem7 34889. Show that when C =/= S, C satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   &    |- C = ( ( Q .\/ T ) ./\ ( P .\/ S ) )   =>    |- ( ( ph /\ C =/= S ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
Theorem	4atexlemcnd 34886	Lemma for 4atexlem7 34889. (Contributed by NM, 24-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   &    |- C = ( ( Q .\/ T ) ./\ ( P .\/ S ) )   &    |- D = ( ( R .\/ T ) ./\ ( P .\/ S ) )   =>    |- ( ph -> C =/= D )
Theorem	4atexlemex4 34887*	Lemma for 4atexlem7 34889. Show that when C = S, D satisfies the existence condition of the consequent. (Contributed by NM, 26-Nov-2012.)
|- ( ph <-> ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( S e. A /\ ( R e. A /\ -. R .<_ W /\ ( P .\/ R ) = ( Q .\/ R ) ) /\ ( T e. A /\ ( U .\/ T ) = ( V .\/ T ) ) ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   &    |- U = ( ( P .\/ Q ) ./\ W )   &    |- V = ( ( P .\/ S ) ./\ W )   &    |- C = ( ( Q .\/ T ) ./\ ( P .\/ S ) )   &    |- D = ( ( R .\/ T ) ./\ ( P .\/ S ) )   =>    |- ( ( ph /\ C = S ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
Theorem	4atexlemex6 34888*	Lemma for 4atexlem7 34889. (Contributed by NM, 25-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( ( K e. HL /\ W e. H ) /\ ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) ) /\ ( ( R e. A /\ -. R .<_ W ) /\ S e. A ) /\ ( ( P .\/ R ) = ( Q .\/ R ) /\ P =/= Q /\ -. S .<_ ( P .\/ Q ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
Theorem	4atexlem7 34889*	Whenever there are at least 4 atoms under P .\/ Q (specifically, P, Q, r, and ( P .\/ Q ) ./\ W), there are also at least 4 atoms under P .\/ S. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p \/ q/0 and hence p \/ s/0 contains at least four atoms..." Note that by cvlsupr2 34158, our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ). With a longer proof, the condition -. S .<_ ( P .\/ Q ) could be eliminated (see 4atex 34890), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ -. S .<_ ( P .\/ Q ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
Theorem	4atex 34890*	Whenever there are at least 4 atoms under P .\/ Q (specifically, P, Q, r, and ( P .\/ Q ) ./\ W), there are also at least 4 atoms under P .\/ S. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p \/ q/0 and hence p \/ s/0 contains at least four atoms..." Note that by cvlsupr2 34158, our ( P .\/ r ) = ( Q .\/ r ) is a shorter way to express r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ). (Contributed by NM, 27-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S e. A ) /\ ( P =/= Q /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( P .\/ z ) = ( S .\/ z ) ) )
Theorem	4atex2 34891*	More general version of 4atex 34890 for a line S .\/ T not necessarily connected to P .\/ Q. (Contributed by NM, 27-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T e. A /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )
Theorem	4atex2-0aOLDN 34892*	Same as 4atex2 34891 except that S is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S = ( 0. ` K ) ) /\ ( P =/= Q /\ ( T e. A /\ -. T .<_ W ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )
Theorem	4atex2-0bOLDN 34893*	Same as 4atex2 34891 except that T is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ T = ( 0. ` K ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )
Theorem	4atex2-0cOLDN 34894*	Same as 4atex2 34891 except that S and T are zero. TODO: do we need this one or 4atex2-0aOLDN 34892 or 4atex2-0bOLDN 34893? (Contributed by NM, 27-May-2013.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ S = ( 0. ` K ) ) /\ ( P =/= Q /\ T = ( 0. ` K ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( S .\/ z ) = ( T .\/ z ) ) )
Theorem	4atex3 34895*	More general version of 4atex 34890 for a line S .\/ T not necessarily connected to P .\/ Q. (Contributed by NM, 29-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- H = ( LHyp ` K )   =>    |- ( ( ( K e. HL /\ W e. H ) /\ ( ( P e. A /\ -. P .<_ W ) /\ ( Q e. A /\ -. Q .<_ W ) /\ ( S e. A /\ -. S .<_ W ) ) /\ ( P =/= Q /\ ( T e. A /\ S =/= T ) /\ E. r e. A ( -. r .<_ W /\ ( P .\/ r ) = ( Q .\/ r ) ) ) ) -> E. z e. A ( -. z .<_ W /\ ( z =/= S /\ z =/= T /\ z .<_ ( S .\/ T ) ) ) )
Theorem	lautset 34896*	The set of lattice automorphisms. (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- I = ( LAut ` K )   =>    |- ( K e. A -> I = { f | ( f : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( f ` x ) .<_ ( f ` y ) ) ) } )
Theorem	islaut 34897*	The predictate "is a lattice automorphism." (Contributed by NM, 11-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- I = ( LAut ` K )   =>    |- ( K e. A -> ( F e. I <-> ( F : B -1-1-onto-> B /\ A. x e. B A. y e. B ( x .<_ y <-> ( F ` x ) .<_ ( F ` y ) ) ) ) )
Theorem	lautle 34898	Less-than or equal property of a lattice automorphism. (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	laut1o 34899	A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012.)
|- B = ( Base ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( K e. A /\ F e. I ) -> F : B -1-1-onto-> B )
Theorem	laut11 34900	One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012.)
|- B = ( Base ` K )   &    |- I = ( LAut ` K )   =>    |- ( ( ( K e. V /\ F e. I ) /\ ( X e. B /\ Y e. B ) ) -> ( ( F ` X ) = ( F ` Y ) <-> X = Y ) )