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
Theorem	paddcom 40401	Projective subspace sum commutes. (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = (𝑌 + 𝑋))
Theorem	paddssat 40402	A projective subspace sum is a set of atoms. (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) ⊆ 𝐴)
Theorem	sspadd1 40403	A projective subspace sum is a superset of its first summand. (ssun1 4130 analog.) (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑋 + 𝑌))
Theorem	sspadd2 40404	A projective subspace sum is a superset of its second summand. (ssun2 4131 analog.) (Contributed by NM, 3-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → 𝑋 ⊆ (𝑌 + 𝑋))
Theorem	paddss1 40405	Subset law for projective subspace sum. (unss1 4137 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑍)))
Theorem	paddss2 40406	Subset law for projective subspace sum. (unss2 4139 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) → (𝑋 ⊆ 𝑌 → (𝑍 + 𝑋) ⊆ (𝑍 + 𝑌)))
Theorem	paddss12 40407	Subset law for projective subspace sum. (unss12 4140 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ 𝑍 ⊆ 𝑊) → (𝑋 + 𝑍) ⊆ (𝑌 + 𝑊)))
Theorem	paddasslem1 40408	Lemma for paddass 40426. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ 𝑥 ≠ 𝑦) ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦)) → ¬ 𝑥 ≤ (𝑟 ∨ 𝑦))
Theorem	paddasslem2 40409	Lemma for paddass 40426. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → 𝑧 ≤ (𝑟 ∨ 𝑦))
Theorem	paddasslem3 40410*	Lemma for paddass 40426. Restate projective space axiom ps-2 40066. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑥 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) → (((¬ 𝑥 ≤ (𝑟 ∨ 𝑦) ∧ 𝑝 ≠ 𝑧) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑧 ≤ (𝑟 ∨ 𝑦))) → ∃𝑠 ∈ 𝐴 (𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))))
Theorem	paddasslem4 40411*	Lemma for paddass 40426. Combine paddasslem1 40408, paddasslem2 40409, and paddasslem3 40410. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴) ∧ (𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦 ∧ ¬ 𝑟 ≤ (𝑥 ∨ 𝑦))) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧))) → ∃𝑠 ∈ 𝐴 (𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧)))
Theorem	paddasslem5 40412	Lemma for paddass 40426. Show 𝑠 ≠ 𝑧 by contradiction. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑟 ∈ 𝐴 ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦))) → 𝑠 ≠ 𝑧)
Theorem	paddasslem6 40413	Lemma for paddass 40426. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ 𝑧 ∈ 𝐴) ∧ (𝑠 ≠ 𝑧 ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) → 𝑝 ≤ (𝑠 ∨ 𝑧))
Theorem	paddasslem7 40414	Lemma for paddass 40426. Combine paddasslem5 40412 and paddasslem6 40413. (Contributed by NM, 9-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴) ∧ (𝑥 ∈ 𝐴 ∧ 𝑦 ∈ 𝐴 ∧ 𝑧 ∈ 𝐴)) ∧ ((¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦)) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧))) → 𝑝 ≤ (𝑠 ∨ 𝑧))
Theorem	paddasslem8 40415	Lemma for paddass 40426. (Contributed by NM, 8-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑠 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ 𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑠 ∨ 𝑧))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem9 40416	Lemma for paddass 40426. Combine paddasslem7 40414 and paddasslem8 40415. (Contributed by NM, 9-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)) ∧ (𝑠 ∈ 𝐴 ∧ 𝑠 ≤ (𝑥 ∨ 𝑦) ∧ 𝑠 ≤ (𝑝 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem10 40417	Lemma for paddass 40426. Use paddasslem4 40411 to eliminate 𝑠 from paddasslem9 40416. (Contributed by NM, 9-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧 ∧ 𝑥 ≠ 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (¬ 𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem11 40418	Lemma for paddass 40426. The case when 𝑝 = 𝑧. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 = 𝑧) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) ∧ 𝑧 ∈ 𝑍) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem12 40419	Lemma for paddass 40426. The case when 𝑥 = 𝑦. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑥 = 𝑦) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem13 40420	Lemma for paddass 40426. The case when 𝑟 ≤ (𝑥 ∨ 𝑦). (Unlike the proof in Maeda and Maeda, we don't need 𝑥 ≠ 𝑦.) (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑝 ≠ 𝑧) ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌) ∧ (𝑟 ≤ (𝑥 ∨ 𝑦) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem14 40421	Lemma for paddass 40426. Remove 𝑝 ≠ 𝑧, 𝑥 ≠ 𝑦, and ¬ 𝑟 ≤ (𝑥 ∨ 𝑦) from antecedent of paddasslem10 40417, using paddasslem11 40418, paddasslem12 40419, and paddasslem13 40420. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑝 ∈ 𝐴 ∧ 𝑟 ∈ 𝐴)) ∧ ((𝑥 ∈ 𝑋 ∧ 𝑦 ∈ 𝑌 ∧ 𝑧 ∈ 𝑍) ∧ (𝑝 ≤ (𝑥 ∨ 𝑟) ∧ 𝑟 ≤ (𝑦 ∨ 𝑧)))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem15 40422	Lemma for paddass 40426. Use elpaddn0 40388 to eliminate 𝑦 and 𝑧 from paddasslem14 40421. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅)) ∧ (𝑝 ∈ 𝐴 ∧ (𝑥 ∈ 𝑋 ∧ 𝑟 ∈ (𝑌 + 𝑍)) ∧ 𝑝 ≤ (𝑥 ∨ 𝑟))) → 𝑝 ∈ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem16 40423	Lemma for paddass 40426. Use elpaddn0 40388 to eliminate 𝑥 and 𝑟 from paddasslem15 40422. (Contributed by NM, 11-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem17 40424	Lemma for paddass 40426. The case when at least one sum argument is empty. (Contributed by NM, 12-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴) ∧ ¬ ((𝑋 ≠ ∅ ∧ (𝑌 + 𝑍) ≠ ∅) ∧ (𝑌 ≠ ∅ ∧ 𝑍 ≠ ∅))) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddasslem18 40425	Lemma for paddass 40426. Combine paddasslem16 40423 and paddasslem17 40424. (Contributed by NM, 12-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) ⊆ ((𝑋 + 𝑌) + 𝑍))
Theorem	paddass 40426	Projective subspace sum is associative. Equation 16.2.1 of [MaedaMaeda] p. 68. In our version, the subspaces do not have to be nonempty. (Contributed by NM, 29-Dec-2011.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) + 𝑍) = (𝑋 + (𝑌 + 𝑍)))
Theorem	padd12N 40427	Commutative/associative law for projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 + (𝑌 + 𝑍)) = (𝑌 + (𝑋 + 𝑍)))
Theorem	padd4N 40428	Rearrangement of 4 terms in a projective subspace sum. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ⊆ 𝐴 ∧ 𝑊 ⊆ 𝐴)) → ((𝑋 + 𝑌) + (𝑍 + 𝑊)) = ((𝑋 + 𝑍) + (𝑌 + 𝑊)))
Theorem	paddidm 40429	Projective subspace sum is idempotent. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 13-Jan-2012.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → (𝑋 + 𝑋) = 𝑋)
Theorem	paddclN 40430	The projective sum of two subspaces is a subspace. Part of Lemma 16.2 of [MaedaMaeda] p. 68. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑋 + 𝑌) ∈ 𝑆)
Theorem	paddssw1 40431	Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍) → (𝑋 + 𝑌) ⊆ (𝑍 + 𝑍)))
Theorem	paddssw2 40432	Subset law for projective subspace sum valid for all subsets of atoms. (Contributed by NM, 14-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → ((𝑋 + 𝑌) ⊆ 𝑍 → (𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍)))
Theorem	paddss 40433	Subset law for projective subspace sum. (unss 4142 analog.) (Contributed by NM, 7-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆)) → ((𝑋 ⊆ 𝑍 ∧ 𝑌 ⊆ 𝑍) ↔ (𝑋 + 𝑌) ⊆ 𝑍))
Theorem	pmodlem1 40434*	Lemma for pmod1i 40436. (Contributed by NM, 9-Mar-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑍 ∈ 𝑆 ∧ 𝑋 ⊆ 𝑍 ∧ 𝑝 ∈ 𝑍) ∧ (𝑞 ∈ 𝑋 ∧ 𝑟 ∈ 𝑌 ∧ 𝑝 ≤ (𝑞 ∨ 𝑟))) → 𝑝 ∈ (𝑋 + (𝑌 ∩ 𝑍)))
Theorem	pmodlem2 40435	Lemma for pmod1i 40436. (Contributed by NM, 9-Mar-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆) ∧ 𝑋 ⊆ 𝑍) → ((𝑋 + 𝑌) ∩ 𝑍) ⊆ (𝑋 + (𝑌 ∩ 𝑍)))
Theorem	pmod1i 40436	The modular law holds in a projective subspace. (Contributed by NM, 10-Mar-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ∈ 𝑆)) → (𝑋 ⊆ 𝑍 → ((𝑋 + 𝑌) ∩ 𝑍) = (𝑋 + (𝑌 ∩ 𝑍))))
Theorem	pmod2iN 40437	Dual of the modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑍 ⊆ 𝑋 → ((𝑋 ∩ 𝑌) + 𝑍) = (𝑋 ∩ (𝑌 + 𝑍))))
Theorem	pmodN 40438	The modular law for projective subspaces. (Contributed by NM, 26-Mar-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑆 ∧ 𝑌 ⊆ 𝐴 ∧ 𝑍 ⊆ 𝐴)) → (𝑋 ∩ (𝑌 + (𝑋 ∩ 𝑍))) = ((𝑋 ∩ 𝑌) + (𝑋 ∩ 𝑍)))
Theorem	pmodl42N 40439	Lemma derived from modular law. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) ∧ (𝑍 ∈ 𝑆 ∧ 𝑊 ∈ 𝑆)) → (((𝑋 + 𝑌) + 𝑍) ∩ ((𝑋 + 𝑌) + 𝑊)) = ((𝑋 + 𝑌) + ((𝑋 + 𝑍) ∩ (𝑌 + 𝑊))))
Theorem	pmapjoin 40440	The projective map of the join of two lattice elements. Part of Equation 15.5.3 of [MaedaMaeda] p. 63. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑀‘𝑋) + (𝑀‘𝑌)) ⊆ (𝑀‘(𝑋 ∨ 𝑌)))
Theorem	pmapjat1 40441	The projective map of the join of a lattice element and an atom. (Contributed by NM, 28-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴) → (𝑀‘(𝑋 ∨ 𝑄)) = ((𝑀‘𝑋) + (𝑀‘𝑄)))
Theorem	pmapjat2 40442	The projective map of the join of an atom with a lattice element. (Contributed by NM, 12-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴) → (𝑀‘(𝑄 ∨ 𝑋)) = ((𝑀‘𝑄) + (𝑀‘𝑋)))
Theorem	pmapjlln1 40443	The projective map of the join of a lattice element and a lattice line (expressed as the join 𝑄 ∨ 𝑅 of two atoms). (Contributed by NM, 16-Sep-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑀‘(𝑋 ∨ (𝑄 ∨ 𝑅))) = ((𝑀‘𝑋) + (𝑀‘(𝑄 ∨ 𝑅))))
Theorem	hlmod1i 40444	A version of the modular law pmod1i 40436 that holds in a Hilbert lattice. (Contributed by NM, 13-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ≤ 𝑍 ∧ (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) + (𝐹‘𝑌))) → ((𝑋 ∨ 𝑌) ∧ 𝑍) = (𝑋 ∨ (𝑌 ∧ 𝑍))))
Theorem	atmod1i1 40445	Version of modular law pmod1i 40436 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 11-May-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑌) → (𝑃 ∨ (𝑋 ∧ 𝑌)) = ((𝑃 ∨ 𝑋) ∧ 𝑌))
Theorem	atmod1i1m 40446	Version of modular law pmod1i 40436 that holds in a Hilbert lattice, when an element meets an atom. (Contributed by NM, 2-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ∧ 𝑃) ≤ 𝑍) → ((𝑋 ∧ 𝑃) ∨ (𝑌 ∧ 𝑍)) = (((𝑋 ∧ 𝑃) ∨ 𝑌) ∧ 𝑍))
Theorem	atmod1i2 40447	Version of modular law pmod1i 40436 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → (𝑋 ∨ (𝑃 ∧ 𝑌)) = ((𝑋 ∨ 𝑃) ∧ 𝑌))
Theorem	llnmod1i2 40448	Version of modular law pmod1i 40436 that holds in a Hilbert lattice, when one element is a lattice line (expressed as the join 𝑃 ∨ 𝑄). (Contributed by NM, 16-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑋 ≤ 𝑌) → (𝑋 ∨ ((𝑃 ∨ 𝑄) ∧ 𝑌)) = ((𝑋 ∨ (𝑃 ∨ 𝑄)) ∧ 𝑌))
Theorem	atmod2i1 40449	Version of modular law pmod2iN 40437 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → ((𝑋 ∧ 𝑌) ∨ 𝑃) = (𝑋 ∧ (𝑌 ∨ 𝑃)))
Theorem	atmod2i2 40450	Version of modular law pmod2iN 40437 that holds in a Hilbert lattice, when one element is an atom. (Contributed by NM, 14-May-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 ≤ 𝑋) → ((𝑋 ∧ 𝑃) ∨ 𝑌) = (𝑋 ∧ (𝑃 ∨ 𝑌)))
Theorem	llnmod2i2 40451	Version of modular law pmod1i 40436 that holds in a Hilbert lattice, when one element is a lattice line (expressed as the join 𝑃 ∨ 𝑄). (Contributed by NM, 16-Sep-2012.) (Revised by Mario Carneiro, 10-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑌 ≤ 𝑋) → ((𝑋 ∧ (𝑃 ∨ 𝑄)) ∨ 𝑌) = (𝑋 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑌)))
Theorem	atmod3i1 40452	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-May-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑃 ≤ 𝑋) → (𝑃 ∨ (𝑋 ∧ 𝑌)) = (𝑋 ∧ (𝑃 ∨ 𝑌)))
Theorem	atmod3i2 40453	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 40454	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 40455	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 40456	Lemma for llnexchb2 40457. (Contributed by NM, 17-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑋) ∧ (𝑋 ∧ 𝑌) ∈ 𝐴) → ((𝑋 ∧ 𝑌) ≤ (𝑃 ∨ 𝑄) ↔ (𝑋 ∧ 𝑌) = (𝑋 ∧ (𝑃 ∨ 𝑄))))
Theorem	llnexchb2 40457	Line exchange property (compare cvlatexchb2 39923 for atoms). (Contributed by NM, 17-Nov-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁) ∧ ((𝑋 ∧ 𝑌) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍)) → ((𝑋 ∧ 𝑌) ≤ 𝑍 ↔ (𝑋 ∧ 𝑌) = (𝑋 ∧ 𝑍)))
Theorem	llnexch2N 40458	Line exchange property (compare cvlatexch2 39925 for atoms). (Contributed by NM, 18-Nov-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑍 ∈ 𝑁) ∧ ((𝑋 ∧ 𝑌) ∈ 𝐴 ∧ 𝑋 ≠ 𝑍)) → ((𝑋 ∧ 𝑌) ≤ 𝑍 → (𝑋 ∧ 𝑍) ≤ 𝑌))
Theorem	dalawlem1 40459	Lemma for dalaw 40474. Special case of dath2 40325, where 𝐶 is replaced by ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)). The remaining lemmas will eliminate the conditions on the atoms imposed by dath2 40325. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) ∧ ((¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃)) ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆)) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈))) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem2 40460	Lemma for dalaw 40474. Utility lemma that breaks ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) into a join of two pieces. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ ((((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ∨ (((𝑃 ∨ 𝑄) ∨ 𝑆) ∧ 𝑇)))
Theorem	dalawlem3 40461	Lemma for dalaw 40474. First piece of dalawlem5 40463. (Contributed by NM, 4-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑄 ∨ 𝑇) ∨ 𝑃) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem4 40462	Lemma for dalaw 40474. Second piece of dalawlem5 40463. (Contributed by NM, 4-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∨ 𝑄) ∧ 𝑇) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem5 40463	Lemma for dalaw 40474. Special case to eliminate the requirement ¬ (𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) in dalawlem1 40459. (Contributed by NM, 4-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem6 40464	Lemma for dalaw 40474. First piece of dalawlem8 40466. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑇) ∧ 𝑆) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem7 40465	Lemma for dalaw 40474. Second piece of dalawlem8 40466. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑄) ∨ 𝑆) ∧ 𝑇) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem8 40466	Lemma for dalaw 40474. Special case to eliminate the requirement ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) in dalawlem1 40459. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem9 40467	Lemma for dalaw 40474. Special case to eliminate the requirement ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃) in dalawlem1 40459. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem10 40468	Lemma for dalaw 40474. Combine dalawlem5 40463, dalawlem8 40466, and dalawlem9 . (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃)) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem11 40469	Lemma for dalaw 40474. First part of dalawlem13 40471. (Contributed by NM, 17-Sep-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem12 40470	Lemma for dalaw 40474. Second part of dalawlem13 40471. (Contributed by NM, 17-Sep-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑄 = 𝑅 ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem13 40471	Lemma for dalaw 40474. Special case to eliminate the requirement ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 in dalawlem1 40459. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem14 40472	Lemma for dalaw 40474. Combine dalawlem10 40468 and dalawlem13 40471. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑃 ∨ 𝑄) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑄 ∨ 𝑅) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑃))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalawlem15 40473	Lemma for dalaw 40474. Swap variable triples 𝑃𝑄𝑅 and 𝑆𝑇𝑈 in dalawlem14 40472, to obtain the elimination of the remaining conditions in dalawlem1 40459. (Contributed by NM, 6-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))
Theorem	dalaw 40474	Desargues's law, derived from Desargues's theorem dath 40324 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 40475	Extend class notation with projective subspace closure.
class PCl
Definition	df-pclN 40476*	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 40523.) (Contributed by NM, 7-Sep-2013.)
⊢ PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦}))
Theorem	pclfvalN 40477*	The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝑈 = (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦}))
Theorem	pclvalN 40478*	Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦})
Theorem	pclclN 40479	Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆)
Theorem	elpclN 40480*	Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    &   ⊢ 𝑄 ∈ V    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑄 ∈ (𝑈‘𝑋) ↔ ∀𝑦 ∈ 𝑆 (𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦)))
Theorem	elpcliN 40481	Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆) ∧ 𝑄 ∈ (𝑈‘𝑋)) → 𝑄 ∈ 𝑌)
Theorem	pclssN 40482	Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘𝑋) ⊆ (𝑈‘𝑌))
Theorem	pclssidN 40483	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 40484	The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆) → (𝑈‘𝑋) = 𝑋)
Theorem	pclbtwnN 40485	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 40486	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 40487	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 40488*	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 40538. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑈 = (PCl‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦))
Theorem	pclcmpatN 40489*	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 40490	Extend class notation with polarity of projective subspace $m$.
class ⊥𝑃
Definition	df-polarityN 40491*	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 40492*	The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝)))))
Theorem	polvalN 40493*	Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.)
⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝))))
Theorem	polval2N 40494	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 40495	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 40496	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 40497	The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴)
Theorem	pol1N 40498	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 40499	The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.)
⊢ ⊥ = (⊥𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅)
Theorem	polpmapN 40500	The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ⊥ = (oc‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    &   ⊢ 𝑃 = (⊥𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋)))