P. 406 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 40501-40600   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	atmod3i2 40501	Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 ∨ (𝑌 ∧ 𝑃)) = (𝑌 ∧ (𝑋 ∨ 𝑃)))
Theorem	atmod4i1 40502	Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 10-Jun-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑌) → ((𝑋 ∧ 𝑌) ∨ 𝑃) = ((𝑋 ∨ 𝑃) ∧ 𝑌))
Theorem	atmod4i2 40503	Version of modular law that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 4-Jun-2012.) (Revised by Mario Carneiro, 10-Mar-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑃 ∧ 𝑌) ∨ 𝑋) = ((𝑃 ∨ 𝑋) ∧ 𝑌))
Theorem	llnexchb2lem 40504	Lemma for llnexchb2 40505. (Contributed by NM, 17-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋) ∧ (𝑋 ∧ 𝑌) ∈ 𝐴) → ((𝑋 ∧ 𝑌) ≤ (𝑃 ∨ 𝑄) ↔ (𝑋 ∧ 𝑌) = (𝑋 ∧ (𝑃 ∨ 𝑄))))
Theorem	llnexchb2 40505	Line exchange property (compare cvlatexchb2 39971 for atoms). (Contributed by NM, 17-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁) ∧ ((𝑋 ∧ 𝑌) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍)) → ((𝑋 ∧ 𝑌) ≤ 𝑍 ↔ (𝑋 ∧ 𝑌) = (𝑋 ∧ 𝑍)))
Theorem	llnexch2N 40506	Line exchange property (compare cvlatexch2 39973 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁) ∧ ((𝑋 ∧ 𝑌) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍)) → ((𝑋 ∧ 𝑌) ≤ 𝑍 → (𝑋 ∧ 𝑍) ≤ 𝑌))
Theorem	dalawlem1 40507	Lemma for dalaw 40522. Special case of dath2 40373, where 𝐶 is replaced by ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)). The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 40373. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) ∧ ((¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃)) ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆)) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem2 40508	Lemma for dalaw 40522. Utility lemma that breaks ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) into a join of two pieces. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ (((𝑃 ∨ 𝑄) ∨ 𝑆) ∧ 𝑇)))
Theorem	dalawlem3 40509	Lemma for dalaw 40522. First piece of dalawlem5 40511. (Contributed by NM, 4-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem4 40510	Lemma for dalaw 40522. Second piece of dalawlem5 40511. (Contributed by NM, 4-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∨ 𝑄) ∧ 𝑇) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem5 40511	Lemma for dalaw 40522. Special case to eliminate the requirement ¬ (𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) in dalawlem1 40507. (Contributed by NM, 4-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem6 40512	Lemma for dalaw 40522. First piece of dalawlem8 40514. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem7 40513	Lemma for dalaw 40522. Second piece of dalawlem8 40514. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑆) ∧ 𝑇) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem8 40514	Lemma for dalaw 40522. Special case to eliminate the requirement ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) in dalawlem1 40507. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem9 40515	Lemma for dalaw 40522. Special case to eliminate the requirement ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃) in dalawlem1 40507. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem10 40516	Lemma for dalaw 40522. Combine dalawlem5 40511, dalawlem8 40514, and dalawlem9 . (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃)) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem11 40517	Lemma for dalaw 40522. First part of dalawlem13 40519. (Contributed by NM, 17-Sep-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem12 40518	Lemma for dalaw 40522. Second part of dalawlem13 40519. (Contributed by NM, 17-Sep-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem13 40519	Lemma for dalaw 40522. Special case to eliminate the requirement ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 in dalawlem1 40507. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem14 40520	Lemma for dalaw 40522. Combine dalawlem10 40516 and dalawlem13 40519. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem15 40521	Lemma for dalaw 40522. Swap variable triples 𝑃𝑄𝑅 and 𝑆𝑇𝑈 in dalawlem14 40520, to obtain the elimination of the remaining conditions in dalawlem1 40507. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalaw 40522	Desargues's law, derived from Desargues's theorem dath 40372 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 40523	Extend class notation with projective subspace closure.
class PCl
Definition	df-pclN 40524*	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 40571.) (Contributed by NM, 7-Sep-2013.)
⊢ PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))
Theorem	pclfvalN 40525*	The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝑈 = (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦}))
Theorem	pclvalN 40526*	Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦})
Theorem	pclclN 40527	Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	elpclN 40528*	Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑄 ∈ V    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑄 ∈ (𝑈‘𝑋) ↔ ∀𝑦 ∈ 𝑆 (𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦)))
Theorem	elpcliN 40529	Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆) ∧ 𝑄 ∈ (𝑈‘𝑋)) → 𝑄 ∈ 𝑌)
Theorem	pclssN 40530	Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘𝑋) ⊆ (𝑈‘𝑌))
Theorem	pclssidN 40531	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 40532	The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆) → (𝑈‘𝑋) = 𝑋)
Theorem	pclbtwnN 40533	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 40534	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 40535	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 40536*	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 40586. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
Theorem	pclcmpatN 40537*	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 40538	Extend class notation with polarity of projective subspace $m$.
class ⊥𝑃
Definition	df-polarityN 40539*	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 40540*	The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝)))))
Theorem	polvalN 40541*	Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝))))
Theorem	polval2N 40542	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 40543	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 40544	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 40545	The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴)
Theorem	pol1N 40546	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 40547	The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅)
Theorem	polpmapN 40548	The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋)))
Theorem	2polpmapN 40549	Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋))
Theorem	2polvalN 40550	Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋)))
Theorem	2polssN 40551	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 40552	Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆))
Theorem	polcon3N 40553	Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))
Theorem	2polcon4bN 40554	Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)))
Theorem	polcon2N 40555	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋))
Theorem	polcon2bN 40556	Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋)))
Theorem	pclss2polN 40557	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 40558	The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅)
Theorem	pcl0bN 40559	The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅))
Theorem	pmaplubN 40560	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 40561	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 40562	Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝑈 = (lub‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆)))
Theorem	paddunN 40563	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 6875.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇)))
Theorem	poldmj1N 40564	De Morgan's law for polarity of projective sum. (oldmj1 39857 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇)))
Theorem	pmapj2N 40565	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 40566	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 40567	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 40568	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 40569	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 40570	Extend class notation with set of all closed projective subspaces for a Hilbert lattice.
class PSubCl
Definition	df-psubclN 40571*	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 40572*	The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)})
Theorem	ispsubclN 40573	The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)))
Theorem	psubcliN 40574	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))
Theorem	psubcli2N 40575	Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)
Theorem	psubclsubN 40576	A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆)
Theorem	psubclssatN 40577	A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴)
Theorem	pmapidclN 40578	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 40579	The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶)
Theorem	1psubclN 40580	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 40581	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 40582	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 40583*	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 40584	The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶)
Theorem	paddatclN 40585	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 40586	The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 40536 and also pclcmpatN 40537. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑆 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	linepsubclN 40587	A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.)
⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶)
Theorem	polsubclN 40588	A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶)
Theorem	poml4N 40589	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 40590	Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋)))
Theorem	poml6N 40591	Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋)
Theorem	osumcllem1N 40592	Lemma for osumclN 40603. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀)
Theorem	osumcllem2N 40593	Lemma for osumclN 40603. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀))
Theorem	osumcllem3N 40594	Lemma for osumclN 40603. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌)
Theorem	osumcllem4N 40595	Lemma for osumclN 40603. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟)
Theorem	osumcllem5N 40596	Lemma for osumclN 40603. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem6N 40597	Lemma for osumclN 40603. Use atom exchange hlatexch1 40031 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem7N 40598*	Lemma for osumclN 40603. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌))
Theorem	osumcllem8N 40599	Lemma for osumclN 40603. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅)
Theorem	osumcllem9N 40600	Lemma for osumclN 40603. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    &   ⊢ 𝐶 = (PSubCl‘𝐾)    &   ⊢ 𝑀 = (𝑋 + {𝑝})    &   ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋)