P. 403 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40201-40300   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	polfvalN 40201*	The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝)))))
Theorem	polvalN 40202*	Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝))))
Theorem	polval2N 40203	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 40204	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 40205	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 40206	The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴)
Theorem	pol1N 40207	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 40208	The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅)
Theorem	polpmapN 40209	The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋)))
Theorem	2polpmapN 40210	Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋))
Theorem	2polvalN 40211	Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋)))
Theorem	2polssN 40212	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 40213	Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆))
Theorem	polcon3N 40214	Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	2polcon4bN 40215	Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))
Theorem	polcon2N 40216	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋))
Theorem	polcon2bN 40217	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋)))
Theorem	pclss2polN 40218	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 40219	The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅)
Theorem	pcl0bN 40220	The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅))
Theorem	pmaplubN 40221	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 40222	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 40223	Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆)))
Theorem	paddunN 40224	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 6839.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))
Theorem	poldmj1N 40225	De Morgan's law for polarity of projective sum. (oldmj1 39518 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇)))
Theorem	pmapj2N 40226	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 40227	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 40228	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 40229	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 40230	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 40231	Extend class notation with set of all closed projective subspaces for a Hilbert lattice.
class PSubCl
Definition	df-psubclN 40232*	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 40233*	The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)})
Theorem	ispsubclN 40234	The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)))
Theorem	psubcliN 40235	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))
Theorem	psubcli2N 40236	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	psubclsubN 40237	A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆)
Theorem	psubclssatN 40238	A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴)
Theorem	pmapidclN 40239	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 40240	The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶)
Theorem	1psubclN 40241	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 40242	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 40243	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 40244*	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 40245	The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶)
Theorem	paddatclN 40246	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 40247	The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 40197 and also pclcmpatN 40198. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑆 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	linepsubclN 40248	A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶)
Theorem	polsubclN 40249	A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶)
Theorem	poml4N 40250	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 40251	Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	poml6N 40252	Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)
Theorem	osumcllem1N 40253	Lemma for osumclN 40264. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀)
Theorem	osumcllem2N 40254	Lemma for osumclN 40264. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀))
Theorem	osumcllem3N 40255	Lemma for osumclN 40264. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌)
Theorem	osumcllem4N 40256	Lemma for osumclN 40264. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟)
Theorem	osumcllem5N 40257	Lemma for osumclN 40264. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem6N 40258	Lemma for osumclN 40264. Use atom exchange hlatexch1 39692 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem7N 40259*	Lemma for osumclN 40264. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem8N 40260	Lemma for osumclN 40264. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅)
Theorem	osumcllem9N 40261	Lemma for osumclN 40264. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋)
Theorem	osumcllem10N 40262	Lemma for osumclN 40264. Contradict osumcllem9N 40261. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 ≠ 𝑋)
Theorem	osumcllem11N 40263	Lemma for osumclN 40264. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))))
Theorem	osumclN 40264	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 40265	For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 40149 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌)))
Theorem	pexmidN 40266	Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 40250. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 40264. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴)
Theorem	pexmidlem1N 40267	Lemma for pexmidN 40266. 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 40268	Lemma for pexmidN 40266. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋) ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem3N 40269	Lemma for pexmidN 40266. Use atom exchange hlatexch1 39692 to swap 𝑝 and 𝑞. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem4N 40270*	Lemma for pexmidN 40266. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem5N 40271	Lemma for pexmidN 40266. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → (( ⊥ ‘𝑋) ∩ 𝑀) = ∅)
Theorem	pexmidlem6N 40272	Lemma for pexmidN 40266. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 = 𝑋)
Theorem	pexmidlem7N 40273	Lemma for pexmidN 40266. Contradict pexmidlem6N 40272. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 ≠ 𝑋)
Theorem	pexmidlem8N 40274	Lemma for pexmidN 40266. The contradiction of pexmidlem6N 40272 and pexmidlem7N 40273 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 40275	Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 40250. 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 40276	Lemma for pl42N 40280. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉))))
Theorem	pl42lem2N 40277	Lemma for pl42N 40280. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((𝐹‘𝑋) + (𝐹‘𝑌)) + (((𝐹‘𝑋) + (𝐹‘𝑊)) ∩ ((𝐹‘𝑌) + (𝐹‘𝑉)))) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉)))))
Theorem	pl42lem3N 40278	Lemma for pl42N 40280. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)) ⊆ ((((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑊)) ∩ (((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑉))))
Theorem	pl42lem4N 40279	Lemma for pl42N 40280. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉))))))
Theorem	pl42N 40280	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 40281	Extend class notation with set of all co-atoms (lattice hyperplanes).
class LHyp
Syntax	claut 40282	Extend class notation with set of all lattice automorphisms.
class LAut
Syntax	cwpointsN 40283	Extend class notation with W points.
class WAtoms
Syntax	cpautN 40284	Extend class notation with set of all projective automorphisms.
class PAut
Definition	df-lhyp 40285*	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 40286*	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 40287*	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 40288*	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 40289*	The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑊 = (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑}))))
Theorem	watvalN 40290	Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑊‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷})))
Theorem	iswatN 40291	The predicate "is a W atom" (corresponding to fiducial atom 𝐷). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    &   ⊢ 𝑊 = (WAtoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑃 ∈ (𝑊‘𝐷) ↔ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ((⊥𝑃‘𝐾)‘{𝐷}))))
Theorem	lhpset 40292*	The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → 𝐻 = {𝑤 ∈ 𝐵 ∣ 𝑤𝐶 1 })
Theorem	islhp 40293	The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐴 → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊𝐶 1 )))
Theorem	islhp2 40294	The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 18-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (𝑊 ∈ 𝐻 ↔ 𝑊𝐶 1 ))
Theorem	lhpbase 40295	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 40296	The lattice unity covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012.)
⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑊𝐶 1 )
Theorem	lhplt 40297	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 40298	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 ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) < 𝑊)
Theorem	lhpexlt 40299*	There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
⊢ < = (lt‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑊)
Theorem	lhp0lt 40300	A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.)
⊢ < = (lt‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐻 = (LHyp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 < 𝑊)