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	atbase 32901	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 28053 analog.) (Contributed by NM, 10-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- ( P e. A -> P e. B )
Theorem	atssbase 32902	The set of atoms is a subset of the base set. (atssch 28052 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- A C_ B
Theorem	0ltat 32903	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 32904	A poset element less than or equal to an atom equals either zero or the atom. (atss 28055 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 32905	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 32906	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 32907	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 32908	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 32909	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 32910*	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 32911*	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 32912	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
|- ( K e. AtLat -> K e. Lat )
Theorem	atlpos 32913	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
|- ( K e. AtLat -> K e. Poset )
Theorem	atl0dm 32914	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 32915	An atomic lattice has a zero element. We can use this in place of op0cl 32796 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. AtLat -> .0. e. B )
Theorem	atl0le 32916	Orthoposet zero is less than or equal to any element. (ch0le 27150 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 32917	An element less than or equal to zero equals zero. (chle0 27152 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 32918	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 32919*	The predicate "is an atom". (elat2 28049 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 32920	An atom is not zero. (atne0 28054 analog.) (Contributed by NM, 5-Nov-2012.)
|- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A ) -> P =/= .0. )
Theorem	atnle0 32921	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 32922	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 32923	If two atoms are comparable, they are equal. (atsseq 28056 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 32924	Frequently-used variation of atcmp 32923. (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 32925	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 32926	An element covered by an atom must be zero. (atcveq0 28057 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 32927	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 32928*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 28069 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 32929	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 28085 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 32930	The meet of distinct atoms is zero. (atnemeq0 28086 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 32931*	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 28071 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 32932*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 28080 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 32933*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 28072, 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 32934*	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 32935*	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 32936*	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 32937	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 32938	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
|- ( K e. CvLat -> K e. Lat )
Theorem	cvlposN 32939	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 32940	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 32941	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 32942	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 32943	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 32944	An atomic covering lattice has the exchange property. (atexch 28090 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 32945	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 32946	A version of cvlexchb1 32942 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 32947	A version of cvlexchb2 32943 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 32948	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 32949	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 32950	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 32951	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 28064 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 32952	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 28084 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 32953	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 32954	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 32955	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 32956	Two equivalent ways of expressing that R is a superposition of P and Q, which can replace the superposition part of ishlat1 32964, ( 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 32966. (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 32957	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 32958	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 32959	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 32960	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 32961	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.21.11  Hilbert lattices
Syntax	chlt 32962	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 32963*	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 32964*	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 32965*	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 32966*	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 32967*	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 32968	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 32969	A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OML )
Theorem	hlclat 32970	A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. CLat )
Theorem	hlcvl 32971	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 32972	A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. AtLat )
Theorem	hlol 32973	A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OL )
Theorem	hlop 32974	A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OP )
Theorem	hllat 32975	A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. Lat )
Theorem	hlomcmat 32976	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 32977	A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. Poset )
Theorem	hlatjcl 32978	Closure of join operation. Frequently-used special case of latjcl 16352 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 32979	Commutatitivity of join operation. Frequently-used special case of latjcom 16360 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 32980	Idempotence of join operation. Frequently-used special case of latjcom 16360 for atoms. (Contributed by NM, 15-Jul-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ X e. A ) -> ( X .\/ X ) = X )
Theorem	hlatjass 32981	Lattice join is associative. Frequently-used special case of latjass 16396 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 32982	Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 16398 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 32983	Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 16398 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 32984	Rotate lattice join of 3 classes. Frequently-used special case of latjrot 16401 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 32985	Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 16402 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 32986	A join's first argument is less than or equal to the join. Special case of latlej1 16361 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 32987	A join's second argument is less than or equal to the join. Special case of latlej2 16362 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 32988*	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 32989*	De Morgan's law for GLB and LUB. Index-set version of glbconN 32988, 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 32990	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 )
Theorem	atnlej2 32991	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 =/= R )
Theorem	hlsuprexch 32992*	A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> ( ( P =/= Q -> E. z e. A ( z =/= P /\ z =/= Q /\ z .<_ ( P .\/ Q ) ) ) /\ A. z e. B ( ( -. P .<_ z /\ P .<_ ( z .\/ Q ) ) -> Q .<_ ( z .\/ P ) ) ) )
Theorem	hlexch1 32993	A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) -> Q .<_ ( X .\/ P ) ) )
Theorem	hlexch2 32994	A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( Q .\/ X ) -> Q .<_ ( P .\/ X ) ) )
Theorem	hlexchb1 32995	A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( X .\/ Q ) <-> ( X .\/ P ) = ( X .\/ Q ) ) )
Theorem	hlexchb2 32996	A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ ( P e. A /\ Q e. A /\ X e. B ) /\ -. P .<_ X ) -> ( P .<_ ( Q .\/ X ) <-> ( P .\/ X ) = ( Q .\/ X ) ) )
Theorem	hlsupr 32997*	A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( ( K e. HL /\ P e. A /\ Q e. A ) /\ P =/= Q ) -> E. r e. A ( r =/= P /\ r =/= Q /\ r .<_ ( P .\/ Q ) ) )
Theorem	hlsupr2 32998*	A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ P e. A /\ Q e. A ) -> E. r e. A ( P .\/ r ) = ( Q .\/ r ) )
Theorem	hlhgt4 32999*	A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( K e. HL -> E. x e. B E. y e. B E. z e. B ( ( .0. .< x /\ x .< y ) /\ ( y .< z /\ z .< .1. ) ) )
Theorem	hlhgt2 33000*	A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.)
|- B = ( Base ` K )   &    |- .< = ( lt ` K )   &    |- .0. = ( 0. ` K )   &    |- .1. = ( 1. ` K )   =>    |- ( K e. HL -> E. x e. B ( .0. .< x /\ x .< .1. ) )