P. 380 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 37901-38000   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dalawlem10 37901	Lemma for dalaw 37907. Combine dalawlem5 37896, dalawlem8 37899, and dalawlem9 . (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃)) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem11 37902	Lemma for dalaw 37907. First part of dalawlem13 37904. (Contributed by NM, 17-Sep-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem12 37903	Lemma for dalaw 37907. Second part of dalawlem13 37904. (Contributed by NM, 17-Sep-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem13 37904	Lemma for dalaw 37907. Special case to eliminate the requirement ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 in dalawlem1 37892. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem14 37905	Lemma for dalaw 37907. Combine dalawlem10 37901 and dalawlem13 37904. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem15 37906	Lemma for dalaw 37907. Swap variable triples 𝑃𝑄𝑅 and 𝑆𝑇𝑈 in dalawlem14 37905, to obtain the elimination of the remaining conditions in dalawlem1 37892. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalaw 37907	Desargues's law, derived from Desargues's theorem dath 37757 and with no conditions on the atoms. If triples ⟨𝑃, 𝑄, 𝑅⟩ and ⟨𝑆, 𝑇, 𝑈⟩ are centrally perspective, i.e., ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈), then they are axially perspective. Theorem 13.3 of [Crawley] p. 110. (Contributed by NM, 7-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)))))
Syntax	cpclN 37908	Extend class notation with projective subspace closure.
class PCl
Definition	df-pclN 37909*	Projective subspace closure, which is the smallest projective subspace containing an arbitrary set of atoms. The subspace closure of the union of a set of projective subspaces is their supremum in PSubSp. Related to an analogous definition of closure used in Lemma 3.1.4 of [PtakPulmannova] p. 68. (Note that this closure is not necessarily one of the closed projective subspaces PSubCl of df-psubclN 37956.) (Contributed by NM, 7-Sep-2013.)
⊢ PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))
Theorem	pclfvalN 37910*	The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝑈 = (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦}))
Theorem	pclvalN 37911*	Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦})
Theorem	pclclN 37912	Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	elpclN 37913*	Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑄 ∈ V    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑄 ∈ (𝑈‘𝑋) ↔ ∀𝑦 ∈ 𝑆 (𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦)))
Theorem	elpcliN 37914	Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆) ∧ 𝑄 ∈ (𝑈‘𝑋)) → 𝑄 ∈ 𝑌)
Theorem	pclssN 37915	Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘𝑋) ⊆ (𝑈‘𝑌))
Theorem	pclssidN 37916	A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ (𝑈‘𝑋))
Theorem	pclidN 37917	The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆) → (𝑈‘𝑋) = 𝑋)
Theorem	pclbtwnN 37918	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.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ (𝑈‘𝑌))) → 𝑋 = (𝑈‘𝑌))
Theorem	pclunN 37919	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.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑈‘(𝑋 + 𝑌)))
Theorem	pclun2N 37920	The projective subspace closure of the union of two subspaces equals their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑋 + 𝑌))
Theorem	pclfinN 37921*	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 37971. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
Theorem	pclcmpatN 37922*	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.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑃 ∈ (𝑈‘𝑋)) → ∃𝑦 ∈ Fin (𝑦 ⊆ 𝑋 ∧ 𝑃 ∈ (𝑈‘𝑦)))
Syntax	cpolN 37923	Extend class notation with polarity of projective subspace $m$.
class ⊥𝑃
Definition	df-polarityN 37924*	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 37925*	The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝)))))
Theorem	polvalN 37926*	Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝))))
Theorem	polval2N 37927	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 37928	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 37929	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 37930	The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴)
Theorem	pol1N 37931	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 37932	The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅)
Theorem	polpmapN 37933	The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋)))
Theorem	2polpmapN 37934	Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋))
Theorem	2polvalN 37935	Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋)))
Theorem	2polssN 37936	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 37937	Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆))
Theorem	polcon3N 37938	Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	2polcon4bN 37939	Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))
Theorem	polcon2N 37940	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋))
Theorem	polcon2bN 37941	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋)))
Theorem	pclss2polN 37942	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 37943	The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅)
Theorem	pcl0bN 37944	The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅))
Theorem	pmaplubN 37945	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 37946	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 37947	Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆)))
Theorem	paddunN 37948	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 6787.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))
Theorem	poldmj1N 37949	De Morgan's law for polarity of projective sum. (oldmj1 37242 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇)))
Theorem	pmapj2N 37950	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 37951	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 37952	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 37953	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 37954	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 37955	Extend class notation with set of all closed projective subspaces for a Hilbert lattice.
class PSubCl
Definition	df-psubclN 37956*	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 37957*	The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)})
Theorem	ispsubclN 37958	The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)))
Theorem	psubcliN 37959	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))
Theorem	psubcli2N 37960	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	psubclsubN 37961	A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆)
Theorem	psubclssatN 37962	A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴)
Theorem	pmapidclN 37963	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 37964	The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶)
Theorem	1psubclN 37965	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 37966	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 37967	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 37968*	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 37969	The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶)
Theorem	paddatclN 37970	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 37971	The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 37921 and also pclcmpatN 37922. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑆 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	linepsubclN 37972	A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶)
Theorem	polsubclN 37973	A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶)
Theorem	poml4N 37974	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 37975	Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	poml6N 37976	Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)
Theorem	osumcllem1N 37977	Lemma for osumclN 37988. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀)
Theorem	osumcllem2N 37978	Lemma for osumclN 37988. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀))
Theorem	osumcllem3N 37979	Lemma for osumclN 37988. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌)
Theorem	osumcllem4N 37980	Lemma for osumclN 37988. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟)
Theorem	osumcllem5N 37981	Lemma for osumclN 37988. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem6N 37982	Lemma for osumclN 37988. Use atom exchange hlatexch1 37416 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem7N 37983*	Lemma for osumclN 37988. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem8N 37984	Lemma for osumclN 37988. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅)
Theorem	osumcllem9N 37985	Lemma for osumclN 37988. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋)
Theorem	osumcllem10N 37986	Lemma for osumclN 37988. Contradict osumcllem9N 37985. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 ≠ 𝑋)
Theorem	osumcllem11N 37987	Lemma for osumclN 37988. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))))
Theorem	osumclN 37988	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 37989	For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 37873 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌)))
Theorem	pexmidN 37990	Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 37974. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 37988. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴)
Theorem	pexmidlem1N 37991	Lemma for pexmidN 37990. 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 37992	Lemma for pexmidN 37990. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋) ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem3N 37993	Lemma for pexmidN 37990. Use atom exchange hlatexch1 37416 to swap 𝑝 and 𝑞. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem4N 37994*	Lemma for pexmidN 37990. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))
Theorem	pexmidlem5N 37995	Lemma for pexmidN 37990. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → (( ⊥ ‘𝑋) ∩ 𝑀) = ∅)
Theorem	pexmidlem6N 37996	Lemma for pexmidN 37990. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 = 𝑋)
Theorem	pexmidlem7N 37997	Lemma for pexmidN 37990. Contradict pexmidlem6N 37996. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 ≠ 𝑋)
Theorem	pexmidlem8N 37998	Lemma for pexmidN 37990. The contradiction of pexmidlem6N 37996 and pexmidlem7N 37997 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 37999	Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 37974. 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 38000	Lemma for pl42N 38004. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉))))