P. 330 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 32901-33000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	lecmtN 32901	Ordered elements commute. (lecmi 25005 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- C = ( cm ` K )   =>    |- ( ( K e. OML /\ X e. B /\ Y e. B ) -> ( X .<_ Y -> X C Y ) )
Theorem	cmtidN 32902	Any element commutes with itself. (cmidi 25013 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- C = ( cm ` K )   =>    |- ( ( K e. OML /\ X e. B ) -> X C X )
Theorem	omlfh1N 32903	Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in [Kalmbach] p. 25. (fh1 25021 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- C = ( cm ` K )   =>    |- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X ./\ ( Y .\/ Z ) ) = ( ( X ./\ Y ) .\/ ( X ./\ Z ) ) )
Theorem	omlfh3N 32904	Foulis-Holland Theorem, part 3. Dual of omlfh1N 32903. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- C = ( cm ` K )   =>    |- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Y /\ X C Z ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ ( X .\/ Z ) ) )
Theorem	omlmod1i2N 32905	Analog of modular law atmod1i2 33503 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- C = ( cm ` K )   =>    |- ( ( K e. OML /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X .<_ Z /\ Y C Z ) ) -> ( X .\/ ( Y ./\ Z ) ) = ( ( X .\/ Y ) ./\ Z ) )
Theorem	omlspjN 32906	Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. OML /\ ( X e. B /\ Y e. B ) /\ X .<_ Y ) -> ( ( X .\/ ( ._|_ ` Y ) ) ./\ Y ) = X )
21.30.7  Atomic lattices with covering property
Syntax	ccvr 32907	Extend class notation with covers relation.
class <o
Syntax	catm 32908	Extend class notation with atoms.
class Atoms
Syntax	cal 32909	Extend class notation with atomic lattices.
class AtLat
Syntax	clc 32910	Extend class notation with lattices with the covering property.
class CvLat
Definition	df-covers 32911*	Define the covers relation ("is covered by") for posets. " a is covered by b " means that a is strictly less than b and there is nothing in between. See cvrval 32914 for the relation form. (Contributed by NM, 18-Sep-2011.)
|- <o = ( p e. _V |-> { <. a , b >. | ( ( a e. ( Base ` p ) /\ b e. ( Base ` p ) ) /\ a ( lt ` p ) b /\ -. E. z e. ( Base ` p ) ( a ( lt ` p ) z /\ z ( lt ` p ) b ) ) } )
Definition	df-ats 32912*	Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.)
|- Atoms = ( p e. _V |-> { a e. ( Base ` p ) | ( 0. ` p ) ( <o ` p ) a } )
Theorem	cvrfval 32913*	Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( K e. A -> C = { <. x , y >. | ( ( x e. B /\ y e. B ) /\ x .< y /\ -. E. z e. B ( x .< z /\ z .< y ) ) } )
Theorem	cvrval 32914*	Binary relation expressing B covers A, which means that B is larger than A and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (cvbr 25686 analog.) (Contributed by NM, 18-Sep-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X .< Y /\ -. E. z e. B ( X .< z /\ z .< Y ) ) ) )
Theorem	cvrlt 32915	The covers relation implies the less-than relation. (cvpss 25689 analog.) (Contributed by NM, 8-Oct-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .< Y )
Theorem	cvrnbtwn 32916	There is no element between the two arguments of the covers relation. (cvnbtwn 25690 analog.) (Contributed by NM, 18-Oct-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. A /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> -. ( X .< Z /\ Z .< Y ) )
Theorem	ncvr1 32917	No element covers the lattice unit. (Contributed by NM, 8-Jul-2013.)
|- B = ( Base ` K )   &    |- .1. = ( 1. ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. OP /\ X e. B ) -> -. .1. C X )
Theorem	cvrletrN 32918	Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) ) -> ( ( X C Y /\ Y .<_ Z ) -> X .< Z ) )
Theorem	cvrval2 32919*	Binary relation expressing Y covers X. Definition of covers in [Kalmbach] p. 15. (cvbr2 25687 analog.) (Contributed by NM, 16-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. A /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( X .< Y /\ A. z e. B ( ( X .< z /\ z .<_ Y ) -> z = Y ) ) ) )
Theorem	cvrnbtwn2 32920	The covers relation implies no in-betweenness. (cvnbtwn2 25691 analog.) (Contributed by NM, 17-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .< Z /\ Z .<_ Y ) <-> Z = Y ) )
Theorem	cvrnbtwn3 32921	The covers relation implies no in-betweenness. (cvnbtwn3 25692 analog.) (Contributed by NM, 4-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .< Y ) <-> X = Z ) )
Theorem	cvrcon3b 32922	Contraposition law for the covers relation. (cvcon3 25688 analog.) (Contributed by NM, 4-Nov-2011.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. OP /\ X e. B /\ Y e. B ) -> ( X C Y <-> ( ._|_ ` Y ) C ( ._|_ ` X ) ) )
Theorem	cvrle 32923	The covers relation implies the less-than-or-equal relation. (Contributed by NM, 12-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- C = ( <o ` K )   =>    |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X .<_ Y )
Theorem	cvrnbtwn4 32924	The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 25693 analog.) (Contributed by NM, 18-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ X C Y ) -> ( ( X .<_ Z /\ Z .<_ Y ) <-> ( X = Z \/ Z = Y ) ) )
Theorem	cvrnle 32925	The covers relation implies the negation of the reverse less-than-or-equal relation. (Contributed by NM, 18-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- C = ( <o ` K )   =>    |- ( ( ( K e. Poset /\ X e. B /\ Y e. B ) /\ X C Y ) -> -. Y .<_ X )
Theorem	cvrne 32926	The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.)
|- B = ( Base ` K )   &    |- C = ( <o ` K )   =>    |- ( ( ( K e. A /\ X e. B /\ Y e. B ) /\ X C Y ) -> X =/= Y )
Theorem	cvrnrefN 32927	The covers relation is not reflexive. (cvnref 25695 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. A /\ X e. B ) -> -. X C X )
Theorem	cvrcmp 32928	If two lattice elements that cover a third are comparable, then they are equal. (Contributed by NM, 6-Feb-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. Poset /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( Z C X /\ Z C Y ) ) -> ( X .<_ Y <-> X = Y ) )
Theorem	cvrcmp2 32929	If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- C = ( <o ` K )   =>    |- ( ( K e. OP /\ ( X e. B /\ Y e. B /\ Z e. B ) /\ ( X C Z /\ Y C Z ) ) -> ( X .<_ Y <-> X = Y ) )
Theorem	pats 32930*	The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. D -> A = { x e. B | .0. C x } )
Theorem	isat 32931	The predicate "is an atom". (ela 25743 analog.) (Contributed by NM, 18-Sep-2011.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. D -> ( P e. A <-> ( P e. B /\ .0. C P ) ) )
Theorem	isat2 32932	The predicate "is an atom". (elatcv0 25745 analog.) (Contributed by NM, 18-Jun-2012.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. D /\ P e. B ) -> ( P e. A <-> .0. C P ) )
Theorem	atcvr0 32933	An atom covers zero. (atcv0 25746 analog.) (Contributed by NM, 4-Nov-2011.)
|- .0. = ( 0. ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. D /\ P e. A ) -> .0. C P )
Theorem	atbase 32934	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 25748 analog.) (Contributed by NM, 10-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- ( P e. A -> P e. B )
Theorem	atssbase 32935	The set of atoms is a subset of the base set. (atssch 25747 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- A C_ B
Theorem	0ltat 32936	An atom is greater than zero. (Contributed by NM, 4-Jul-2012.)
|- .0. = ( 0. ` K )   &    |- .< = ( lt ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. OP /\ P e. A ) -> .0. .< P )
Theorem	leatb 32937	A poset element less than or equal to an atom equals either zero or the atom. (atss 25750 analog.) (Contributed by NM, 17-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. OP /\ X e. B /\ P e. A ) -> ( X .<_ P <-> ( X = P \/ X = .0. ) ) )
Theorem	leat 32938	A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OP /\ X e. B /\ P e. A ) /\ X .<_ P ) -> ( X = P \/ X = .0. ) )
Theorem	leat2 32939	A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-2013.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OP /\ X e. B /\ P e. A ) /\ ( X =/= .0. /\ X .<_ P ) ) -> X = P )
Theorem	leat3 32940	A poset element less than or equal to an atom is either an atom or zero. (Contributed by NM, 2-Dec-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OP /\ X e. B /\ P e. A ) /\ X .<_ P ) -> ( X e. A \/ X = .0. ) )
Theorem	meetat 32941	The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012.)
|- B = ( Base ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = P \/ ( X ./\ P ) = .0. ) )
Theorem	meetat2 32942	The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012.)
|- B = ( Base ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. OL /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) e. A \/ ( X ./\ P ) = .0. ) )
Definition	df-atl 32943*	Define the class of atomic lattices, in which every nonzero element is greater than or equal to an atom. We also ensure the existence of a lattice zero, since a lattice by itself may not have a zero. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.)
|- AtLat = { k e. Lat | ( ( Base ` k ) e. dom ( glb ` k ) /\ A. x e. ( Base ` k ) ( x =/= ( 0. ` k ) -> E. p e. ( Atoms ` k ) p ( le ` k ) x ) ) }
Theorem	isatl 32944*	The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.)
|- B = ( Base ` K )   &    |- G = ( glb ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. AtLat <-> ( K e. Lat /\ B e. dom G /\ A. x e. B ( x =/= .0. -> E. y e. A y .<_ x ) ) )
Theorem	atllat 32945	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
|- ( K e. AtLat -> K e. Lat )
Theorem	atlpos 32946	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
|- ( K e. AtLat -> K e. Poset )
Theorem	atl0dm 32947	Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   =>    |- ( K e. AtLat -> B e. dom G )
Theorem	atl0cl 32948	An atomic lattice has a zero element. We can use this in place of op0cl 32829 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. AtLat -> .0. e. B )
Theorem	atl0le 32949	Orthoposet zero is less than or equal to any element. (ch0le 24844 analog.) (Contributed by NM, 12-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. AtLat /\ X e. B ) -> .0. .<_ X )
Theorem	atlle0 32950	An element less than or equal to zero equals zero. (chle0 24846 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. AtLat /\ X e. B ) -> ( X .<_ .0. <-> X = .0. ) )
Theorem	atlltn0 32951	A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( ( K e. AtLat /\ X e. B ) -> ( .0. .< X <-> X =/= .0. ) )
Theorem	isat3 32952*	The predicate "is an atom". (elat2 25744 analog.) (Contributed by NM, 27-Apr-2014.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. AtLat -> ( P e. A <-> ( P e. B /\ P =/= .0. /\ A. x e. B ( x .<_ P -> ( x = P \/ x = .0. ) ) ) ) )
Theorem	atn0 32953	An atom is not zero. (atne0 25749 analog.) (Contributed by NM, 5-Nov-2012.)
|- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A ) -> P =/= .0. )
Theorem	atnle0 32954	An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.)
|- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A ) -> -. P .<_ .0. )
Theorem	atlen0 32955	A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. AtLat /\ X e. B /\ P e. A ) /\ P .<_ X ) -> X =/= .0. )
Theorem	atcmp 32956	If two atoms are comparable, they are equal. (atsseq 25751 analog.) (Contributed by NM, 13-Oct-2011.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P .<_ Q <-> P = Q ) )
Theorem	atncmp 32957	Frequently-used variation of atcmp 32956. (Contributed by NM, 29-Jun-2012.)
|- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( -. P .<_ Q <-> P =/= Q ) )
Theorem	atnlt 32958	Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.)
|- .< = ( lt ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P .< Q )
Theorem	atcvreq0 32959	An element covered by an atom must be zero. (atcveq0 25752 analog.) (Contributed by NM, 4-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ X e. B /\ P e. A ) -> ( X C P <-> X = .0. ) )
Theorem	atncvrN 32960	Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.)
|- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> -. P C Q )
Theorem	atlex 32961*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 25764 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ X e. B /\ X =/= .0. ) -> E. y e. A y .<_ X )
Theorem	atnle 32962	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 25780 analog.) (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A /\ X e. B ) -> ( -. P .<_ X <-> ( P ./\ X ) = .0. ) )
Theorem	atnem0 32963	The meet of distinct atoms is zero. (atnemeq0 25781 analog.) (Contributed by NM, 5-Nov-2012.)
|- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> ( P ./\ Q ) = .0. ) )
Theorem	atlatmstc 32964*	An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in [Kalmbach] p. 140; also remark in [BeltramettiCassinelli] p. 98. (hatomistici 25766 analog.) (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .1. = ( lub ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B ) -> ( .1. ` { y e. A | y .<_ X } ) = X )
Theorem	atlatle 32965*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 25775 analog.) (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .<_ Y <-> A. p e. A ( p .<_ X -> p .<_ Y ) ) )
Theorem	atlrelat1 32966*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 25767, with /\ swapped, analog.) (Contributed by NM, 4-Dec-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ X e. B /\ Y e. B ) -> ( X .< Y -> E. p e. A ( -. p .<_ X /\ p .<_ Y ) ) )
Definition	df-cvlat 32967*	Define the class of atomic lattices with the covering property. (This is actually the exchange property, but they are equivalent. The literature usually uses the covering property terminology.) (Contributed by NM, 5-Nov-2012.)
|- CvLat = { k e. AtLat | A. a e. ( Atoms ` k ) A. b e. ( Atoms ` k ) A. c e. ( Base ` k ) ( ( -. a ( le ` k ) c /\ a ( le ` k ) ( c ( join ` k ) b ) ) -> b ( le ` k ) ( c ( join ` k ) a ) ) }
Theorem	iscvlat 32968*	The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( -. p .<_ x /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
Theorem	iscvlat2N 32969*	The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. CvLat <-> ( K e. AtLat /\ A. p e. A A. q e. A A. x e. B ( ( ( p ./\ x ) = .0. /\ p .<_ ( x .\/ q ) ) -> q .<_ ( x .\/ p ) ) ) )
Theorem	cvlatl 32970	An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.)
|- ( K e. CvLat -> K e. AtLat )
Theorem	cvllat 32971	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
|- ( K e. CvLat -> K e. Lat )
Theorem	cvlposN 32972	An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
|- ( K e. CvLat -> K e. Poset )
Theorem	cvlexch1 32973	An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )
Theorem	cvlexch2 32974	An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( Q .\/ X ) -> Q .<_ ( P .\/ X ) ) )
Theorem	cvlexchb1 32975	An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
Theorem	cvlexchb2 32976	An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( Q .\/ X ) <-> ( P .\/ X ) = ( Q .\/ X ) ) )
Theorem	cvlexch3 32977	An atomic covering lattice has the exchange property. (atexch 25785 analog.) (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )
Theorem	cvlexch4N 32978	An atomic covering lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ X e. B ) /\ ( P ./\ X ) = .0. ) -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
Theorem	cvlatexchb1 32979	A version of cvlexchb1 32975 for atoms. (Contributed by NM, 5-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( R .\/ Q ) <-> ( R .\/ P ) = ( R .\/ Q ) ) )
Theorem	cvlatexchb2 32980	A version of cvlexchb2 32976 for atoms. (Contributed by NM, 5-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( Q .\/ R ) <-> ( P .\/ R ) = ( Q .\/ R ) ) )
Theorem	cvlatexch1 32981	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( R .\/ Q ) -> Q .<_ ( R .\/ P ) ) )
Theorem	cvlatexch2 32982	Atom exchange property. (Contributed by NM, 5-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= R ) -> ( P .<_ ( Q .\/ R ) -> Q .<_ ( P .\/ R ) ) )
Theorem	cvlatexch3 32983	Atom exchange property. (Contributed by NM, 29-Nov-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ P =/= R ) ) -> ( P .<_ ( Q .\/ R ) -> ( P .\/ Q ) = ( P .\/ R ) ) )
Theorem	cvlcvr1 32984	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 25759 analog.) (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( -. P .<_ X <-> X C ( X .\/ P ) ) )
Theorem	cvlcvrp 32985	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 25779 analog.) (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- .0. = ( 0. ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ X e. B /\ P e. A ) -> ( ( X ./\ P ) = .0. <-> X C ( X .\/ P ) ) )
Theorem	cvlatcvr1 32986	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
|- .\/ = ( join ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> P C ( P .\/ Q ) ) )
Theorem	cvlatcvr2 32987	An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.)
|- .\/ = ( join ` K )   &    |- C = ( <o ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ P e. A /\ Q e. A ) -> ( P =/= Q <-> P C ( Q .\/ P ) ) )
Theorem	cvlsupr2 32988	Two equivalent ways of expressing that R is a superposition of P and Q. (Contributed by NM, 5-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ P =/= Q ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) )
Theorem	cvlsupr3 32989	Two equivalent ways of expressing that R is a superposition of P and Q, which can replace the superposition part of ishlat1 32997, ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ), with the simpler E. z e. A ( x .\/ z ) = ( y .\/ z ) as shown in ishlat3N 32999. (Contributed by NM, 5-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ R ) = ( Q .\/ R ) <-> ( P =/= Q -> ( R =/= P /\ R =/= Q /\ R .<_ ( P .\/ Q ) ) ) ) )
Theorem	cvlsupr4 32990	Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ). (Contributed by NM, 9-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> R .<_ ( P .\/ Q ) )
Theorem	cvlsupr5 32991	Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ). (Contributed by NM, 9-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> R =/= P )
Theorem	cvlsupr6 32992	Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ). (Contributed by NM, 9-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> R =/= Q )
Theorem	cvlsupr7 32993	Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ). (Contributed by NM, 24-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> ( P .\/ Q ) = ( R .\/ Q ) )
Theorem	cvlsupr8 32994	Consequence of superposition condition ( P .\/ R ) = ( Q .\/ R ). (Contributed by NM, 24-Nov-2012.)
|- A = ( Atoms ` K )   &    |- .\/ = ( join ` K )   =>    |- ( ( K e. CvLat /\ ( P e. A /\ Q e. A /\ R e. A ) /\ ( P =/= Q /\ ( P .\/ R ) = ( Q .\/ R ) ) ) -> ( P .\/ Q ) = ( P .\/ R ) )
21.30.8  Hilbert lattices
Syntax	chlt 32995	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 32996*	Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.)
|- HL = { l e. ( ( OML i^i CLat ) i^i CvLat ) | ( A. a e. ( Atoms ` l ) A. b e. ( Atoms ` l ) ( a =/= b -> E. c e. ( Atoms ` l ) ( c =/= a /\ c =/= b /\ c ( le ` l ) ( a ( join ` l ) b ) ) ) /\ E. a e. ( Base ` l ) E. b e. ( Base ` l ) E. c e. ( Base ` l ) ( ( ( 0. ` l ) ( lt ` l ) a /\ a ( lt ` l ) b ) /\ ( b ( lt ` l ) c /\ c ( lt ` l ) ( 1. ` l ) ) ) ) }
Theorem	ishlat1 32997*	The predicate "is a Hilbert lattice," which is orthomodular ( K e. OML), complete ( K e. CLat), atomic and satisfying the exchange (or covering) property ( K e. CvLat), satisfies the superposition principle, and has a minimum height of 4. (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- .\/ = ( join ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
Theorem	ishlat2 32998*	The predicate "is a Hilbert lattice". Here we replace K e. CvLat with the weaker K e. AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- .\/ = ( join ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. AtLat ) /\ ( A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
Theorem	ishlat3N 32999*	The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form E. z e. A ( x .\/ z ) = ( y .\/ z ). The exchange property and atomicity are provided by K e. CvLat, and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- .\/ = ( join ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( K e. HL <-> ( ( K e. OML /\ K e. CLat /\ K e. CvLat ) /\ ( A. x e. A A. y e. A E. z e. A ( x .\/ z ) = ( y .\/ z ) /\ E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) ) ) )
Theorem	ishlatiN 33000*	Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.)
|- K e. OML   &    |- K e. CLat   &    |- K e. AtLat   &    |- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .< = ( lt ` K )   &    |- .\/ = ( join ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   &    |- A = ( Atoms ` K )   &    |- A. x e. A A. y e. A ( ( x =/= y -> E. z e. A ( z =/= x /\ z =/= y /\ z .<_ ( x .\/ y ) ) ) /\ A. z e. B ( ( -. x .<_ z /\ x .<_ ( z .\/ y ) ) -> y .<_ ( z .\/ x ) ) )   &    |- E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) )   =>    |- K e. HL