P. 405 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40401-40500   *Has distinct variable group(s)

Type	Label	Description
Statement
Syntax	cpolN 40401	Extend class notation with polarity of projective subspace $m$.
class ⊥𝑃
Definition	df-polarityN 40402*	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‘𝑙 ensures it is defined when 𝑚 = ∅. (Contributed by NM, 23-Oct-2011.)
⊢ ⊥𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝)))))
Theorem	polfvalN 40403*	The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝)))))
Theorem	polvalN 40404*	Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝))))
Theorem	polval2N 40405	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.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝑀‘( ⊥ ‘(𝑈‘𝑋))))
Theorem	polsubN 40406	The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝑆)
Theorem	polssatN 40407	The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ⊆ 𝐴)
Theorem	pol0N 40408	The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴)
Theorem	pol1N 40409	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.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ( ⊥ ‘𝐴) = ∅)
Theorem	2pol0N 40410	The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅)
Theorem	polpmapN 40411	The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋)))
Theorem	2polpmapN 40412	Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋))
Theorem	2polvalN 40413	Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋)))
Theorem	2polssN 40414	A set of atoms is a subset of its double polarity. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	3polN 40415	Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆))
Theorem	polcon3N 40416	Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	2polcon4bN 40417	Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))
Theorem	polcon2N 40418	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋))
Theorem	polcon2bN 40419	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋)))
Theorem	pclss2polN 40420	The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ⊆ ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	pcl0N 40421	The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅)
Theorem	pcl0bN 40422	The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅))
Theorem	pmaplubN 40423	The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑈‘(𝑀‘𝑋)) = 𝑋)
Theorem	sspmaplubN 40424	A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ (𝑀‘(𝑈‘𝑆)))
Theorem	2pmaplubN 40425	Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆)))
Theorem	paddunN 40426	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 6838.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))
Theorem	poldmj1N 40427	De Morgan's law for polarity of projective sum. (oldmj1 39720 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇)))
Theorem	pmapj2N 40428	The projective map of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘(𝑋 ∨ 𝑌)) = ( ⊥ ‘( ⊥ ‘((𝑀‘𝑋) + (𝑀‘𝑌)))))
Theorem	pmapocjN 40429	The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ 𝑁 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘( ⊥ ‘(𝑋 ∨ 𝑌))) = (𝑁‘((𝐹‘𝑋) + (𝐹‘𝑌))))
Theorem	polatN 40430	The polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴) → (𝑃‘{𝑄}) = (𝑀‘( ⊥ ‘𝑄)))
Theorem	2polatN 40431	Double polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑃‘(𝑃‘{𝑄})) = {𝑄})
Theorem	pnonsingN 40432	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.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) = ∅)
Syntax	cpscN 40433	Extend class notation with set of all closed projective subspaces for a Hilbert lattice.
class PSubCl
Definition	df-psubclN 40434*	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 = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)})
Theorem	psubclsetN 40435*	The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)})
Theorem	ispsubclN 40436	The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)))
Theorem	psubcliN 40437	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))
Theorem	psubcli2N 40438	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	psubclsubN 40439	A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆)
Theorem	psubclssatN 40440	A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴)
Theorem	pmapidclN 40441	Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → (𝑀‘(𝑈‘𝑋)) = 𝑋)
Theorem	0psubclN 40442	The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶)
Theorem	1psubclN 40443	The set of all atoms is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → 𝐴 ∈ 𝐶)
Theorem	atpsubclN 40444	A point (singleton of an atom) is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → {𝑄} ∈ 𝐶)
Theorem	pmapsubclN 40445	A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ 𝐶)
Theorem	ispsubcl2N 40446*	Alternate predicate for "is a closed projective subspace". Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦)))
Theorem	psubclinN 40447	The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶)
Theorem	paddatclN 40448	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.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) ∈ 𝐶)
Theorem	pclfinclN 40449	The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 40399 and also pclcmpatN 40400. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑆 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	linepsubclN 40450	A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶)
Theorem	polsubclN 40451	A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶)
Theorem	poml4N 40452	Orthomodular law for projective lattices. Lemma 3.3(1) in [Holland95] p. 215. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋))))
Theorem	poml5N 40453	Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	poml6N 40454	Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)
Theorem	osumcllem1N 40455	Lemma for osumclN 40466. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀)
Theorem	osumcllem2N 40456	Lemma for osumclN 40466. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀))
Theorem	osumcllem3N 40457	Lemma for osumclN 40466. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌)
Theorem	osumcllem4N 40458	Lemma for osumclN 40466. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟)
Theorem	osumcllem5N 40459	Lemma for osumclN 40466. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem6N 40460	Lemma for osumclN 40466. Use atom exchange hlatexch1 39894 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem7N 40461*	Lemma for osumclN 40466. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem8N 40462	Lemma for osumclN 40466. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅)
Theorem	osumcllem9N 40463	Lemma for osumclN 40466. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋)
Theorem	osumcllem10N 40464	Lemma for osumclN 40466. Contradict osumcllem9N 40463. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 ≠ 𝑋)
Theorem	osumcllem11N 40465	Lemma for osumclN 40466. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))))
Theorem	osumclN 40466	Closure of orthogonal sum. If 𝑋 and 𝑌 are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (𝑋 + 𝑌) ∈ 𝐶)
Theorem	pmapojoinN 40467	For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 40351 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌)))
Theorem	pexmidN 40468	Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 40452. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 40466. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴)
Theorem	pexmidlem1N 40469	Lemma for pexmidN 40468. Holland's proof implicitly requires 𝑞 ≠ 𝑟, which we prove here. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋))) → 𝑞 ≠ 𝑟)
Theorem	pexmidlem2N 40470	Lemma for pexmidN 40468. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋) ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem3N 40471	Lemma for pexmidN 40468. Use atom exchange hlatexch1 39894 to swap 𝑝 and 𝑞. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem4N 40472*	Lemma for pexmidN 40468. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem5N 40473	Lemma for pexmidN 40468. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → (( ⊥ ‘𝑋) ∩ 𝑀) = ∅)
Theorem	pexmidlem6N 40474	Lemma for pexmidN 40468. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 = 𝑋)
Theorem	pexmidlem7N 40475	Lemma for pexmidN 40468. Contradict pexmidlem6N 40474. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 ≠ 𝑋)
Theorem	pexmidlem8N 40476	Lemma for pexmidN 40468. The contradiction of pexmidlem6N 40474 and pexmidlem7N 40475 shows that there can be no atom 𝑝 that is not in 𝑋 + ( ⊥ ‘𝑋), which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅)) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴)
Theorem	pexmidALTN 40477	Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 40452. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables 𝑋, 𝑀, 𝑝, 𝑞, 𝑟 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.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴)
Theorem	pl42lem1N 40478	Lemma for pl42N 40482. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉))))
Theorem	pl42lem2N 40479	Lemma for pl42N 40482. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((𝐹‘𝑋) + (𝐹‘𝑌)) + (((𝐹‘𝑋) + (𝐹‘𝑊)) ∩ ((𝐹‘𝑌) + (𝐹‘𝑉)))) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉)))))
Theorem	pl42lem3N 40480	Lemma for pl42N 40482. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)) ⊆ ((((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑊)) ∩ (((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑉))))
Theorem	pl42lem4N 40481	Lemma for pl42N 40482. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉))))))
Theorem	pl42N 40482	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.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → ((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉) ≤ ((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉)))))
Syntax	clh 40483	Extend class notation with set of all co-atoms (lattice hyperplanes).
class LHyp
Syntax	claut 40484	Extend class notation with set of all lattice automorphisms.
class LAut
Syntax	cwpointsN 40485	Extend class notation with W points.
class WAtoms
Syntax	cpautN 40486	Extend class notation with set of all projective automorphisms.
class PAut
Definition	df-lhyp 40487*	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 = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)})
Definition	df-laut 40488*	Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.)
⊢ LAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))})
Definition	df-watsN 40489*	Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" 𝑑. These are all atoms not in the polarity of {𝑑}), which is the hyperplane determined by 𝑑. Definition of set W in [Crawley] p. 111. (Contributed by NM, 26-Jan-2012.)
⊢ WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑}))))
Definition	df-pautN 40490*	Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.)
⊢ PAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))})
Theorem	watfvalN 40491*	The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑊 = (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑}))))
Theorem	watvalN 40492	Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑊‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷})))
Theorem	iswatN 40493	The predicate "is a W atom" (corresponding to fiducial atom 𝐷). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑃 ∈ (𝑊‘𝐷) ↔ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ((⊥𝑃‘𝐾)‘{𝐷}))))
Theorem	lhpset 40494*	The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐻 = {𝑤 ∈ 𝐵 ∣ 𝑤𝐶 1 })
Theorem	islhp 40495	The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊𝐶 1 )))
Theorem	islhp2 40496	The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (𝑊 ∈ 𝐻 ↔ 𝑊𝐶 1 ))
Theorem	lhpbase 40497	A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵)
Theorem	lhp1cvr 40498	The lattice unity covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012.)
⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑊𝐶 1 )
Theorem	lhplt 40499	An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊)) → 𝑃 < 𝑊)
Theorem	lhp2lt 40500	The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) < 𝑊)