P. 344 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 34301-34400   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	isat2 34301	The predicate "is an atom". (elatcv0 27033 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 34302	An atom covers zero. (atcv0 27034 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 34303	An atom is a member of the lattice base set (i.e. a lattice element). (atelch 27036 analog.) (Contributed by NM, 10-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- ( P e. A -> P e. B )
Theorem	atssbase 34304	The set of atoms is a subset of the base set. (atssch 27035 analog.) (Contributed by NM, 21-Oct-2011.)
|- B = ( Base ` K )   &    |- A = ( Atoms ` K )   =>    |- A C_ B
Theorem	0ltat 34305	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 34306	A poset element less than or equal to an atom equals either zero or the atom. (atss 27038 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 34307	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 34308	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 34309	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 34310	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 34311	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 34312*	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 34313*	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 34314	An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.)
|- ( K e. AtLat -> K e. Lat )
Theorem	atlpos 34315	An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.)
|- ( K e. AtLat -> K e. Poset )
Theorem	atl0dm 34316	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 34317	An atomic lattice has a zero element. We can use this in place of op0cl 34198 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.)
|- B = ( Base ` K )   &    |- .0. = ( 0. ` K )   =>    |- ( K e. AtLat -> .0. e. B )
Theorem	atl0le 34318	Orthoposet zero is less than or equal to any element. (ch0le 26132 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 34319	An element less than or equal to zero equals zero. (chle0 26134 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 34320	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 34321*	The predicate "is an atom". (elat2 27032 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 34322	An atom is not zero. (atne0 27037 analog.) (Contributed by NM, 5-Nov-2012.)
|- .0. = ( 0. ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. AtLat /\ P e. A ) -> P =/= .0. )
Theorem	atnle0 34323	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 34324	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 34325	If two atoms are comparable, they are equal. (atsseq 27039 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 34326	Frequently-used variation of atcmp 34325. (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 34327	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 34328	An element covered by an atom must be zero. (atcveq0 27040 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 34329	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 34330*	Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 27052 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 34331	Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 27068 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 34332	The meet of distinct atoms is zero. (atnemeq0 27069 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 34333*	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 27054 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 34334*	The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 27063 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 34335*	An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 27055, 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 34336*	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 34337*	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 34338*	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 34339	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 34340	An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.)
|- ( K e. CvLat -> K e. Lat )
Theorem	cvlposN 34341	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 34342	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 34343	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 34344	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 34345	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 34346	An atomic covering lattice has the exchange property. (atexch 27073 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 34347	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 34348	A version of cvlexchb1 34344 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 34349	A version of cvlexchb2 34345 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 34350	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 34351	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 34352	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 34353	The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 27047 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 34354	A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 27067 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 34355	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 34356	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 34357	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 34358	Two equivalent ways of expressing that R is a superposition of P and Q, which can replace the superposition part of ishlat1 34366, ( 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 34368. (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 34359	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 34360	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 34361	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 34362	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 34363	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 34364	Extend class notation with Hilbert lattices.
class HL
Definition	df-hlat 34365*	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 34366*	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 34367*	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 34368*	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 34369*	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 34370	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 34371	A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OML )
Theorem	hlclat 34372	A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. CLat )
Theorem	hlcvl 34373	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 34374	A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. AtLat )
Theorem	hlol 34375	A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OL )
Theorem	hlop 34376	A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. OP )
Theorem	hllat 34377	A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. Lat )
Theorem	hlomcmat 34378	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 34379	A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.)
|- ( K e. HL -> K e. Poset )
Theorem	hlatjcl 34380	Closure of join operation. Frequently-used special case of latjcl 15541 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 34381	Commutatitivity of join operation. Frequently-used special case of latjcom 15549 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 34382	Idempotence of join operation. Frequently-used special case of latjcom 15549 for atoms. (Contributed by NM, 15-Jul-2012.)
|- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   =>    |- ( ( K e. HL /\ X e. A ) -> ( X .\/ X ) = X )
Theorem	hlatjass 34383	Lattice join is associative. Frequently-used special case of latjass 15585 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 34384	Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 15587 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 34385	Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 15587 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 34386	Rotate lattice join of 3 classes. Frequently-used special case of latjrot 15590 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 34387	Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 15591 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 34388	A join's first argument is less than or equal to the join. Special case of latlej1 15550 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 34389	A join's second argument is less than or equal to the join. Special case of latlej2 15551 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 34390*	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 34391*	De Morgan's law for GLB and LUB. Index-set version of glbconN 34390, 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 34392	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 34393	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 34394*	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 34395	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 34396	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 34397	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 34398	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 34399*	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 34400*	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 ) )