P. 355 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 35401-35500   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	cvrnbtwn4 35401	The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 27406 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 35402	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 35403	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 35404	The covers relation is not reflexive. (cvnref 27408 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 35405	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 35406	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 35407*	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 35408	The predicate "is an atom". (ela 27456 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 35409	The predicate "is an atom". (elatcv0 27458 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 35410	An atom covers zero. (atcv0 27459 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 35411	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 27461 analog.) (Contributed by NM, 10-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- ( P e. A -> P e. B )
Theorem	atssbase 35412	The set of atoms is a subset of the base set. (atssch 27460 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- A C_ B
Theorem	0ltat 35413	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 35414	A poset element less than or equal to an atom equals either zero or the atom. (atss 27463 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 35415	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 35416	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 35417	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 35418	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 35419	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 35420*	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 35421*	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 35422	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
|- ( K e. AtLat -> K e. Lat )
Theorem	atlpos 35423	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
|- ( K e. AtLat -> K e. Poset )
Theorem	atl0dm 35424	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 35425	An atomic lattice has a zero element. We can use this in place of op0cl 35306 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. AtLat -> .0. e. B )
Theorem	atl0le 35426	Orthoposet zero is less than or equal to any element. (ch0le 26557 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 35427	An element less than or equal to zero equals zero. (chle0 26559 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 35428	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 35429*	The predicate "is an atom". (elat2 27457 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 35430	An atom is not zero. (atne0 27462 analog.) (Contributed by NM, 5-Nov-2012.)
|- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A ) -> P =/= .0. )
Theorem	atnle0 35431	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 35432	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 35433	If two atoms are comparable, they are equal. (atsseq 27464 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 35434	Frequently-used variation of atcmp 35433. (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 35435	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 35436	An element covered by an atom must be zero. (atcveq0 27465 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 35437	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 35438*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 27477 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 35439	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 27493 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 35440	The meet of distinct atoms is zero. (atnemeq0 27494 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 35441*	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 27479 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 35442*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 27488 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 35443*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 27480, 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 35444*	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 35445*	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 35446*	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 35447	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 35448	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
|- ( K e. CvLat -> K e. Lat )
Theorem	cvlposN 35449	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 35450	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 35451	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 35452	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 35453	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 35454	An atomic covering lattice has the exchange property. (atexch 27498 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 35455	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 35456	A version of cvlexchb1 35452 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 35457	A version of cvlexchb2 35453 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 35458	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 35459	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 35460	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 35461	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 27472 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 35462	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27492 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 35463	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 35464	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 35465	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 35466	Two equivalent ways of expressing that R is a superposition of P and Q, which can replace the superposition part of ishlat1 35474, ( 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 35476. (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 35467	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 35468	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 35469	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 35470	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 35471	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.29.8  Hilbert lattices
Syntax	chlt 35472	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 35473*	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 35474*	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 35475*	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 35476*	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 35477*	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
Theorem	hlomcmcv 35478	A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.)
|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. CvLat ) )
Theorem	hloml 35479	A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OML )
Theorem	hlclat 35480	A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. CLat )
Theorem	hlcvl 35481	A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.)
|- ( K e. HL -> K e. CvLat )
Theorem	hlatl 35482	A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. AtLat )
Theorem	hlol 35483	A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OL )
Theorem	hlop 35484	A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OP )
Theorem	hllat 35485	A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. Lat )
Theorem	hlomcmat 35486	A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.)
|- ( K e. HL -> ( K e. OML /\ K e. CLat /\ K e. AtLat ) )
Theorem	hlpos 35487	A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. Poset )
Theorem	hlatjcl 35488	Closure of join operation. Frequently-used special case of latjcl 15880 for atoms. (Contributed by NM, 15-Jun-2012.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X .\/ Y ) e. B )
Theorem	hlatjcom 35489	Commutatitivity of join operation. Frequently-used special case of latjcom 15888 for atoms. (Contributed by NM, 15-Jun-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ X e. A /\ Y e. A ) -> ( X .\/ Y ) = ( Y .\/ X ) )
Theorem	hlatjidm 35490	Idempotence of join operation. Frequently-used special case of latjcom 15888 for atoms. (Contributed by NM, 15-Jul-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ X e. A ) -> ( X .\/ X ) = X )
Theorem	hlatjass 35491	Lattice join is associative. Frequently-used special case of latjass 15924 for atoms. (Contributed by NM, 27-Jul-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) = ( P .\/ ( Q .\/ R ) ) )
Theorem	hlatj12 35492	Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 15926 for atoms. (Contributed by NM, 4-Jun-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( P .\/ ( Q .\/ R ) ) = ( Q .\/ ( P .\/ R ) ) )
Theorem	hlatj32 35493	Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 15926 for atoms. (Contributed by NM, 21-Jul-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( P .\/ R ) .\/ Q ) )
Theorem	hlatjrot 35494	Rotate lattice join of 3 classes. Frequently-used special case of latjrot 15929 for atoms. (Contributed by NM, 2-Aug-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) ) -> ( ( P .\/ Q ) .\/ R ) = ( ( R .\/ P ) .\/ Q ) )
Theorem	hlatj4 35495	Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 15930 for atoms. (Contributed by NM, 9-Aug-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A ) /\ ( R e. A /\ S e. A ) ) -> ( ( P .\/ Q ) .\/ ( R .\/ S ) ) = ( ( P .\/ R ) .\/ ( Q .\/ S ) ) )
Theorem	hlatlej1 35496	A join's first argument is less than or equal to the join. Special case of latlej1 15889 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> P .<_ ( P .\/ Q ) )
Theorem	hlatlej2 35497	A join's second argument is less than or equal to the join. Special case of latlej2 15890 to show an atom is on a line. (Contributed by NM, 15-May-2013.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> Q .<_ ( P .\/ Q ) )
Theorem	glbconN 35498*	De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. HL /\ S C_ B ) -> ( G ` S ) = ( ._|_ ` ( U ` { x e. B | ( ._|_ ` x ) e. S } ) ) )
Theorem	glbconxN 35499*	De Morgan's law for GLB and LUB. Index-set version of glbconN 35498, where we read S as S ( i ). (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- G = ( glb ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( K e. HL /\ A. i e. I S e. B ) -> ( G ` { x | E. i e. I x = S } ) = ( ._|_ ` ( U ` { x | E. i e. I x = ( ._|_ ` S ) } ) ) )
Theorem	atnlej1 35500	If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ R e. A ) /\ -. P .<_ ( Q .\/ R ) ) -> P =/= Q )