P. 336 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 33501-33600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	pclclN 33501	Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. V /\ X C_ A ) -> ( U ` X ) e. S )
Theorem	elpclN 33502*	Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- U = ( PCl ` K )   &    |- Q e. _V   =>    |- ( ( K e. V /\ X C_ A ) -> ( Q e. ( U ` X ) <-> A. y e. S ( X C_ y -> Q e. y ) ) )
Theorem	elpcliN 33503	Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( ( K e. V /\ X C_ Y /\ Y e. S ) /\ Q e. ( U ` X ) ) -> Q e. Y )
Theorem	pclssN 33504	Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. V /\ X C_ Y /\ Y C_ A ) -> ( U ` X ) C_ ( U ` Y ) )
Theorem	pclssidN 33505	A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. V /\ X C_ A ) -> X C_ ( U ` X ) )
Theorem	pclidN 33506	The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. V /\ X e. S ) -> ( U ` X ) = X )
Theorem	pclbtwnN 33507	A projective subspace sandwiched between a set of atoms and the set's projective subspace closure equals the closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( ( K e. V /\ X e. S ) /\ ( Y C_ X /\ X C_ ( U ` Y ) ) ) -> X = ( U ` Y ) )
Theorem	pclunN 33508	The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. V /\ X C_ A /\ Y C_ A ) -> ( U ` ( X u. Y ) ) = ( U ` ( X .+ Y ) ) )
Theorem	pclun2N 33509	The projective subspace closure of the union of two subspaces equals their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- .+ = ( +P ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. HL /\ X e. S /\ Y e. S ) -> ( U ` ( X u. Y ) ) = ( X .+ Y ) )
Theorem	pclfinN 33510*	The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of [PtakPulmannova] p. 72. Compare the closed subspace version pclfinclN 33560. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. AtLat /\ X C_ A ) -> ( U ` X ) = U_ y e. ( Fin i^i ~P X ) ( U ` y ) )
Theorem	pclcmpatN 33511*	The set of projective subspaces is compactly atomistic: if an atom is in the projective subspace closure of a set of atoms, it also belongs to the projective subspace closure of a finite subset of that set. Analogous to Lemma 3.3.10 of [PtakPulmannova] p. 74. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. AtLat /\ X C_ A /\ P e. ( U ` X ) ) -> E. y e. Fin ( y C_ X /\ P e. ( U ` y ) ) )
Syntax	cpolN 33512	Extend class notation with polarity of projective subspace $m$.
class _|_P
Definition	df-polarityN 33513*	Define polarity of projective subspace, which is a kind of complement of the subspace. Item 2 in [Holland95] p. 222 bottom. For more generality, we define it for all subsets of atoms, not just projective subspaces. The intersection with Atoms ` l ensures it is defined when m = (/). (Contributed by NM, 23-Oct-2011.)
|- _|_P = ( l e. _V |-> ( m e. ~P ( Atoms ` l ) |-> ( ( Atoms ` l ) i^i |^|_ p e. m ( ( pmap ` l ) ` ( ( oc ` l ) ` p ) ) ) ) )
Theorem	polfvalN 33514*	The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
|- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   &    |- P = ( _|_P ` K )   =>    |- ( K e. B -> P = ( m e. ~P A |-> ( A i^i |^|_ p e. m ( M ` ( ._|_ ` p ) ) ) ) )
Theorem	polvalN 33515*	Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
|- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   &    |- P = ( _|_P ` K )   =>    |- ( ( K e. B /\ X C_ A ) -> ( P ` X ) = ( A i^i |^|_ p e. X ( M ` ( ._|_ ` p ) ) ) )
Theorem	polval2N 33516	Alternate expression for value of the projective subspace polarity function. Equation for polarity in [Holland95] p. 223. (Contributed by NM, 22-Jan-2012.) (New usage is discouraged.)
|- U = ( lub ` K )   &    |- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   &    |- P = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( P ` X ) = ( M ` ( ._|_ ` ( U ` X ) ) ) )
Theorem	polsubN 33517	The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- S = ( PSubSp ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) e. S )
Theorem	polssatN 33518	The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) C_ A )
Theorem	pol0N 33519	The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( K e. B -> ( ._|_ ` (/) ) = A )
Theorem	pol1N 33520	The polarity of the whole projective subspace is the empty space. Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( K e. HL -> ( ._|_ ` A ) = (/) )
Theorem	2pol0N 33521	The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
|- ._|_ = ( _|_P ` K )   =>    |- ( K e. HL -> ( ._|_ ` ( ._|_ ` (/) ) ) = (/) )
Theorem	polpmapN 33522	The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- ._|_ = ( oc ` K )   &    |- M = ( pmap ` K )   &    |- P = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X e. B ) -> ( P ` ( M ` X ) ) = ( M ` ( ._|_ ` X ) ) )
Theorem	2polpmapN 33523	Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- M = ( pmap ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X e. B ) -> ( ._|_ ` ( ._|_ ` ( M ` X ) ) ) = ( M ` X ) )
Theorem	2polvalN 33524	Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- U = ( lub ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` ( ._|_ ` X ) ) = ( M ` ( U ` X ) ) )
Theorem	2polssN 33525	A set of atoms is a subset of its double polarity. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> X C_ ( ._|_ ` ( ._|_ ` X ) ) )
Theorem	3polN 33526	Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ S C_ A ) -> ( ._|_ ` ( ._|_ ` ( ._|_ ` S ) ) ) = ( ._|_ ` S ) )
Theorem	polcon3N 33527	Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ Y C_ A /\ X C_ Y ) -> ( ._|_ ` Y ) C_ ( ._|_ ` X ) )
Theorem	2polcon4bN 33528	Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( ._|_ ` ( ._|_ ` X ) ) C_ ( ._|_ ` ( ._|_ ` Y ) ) <-> ( ._|_ ` Y ) C_ ( ._|_ ` X ) ) )
Theorem	polcon2N 33529	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> Y C_ ( ._|_ ` X ) )
Theorem	polcon2bN 33530	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( X C_ ( ._|_ ` Y ) <-> Y C_ ( ._|_ ` X ) ) )
Theorem	pclss2polN 33531	The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( U ` X ) C_ ( ._|_ ` ( ._|_ ` X ) ) )
Theorem	pcl0N 33532	The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
|- U = ( PCl ` K )   =>    |- ( K e. HL -> ( U ` (/) ) = (/) )
Theorem	pcl0bN 33533	The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- U = ( PCl ` K )   =>    |- ( ( K e. HL /\ P C_ A ) -> ( ( U ` P ) = (/) <-> P = (/) ) )
Theorem	pmaplubN 33534	The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- U = ( lub ` K )   &    |- M = ( pmap ` K )   =>    |- ( ( K e. HL /\ X e. B ) -> ( U ` ( M ` X ) ) = X )
Theorem	sspmaplubN 33535	A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
|- U = ( lub ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   =>    |- ( ( K e. HL /\ S C_ A ) -> S C_ ( M ` ( U ` S ) ) )
Theorem	2pmaplubN 33536	Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
|- U = ( lub ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   =>    |- ( ( K e. HL /\ S C_ A ) -> ( M ` ( U ` ( M ` ( U ` S ) ) ) ) = ( M ` ( U ` S ) ) )
Theorem	paddunN 33537	The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d 5892.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ._|_ ` ( S u. T ) ) )
Theorem	poldmj1N 33538	De Morgan's law for polarity of projective sum. (oldmj1 32832 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ S C_ A /\ T C_ A ) -> ( ._|_ ` ( S .+ T ) ) = ( ( ._|_ ` S ) i^i ( ._|_ ` T ) ) )
Theorem	pmapj2N 33539	The projective map of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- M = ( pmap ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( M ` ( X .\/ Y ) ) = ( ._|_ ` ( ._|_ ` ( ( M ` X ) .+ ( M ` Y ) ) ) ) )
Theorem	pmapocjN 33540	The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- F = ( pmap ` K )   &    |- .+ = ( +P ` K )   &    |- N = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X e. B /\ Y e. B ) -> ( F ` ( ._|_ ` ( X .\/ Y ) ) ) = ( N ` ( ( F ` X ) .+ ( F ` Y ) ) ) )
Theorem	polatN 33541	The polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
|- ._|_ = ( oc ` K )   &    |- A = ( Atoms ` K )   &    |- M = ( pmap ` K )   &    |- P = ( _|_P ` K )   =>    |- ( ( K e. OL /\ Q e. A ) -> ( P ` { Q } ) = ( M ` ( ._|_ ` Q ) ) )
Theorem	2polatN 33542	Double polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- P = ( _|_P ` K )   =>    |- ( ( K e. HL /\ Q e. A ) -> ( P ` ( P ` { Q } ) ) = { Q } )
Theorem	pnonsingN 33543	The intersection of a set of atoms and its polarity is empty. Definition of nonsingular in [Holland95] p. 214. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- P = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( X i^i ( P ` X ) ) = (/) )
Syntax	cpscN 33544	Extend class notation with set of all closed projective subspaces for a Hilbert lattice.
class PSubCl
Definition	df-psubclN 33545*	Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in [Holland95] p. 223. (Contributed by NM, 23-Jan-2012.)
|- PSubCl = ( k e. _V |-> { s | ( s C_ ( Atoms ` k ) /\ ( ( _|_P ` k ) ` ( ( _|_P ` k ) ` s ) ) = s ) } )
Theorem	psubclsetN 33546*	The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( K e. B -> C = { s | ( s C_ A /\ ( ._|_ ` ( ._|_ ` s ) ) = s ) } )
Theorem	ispsubclN 33547	The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( K e. D -> ( X e. C <-> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) ) )
Theorem	psubcliN 33548	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. D /\ X e. C ) -> ( X C_ A /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) )
Theorem	psubcli2N 33549	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
|- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. D /\ X e. C ) -> ( ._|_ ` ( ._|_ ` X ) ) = X )
Theorem	psubclsubN 33550	A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
|- S = ( PSubSp ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X e. C ) -> X e. S )
Theorem	psubclssatN 33551	A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. D /\ X e. C ) -> X C_ A )
Theorem	pmapidclN 33552	Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
|- U = ( lub ` K )   &    |- M = ( pmap ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X e. C ) -> ( M ` ( U ` X ) ) = X )
Theorem	0psubclN 33553	The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- C = ( PSubCl ` K )   =>    |- ( K e. HL -> (/) e. C )
Theorem	1psubclN 33554	The set of all atoms is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( K e. HL -> A e. C )
Theorem	atpsubclN 33555	A point (singleton of an atom) is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ Q e. A ) -> { Q } e. C )
Theorem	pmapsubclN 33556	A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- M = ( pmap ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X e. B ) -> ( M ` X ) e. C )
Theorem	ispsubcl2N 33557*	Alternate predicate for "is a closed projective subspace". Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- M = ( pmap ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( K e. HL -> ( X e. C <-> E. y e. B X = ( M ` y ) ) )
Theorem	psubclinN 33558	The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X e. C /\ Y e. C ) -> ( X i^i Y ) e. C )
Theorem	paddatclN 33559	The projective sum of a closed subspace and an atom is a closed projective subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X e. C /\ Q e. A ) -> ( X .+ { Q } ) e. C )
Theorem	pclfinclN 33560	The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 33510 and also pclcmpatN 33511. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- U = ( PCl ` K )   &    |- S = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X C_ A /\ X e. Fin ) -> ( U ` X ) e. S )
Theorem	linepsubclN 33561	A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- N = ( Lines ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X e. N ) -> X e. C )
Theorem	polsubclN 33562	A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( K e. HL /\ X C_ A ) -> ( ._|_ ` X ) e. C )
Theorem	poml4N 33563	Orthomodular law for projective lattices. Lemma 3.3(1) in [Holland95] p. 215. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ X C_ A /\ Y C_ A ) -> ( ( X C_ Y /\ ( ._|_ ` ( ._|_ ` Y ) ) = Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = ( ._|_ ` ( ._|_ ` X ) ) ) )
Theorem	poml5N 33564	Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i ( ._|_ ` Y ) ) ) i^i ( ._|_ ` Y ) ) = ( ._|_ ` ( ._|_ ` X ) ) )
Theorem	poml6N 33565	Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- C = ( PSubCl ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ Y ) -> ( ( ._|_ ` ( ( ._|_ ` X ) i^i Y ) ) i^i Y ) = X )
Theorem	osumcllem1N 33566	Lemma for osumclN 33577. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. U ) -> ( U i^i M ) = M )
Theorem	osumcllem2N 33567	Lemma for osumclN 33577. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. U ) -> X C_ ( U i^i M ) )
Theorem	osumcllem3N 33568	Lemma for osumclN 33577. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( K e. HL /\ Y e. C /\ X C_ ( ._|_ ` Y ) ) -> ( ( ._|_ ` X ) i^i U ) = Y )
Theorem	osumcllem4N 33569	Lemma for osumclN 33577. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ Y C_ A /\ X C_ ( ._|_ ` Y ) ) /\ ( r e. X /\ q e. Y ) ) -> q =/= r )
Theorem	osumcllem5N 33570	Lemma for osumclN 33577. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ ( r e. X /\ q e. Y /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ Y ) )
Theorem	osumcllem6N 33571	Lemma for osumclN 33577. Use atom exchange hlatexch1 33005 to swap p and q. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ p e. A ) /\ ( r e. X /\ q e. Y /\ q .<_ ( r .\/ p ) ) ) -> p e. ( X .+ Y ) )
Theorem	osumcllem7N 33572*	Lemma for osumclN 33577. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ q e. ( Y i^i M ) ) -> p e. ( X .+ Y ) )
Theorem	osumcllem8N 33573	Lemma for osumclN 33577. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. A ) /\ -. p e. ( X .+ Y ) ) -> ( Y i^i M ) = (/) )
Theorem	osumcllem9N 33574	Lemma for osumclN 33577. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) /\ p e. U ) /\ -. p e. ( X .+ Y ) ) -> M = X )
Theorem	osumcllem10N 33575	Lemma for osumclN 33577. Contradict osumcllem9N 33574. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   &    |- M = ( X .+ { p } )   &    |- U = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) )   =>    |- ( ( ( K e. HL /\ X C_ A /\ Y C_ A ) /\ p e. A /\ -. p e. ( X .+ Y ) ) -> M =/= X )
Theorem	osumcllem11N 33576	Lemma for osumclN 33577. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ ( X C_ ( ._|_ ` Y ) /\ X =/= (/) ) ) -> ( X .+ Y ) = ( ._|_ ` ( ._|_ ` ( X .+ Y ) ) ) )
Theorem	osumclN 33577	Closure of orthogonal sum. If X and Y are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- C = ( PSubCl ` K )   =>    |- ( ( ( K e. HL /\ X e. C /\ Y e. C ) /\ X C_ ( ._|_ ` Y ) ) -> ( X .+ Y ) e. C )
Theorem	pmapojoinN 33578	For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 33462 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- M = ( pmap ` K )   &    |- ._|_ = ( oc ` K )   &    |- .+ = ( +P ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ X .<_ ( ._|_ ` Y ) ) -> ( M ` ( X .\/ Y ) ) = ( ( M ` X ) .+ ( M ` Y ) ) )
Theorem	pexmidN 33579	Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 33563. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 33577. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )
Theorem	pexmidlem1N 33580	Lemma for pexmidN 33579. Holland's proof implicitly requires q =/= r, which we prove here. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) ) -> q =/= r )
Theorem	pexmidlem2N 33581	Lemma for pexmidN 33579. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) /\ p .<_ ( r .\/ q ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
Theorem	pexmidlem3N 33582	Lemma for pexmidN 33579. Use atom exchange hlatexch1 33005 to swap p and q. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( r e. X /\ q e. ( ._|_ ` X ) ) /\ q .<_ ( r .\/ p ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
Theorem	pexmidlem4N 33583*	Lemma for pexmidN 33579. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ q e. ( ( ._|_ ` X ) i^i M ) ) ) -> p e. ( X .+ ( ._|_ ` X ) ) )
Theorem	pexmidlem5N 33584	Lemma for pexmidN 33579. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> ( ( ._|_ ` X ) i^i M ) = (/) )
Theorem	pexmidlem6N 33585	Lemma for pexmidN 33579. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M = X )
Theorem	pexmidlem7N 33586	Lemma for pexmidN 33579. Contradict pexmidlem6N 33585. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
|- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   &    |- M = ( X .+ { p } )   =>    |- ( ( ( K e. HL /\ X C_ A /\ p e. A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) /\ -. p e. ( X .+ ( ._|_ ` X ) ) ) ) -> M =/= X )
Theorem	pexmidlem8N 33587	Lemma for pexmidN 33579. The contradiction of pexmidlem6N 33585 and pexmidlem7N 33586 shows that there can be no atom p that is not in X .+ ( ._|_ ` X ), which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( ( K e. HL /\ X C_ A ) /\ ( ( ._|_ ` ( ._|_ ` X ) ) = X /\ X =/= (/) ) ) -> ( X .+ ( ._|_ ` X ) ) = A )
Theorem	pexmidALTN 33588	Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 33563. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables X, M, p, q, r in place of Hollands' l, m, P, Q, L respectively. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
|- A = ( Atoms ` K )   &    |- .+ = ( +P ` K )   &    |- ._|_ = ( _|_P ` K )   =>    |- ( ( ( K e. HL /\ X C_ A ) /\ ( ._|_ ` ( ._|_ ` X ) ) = X ) -> ( X .+ ( ._|_ ` X ) ) = A )
Theorem	pl42lem1N 33589	Lemma for pl42N 33593. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- F = ( pmap ` K )   &    |- .+ = ( +P ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) = ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) ) )
Theorem	pl42lem2N 33590	Lemma for pl42N 33593. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- F = ( pmap ` K )   &    |- .+ = ( +P ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( ( ( F ` X ) .+ ( F ` W ) ) i^i ( ( F ` Y ) .+ ( F ` V ) ) ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
Theorem	pl42lem3N 33591	Lemma for pl42N 33593. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- F = ( pmap ` K )   &    |- .+ = ( +P ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( ( ( ( F ` X ) .+ ( F ` Y ) ) i^i ( F ` Z ) ) .+ ( F ` W ) ) i^i ( F ` V ) ) C_ ( ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` W ) ) i^i ( ( ( F ` X ) .+ ( F ` Y ) ) .+ ( F ` V ) ) ) )
Theorem	pl42lem4N 33592	Lemma for pl42N 33593. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   &    |- F = ( pmap ` K )   &    |- .+ = ( +P ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( F ` ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) ) C_ ( F ` ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) ) )
Theorem	pl42N 33593	Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in [MegPav2000] p. 2366). (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
|- B = ( Base ` K )   &    |- .<_ = ( le ` K )   &    |- .\/ = ( join ` K )   &    |- ./\ = ( meet ` K )   &    |- ._|_ = ( oc ` K )   =>    |- ( ( ( K e. HL /\ X e. B /\ Y e. B ) /\ ( Z e. B /\ W e. B /\ V e. B ) ) -> ( ( X .<_ ( ._|_ ` Y ) /\ Z .<_ ( ._|_ ` W ) ) -> ( ( ( ( X .\/ Y ) ./\ Z ) .\/ W ) ./\ V ) .<_ ( ( X .\/ Y ) .\/ ( ( X .\/ W ) ./\ ( Y .\/ V ) ) ) ) )
Syntax	clh 33594	Extend class notation with set of all co-atoms (lattice hyperplanes).
class LHyp
Syntax	claut 33595	Extend class notation with set of all lattice automorphisms.
class LAut
Syntax	cwpointsN 33596	Extend class notation with W points.
class WAtoms
Syntax	cpautN 33597	Extend class notation with set of all projective automorphisms.
class PAut
Definition	df-lhyp 33598*	Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e. all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.)
|- LHyp = ( k e. _V |-> { x e. ( Base ` k ) | x ( <o ` k ) ( 1. ` k ) } )
Definition	df-laut 33599*	Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.)
|- LAut = ( k e. _V |-> { f | ( f : ( Base ` k ) -1-1-onto-> ( Base ` k ) /\ A. x e. ( Base ` k ) A. y e. ( Base ` k ) ( x ( le ` k ) y <-> ( f ` x ) ( le ` k ) ( f ` y ) ) ) } )
Definition	df-watsN 33600*	Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" d. These are all atoms not in the polarity of { d } ), which is the hyperplane determined by d. Definition of set W in [Crawley] p. 111. (Contributed by NM, 26-Jan-2012.)
|- WAtoms = ( k e. _V |-> ( d e. ( Atoms ` k ) |-> ( ( Atoms ` k ) \ ( ( _|_P ` k ) ` { d } ) ) ) )