P. 398 of Theorem List - Metamath Proof Explorer

Theorem List for Metamath Proof Explorer - 39701-39800   *Has distinct variable group(s)

Type	Label	Description
Statement
Theorem	dalem27 39701	Lemma for dath 39738. Show that the line 𝐺𝑃 intersects the dummy center of perspectivity 𝑐. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐺 ∨ 𝑃))
Theorem	dalem28 39702	Lemma for dath 39738. Lemma dalem27 39701 expressed differently. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑃 ≤ (𝐺 ∨ 𝑐))
Theorem	dalem29 39703	Lemma for dath 39738. Analogue of dalem23 39698 for 𝐻. (Contributed by NM, 2-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐻 ∈ 𝐴)
Theorem	dalem30 39704	Lemma for dath 39738. Analogue of dalem24 39699 for 𝐻. (Contributed by NM, 3-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐻 ≤ 𝑌)
Theorem	dalem31N 39705	Lemma for dath 39738. Analogue of dalem25 39700 for 𝐻. (Contributed by NM, 4-Aug-2012.) (New usage is discouraged.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≠ 𝐻)
Theorem	dalem32 39706	Lemma for dath 39738. Analogue of dalem27 39701 for 𝐻. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐻 ∨ 𝑄))
Theorem	dalem33 39707	Lemma for dath 39738. Analogue of dalem28 39702 for 𝐻. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑄 ≤ (𝐻 ∨ 𝑐))
Theorem	dalem34 39708	Lemma for dath 39738. Analogue of dalem23 39698 for 𝐼. (Contributed by NM, 2-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐼 ∈ 𝐴)
Theorem	dalem35 39709	Lemma for dath 39738. Analogue of dalem24 39699 for 𝐼. (Contributed by NM, 3-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐼 ≤ 𝑌)
Theorem	dalem36 39710	Lemma for dath 39738. Analogue of dalem27 39701 for 𝐼. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐼 ∨ 𝑅))
Theorem	dalem37 39711	Lemma for dath 39738. Analogue of dalem28 39702 for 𝐼. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑅 ≤ (𝐼 ∨ 𝑐))
Theorem	dalem38 39712	Lemma for dath 39738. Plane 𝑌 belongs to the 3-dimensional volume 𝐺𝐻𝐼𝑐. (Contributed by NM, 5-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑌 ≤ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∨ 𝑐))
Theorem	dalem39 39713	Lemma for dath 39738. Auxiliary atoms 𝐺, 𝐻, and 𝐼 are not colinear. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐻 ≤ (𝐼 ∨ 𝐺))
Theorem	dalem40 39714	Lemma for dath 39738. Analogue of dalem39 39713 for 𝐼. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐼 ≤ (𝐺 ∨ 𝐻))
Theorem	dalem41 39715	Lemma for dath 39738. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ≠ 𝐻)
Theorem	dalem42 39716	Lemma for dath 39738. Auxiliary atoms 𝐺𝐻𝐼 form a plane. (Contributed by NM, 4-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂)
Theorem	dalem43 39717	Lemma for dath 39738. Planes 𝐺𝐻𝐼 and 𝑌 are different. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌)
Theorem	dalem44 39718	Lemma for dath 39738. Dummy center of perspectivity 𝑐 lies outside of plane 𝐺𝐻𝐼. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ ((𝐺 ∨ 𝐻) ∨ 𝐼))
Theorem	dalem45 39719	Lemma for dath 39738. Dummy center of perspectivity 𝑐 is not on the line 𝐺𝐻. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻))
Theorem	dalem46 39720	Lemma for dath 39738. Analogue of dalem45 39719 for 𝐻𝐼. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐻 ∨ 𝐼))
Theorem	dalem47 39721	Lemma for dath 39738. Analogue of dalem45 39719 for 𝐼𝐺. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐼 ∨ 𝐺))
Theorem	dalem48 39722	Lemma for dath 39738. Analogue of dalem45 39719 for 𝑃𝑄. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑃 ∨ 𝑄))
Theorem	dalem49 39723	Lemma for dath 39738. Analogue of dalem45 39719 for 𝑄𝑅. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑄 ∨ 𝑅))
Theorem	dalem50 39724	Lemma for dath 39738. Analogue of dalem45 39719 for 𝑅𝑃. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑅 ∨ 𝑃))
Theorem	dalem51 39725	Lemma for dath 39738. Construct the condition 𝜑 with 𝑐, 𝐺𝐻𝐼, and 𝑌 in place of 𝐶, 𝑌, and 𝑍 respectively. This lets us reuse the special case of Desargues's theorem where 𝑌 ≠ 𝑍, to eventually prove the case where 𝑌 = 𝑍. (Contributed by NM, 16-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((((𝐾 ∈ HL ∧ 𝑐 ∈ 𝐴) ∧ (𝐺 ∈ 𝐴 ∧ 𝐻 ∈ 𝐴 ∧ 𝐼 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝑐 ≤ (𝐺 ∨ 𝐻) ∧ ¬ 𝑐 ≤ (𝐻 ∨ 𝐼) ∧ ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) ∧ (¬ 𝑐 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑐 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) ∧ (𝑐 ≤ (𝐺 ∨ 𝑃) ∧ 𝑐 ≤ (𝐻 ∨ 𝑄) ∧ 𝑐 ≤ (𝐼 ∨ 𝑅)))) ∧ ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌))
Theorem	dalem52 39726	Lemma for dath 39738. Lines 𝐺𝐻 and 𝑃𝑄 intersect at an atom. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴)
Theorem	dalem53 39727	Lemma for dath 39738. The auxiliary axis of perspectivity 𝐵 is a line (analogous to the actual axis of perspectivity 𝑋 in dalem15 39680. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑁 = (LLines‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐵 ∈ 𝑁)
Theorem	dalem54 39728	Lemma for dath 39738. Line 𝐺𝐻 intersects the auxiliary axis of perspectivity 𝐵. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ 𝐴)
Theorem	dalem55 39729	Lemma for dath 39738. Lines 𝐺𝐻 and 𝑃𝑄 intersect at the auxiliary line 𝐵 (later shown to be an axis of perspectivity; see dalem60 39734). (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) = ((𝐺 ∨ 𝐻) ∧ 𝐵))
Theorem	dalem56 39730	Lemma for dath 39738. Analogue of dalem55 39729 for line 𝑆𝑇. (Contributed by NM, 8-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑆 ∨ 𝑇)) = ((𝐺 ∨ 𝐻) ∧ 𝐵))
Theorem	dalem57 39731	Lemma for dath 39738. Axis of perspectivity point 𝐷 is on the auxiliary line 𝐵. (Contributed by NM, 9-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐷 ≤ 𝐵)
Theorem	dalem58 39732	Lemma for dath 39738. Analogue of dalem57 39731 for 𝐸. (Contributed by NM, 10-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐸 ≤ 𝐵)
Theorem	dalem59 39733	Lemma for dath 39738. Analogue of dalem57 39731 for 𝐹. (Contributed by NM, 10-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐹 ≤ 𝐵)
Theorem	dalem60 39734	Lemma for dath 39738. 𝐵 is an axis of perspectivity (almost). (Contributed by NM, 11-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆))    &   ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇))    &   ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈))    &   ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌)    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐷 ∨ 𝐸) = 𝐵)
Theorem	dalem61 39735	Lemma for dath 39738. Show that atoms 𝐷, 𝐸, and 𝐹 lie on the same line (axis of perspectivity). Eliminate hypotheses containing dummy atoms 𝑐 and 𝑑. (Contributed by NM, 11-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑))))    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐹 ≤ (𝐷 ∨ 𝐸))
Theorem	dalem62 39736	Lemma for dath 39738. Eliminate the condition 𝜓 containing dummy variables 𝑐 and 𝑑. (Contributed by NM, 11-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))    ⇒   ⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝐹 ≤ (𝐷 ∨ 𝐸))
Theorem	dalem63 39737	Lemma for dath 39738. Combine the cases where 𝑌 and 𝑍 are different planes with the case where 𝑌 and 𝑍 are the same plane. (Contributed by NM, 11-Aug-2012.)
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))))    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅)    &   ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))    ⇒   ⊢ (𝜑 → 𝐹 ≤ (𝐷 ∨ 𝐸))
Theorem	dath 39738	Desargues's theorem of projective geometry (proved for a Hilbert lattice). Assume each triple of atoms (points) 𝑃𝑄𝑅 and 𝑆𝑇𝑈 forms a triangle (i.e. determines a plane). Assume that lines 𝑃𝑆, 𝑄𝑇, and 𝑅𝑈 meet at a "center of perspectivity" 𝐶. (We also assume that 𝐶 is not on any of the 6 lines forming the two triangles.) Then the atoms 𝐷 = (𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇), 𝐸 = (𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈), 𝐹 = (𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆) are colinear, forming an "axis of perspectivity". Our proof roughly follows Theorem 2.7.1, p. 78 in Beutelspacher and Rosenbaum, Projective Geometry: From Foundations to Applications, Cambridge University Press (1988). Unlike them, we do not assume that 𝐶 is an atom to make this theorem slightly more general for easier future use. However, we prove that 𝐶 must be an atom in dalemcea 39662. For a visual demonstration, see the "Desargues's theorem" applet at http://www.dynamicgeometry.com/JavaSketchpad/Gallery.html 39662. The points I, J, and K there define the axis of perspectivity. See Theorems dalaw 39888 for Desargues's law, which eliminates all of the preconditions on the atoms except for central perspectivity. This is Metamath 100 proof #87. (Contributed by NM, 20-Aug-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → 𝐹 ≤ (𝐷 ∨ 𝐸))
Theorem	dath2 39739	Version of Desargues's theorem dath 39738 with a different variable ordering. (Contributed by NM, 7-Oct-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑂 = (LPlanes‘𝐾)    &   ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇))    &   ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈))    &   ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → 𝐷 ≤ (𝐸 ∨ 𝐹))
Theorem	lineset 39740*	The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})})
Theorem	isline 39741*	The predicate "is a line". (Contributed by NM, 19-Sep-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑁 ↔ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑋 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})))
Theorem	islinei 39742*	Condition implying "is a line". (Contributed by NM, 3-Feb-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ 𝑋 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑄 ∨ 𝑅)})) → 𝑋 ∈ 𝑁)
Theorem	pointsetN 39743*	The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (Points‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑃 = {𝑝 ∣ ∃𝑎 ∈ 𝐴 𝑝 = {𝑎}})
Theorem	ispointN 39744*	The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (Points‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝐴 𝑋 = {𝑎}))
Theorem	atpointN 39745	The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (Points‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴) → {𝑋} ∈ 𝑃)
Theorem	psubspset 39746*	The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → 𝑆 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑠))})
Theorem	ispsubsp 39747*	The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ 𝑋 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑋))))
Theorem	ispsubsp2 39748*	The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝐴 (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑝 ≤ (𝑞 ∨ 𝑟) → 𝑝 ∈ 𝑋))))
Theorem	psubspi 39749*	Property of a projective subspace. (Contributed by NM, 13-Jan-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑃 ≤ (𝑞 ∨ 𝑟)) → 𝑃 ∈ 𝑋)
Theorem	psubspi2N 39750	Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑃 ∈ 𝑋)
Theorem	0psubN 39751	The empty set is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.)
⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → ∅ ∈ 𝑆)
Theorem	snatpsubN 39752	The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → {𝑃} ∈ 𝑆)
Theorem	pointpsubN 39753	A point (singleton of an atom) is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.)
⊢ 𝑃 = (Points‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝑃) → 𝑋 ∈ 𝑆)
Theorem	linepsubN 39754	A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.)
⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝑆)
Theorem	atpsubN 39755	The set of all atoms is a projective subspace. Remark below Definition 15.1 of [MaedaMaeda] p. 61. (Contributed by NM, 13-Oct-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝑉 → 𝐴 ∈ 𝑆)
Theorem	psubssat 39756	A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ⊆ 𝐴)
Theorem	psubatN 39757	A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋) → 𝑌 ∈ 𝐴)
Theorem	pmapfval 39758*	The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐶 → 𝑀 = (𝑥 ∈ 𝐵 ↦ {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥}))
Theorem	pmapval 39759*	Value of the projective map of a Hilbert lattice. Definition in Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 2-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) = {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑋})
Theorem	elpmap 39760	Member of a projective map. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∈ (𝑀‘𝑋) ↔ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋)))
Theorem	pmapssat 39761	The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴)
Theorem	pmapssbaN 39762	A weakening of pmapssat 39761 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐵)
Theorem	pmaple 39763	The projective map of a Hilbert lattice preserves ordering. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ (𝑀‘𝑋) ⊆ (𝑀‘𝑌)))
Theorem	pmap11 39764	The projective map of a Hilbert lattice is one-to-one. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑀‘𝑋) = (𝑀‘𝑌) ↔ 𝑋 = 𝑌))
Theorem	pmapat 39765	The projective map of an atom. (Contributed by NM, 25-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑀‘𝑃) = {𝑃})
Theorem	elpmapat 39766	Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ (𝑀‘𝑃) ↔ 𝑋 = 𝑃))
Theorem	pmap0 39767	Value of the projective map of a Hilbert lattice at lattice zero. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
⊢ 0 = (0.‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ AtLat → (𝑀‘ 0 ) = ∅)
Theorem	pmapeq0 39768	A projective map value is zero iff its argument is lattice zero. (Contributed by NM, 27-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) = ∅ ↔ 𝑋 = 0 ))
Theorem	pmap1N 39769	Value of the projective map of a Hilbert lattice at lattice unity. Part of Theorem 15.5.1 of [MaedaMaeda] p. 62. (Contributed by NM, 22-Oct-2011.) (New usage is discouraged.)
⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ OP → (𝑀‘ 1 ) = 𝐴)
Theorem	pmapsub 39770	The projective map of a Hilbert lattice maps to projective subspaces. Part of Theorem 15.5 of [MaedaMaeda] p. 62. (Contributed by NM, 17-Oct-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝑆 = (PSubSp‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ 𝑆)
Theorem	pmapglbx 39771*	The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb 39772, where we read 𝑆 as 𝑆(𝑖). Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆))
Theorem	pmapglb 39772*	The projective map of the GLB of a set of lattice elements 𝑆. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵 ∧ 𝑆 ≠ ∅) → (𝑀‘(𝐺‘𝑆)) = ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥))
Theorem	pmapglb2N 39773*	The projective map of the GLB of a set of lattice elements 𝑆. Variant of Theorem 15.5.2 of [MaedaMaeda] p. 62. Allows 𝑆 = ∅. (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝑀‘(𝐺‘𝑆)) = (𝐴 ∩ ∩ 𝑥 ∈ 𝑆 (𝑀‘𝑥)))
Theorem	pmapglb2xN 39774*	The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N 39773, where we read 𝑆 as 𝑆(𝑖). Extension of Theorem 15.5.2 of [MaedaMaeda] p. 62 that allows 𝐼 = ∅. (Contributed by NM, 21-Jan-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐺 = (glb‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = (𝐴 ∩ ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆)))
Theorem	pmapmeet 39775	The projective map of a meet. (Contributed by NM, 25-Jan-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑃 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑃‘(𝑋 ∧ 𝑌)) = ((𝑃‘𝑋) ∩ (𝑃‘𝑌)))
Theorem	isline2 39776*	Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (𝐾 ∈ Lat → (𝑋 ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑀‘(𝑝 ∨ 𝑞)))))
Theorem	linepmap 39777	A line described with a projective map. (Contributed by NM, 3-Feb-2012.)
⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑀‘(𝑃 ∨ 𝑄)) ∈ 𝑁)
Theorem	isline3 39778*	Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑝 ∨ 𝑞))))
Theorem	isline4N 39779*	Definition of line in terms of original lattice elements. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 𝑝𝐶𝑋))
Theorem	lneq2at 39780	A line equals the join of any two of its distinct points (atoms). (Contributed by NM, 29-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑀‘𝑋) ∈ 𝑁) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑋)) → 𝑋 = (𝑃 ∨ 𝑄))
Theorem	lnatexN 39781*	There is an atom in a line different from any other. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ (𝑀‘𝑋) ∈ 𝑁) → ∃𝑞 ∈ 𝐴 (𝑞 ≠ 𝑃 ∧ 𝑞 ≤ 𝑋))
Theorem	lnjatN 39782*	Given an atom in a line, there is another atom which when joined equals the line. (Contributed by NM, 30-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → ∃𝑞 ∈ 𝐴 (𝑞 ≠ 𝑃 ∧ 𝑋 = (𝑃 ∨ 𝑞)))
Theorem	lncvrelatN 39783	A lattice element covered by a line is an atom. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃𝐶𝑋)) → 𝑃 ∈ 𝐴)
Theorem	lncvrat 39784	A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → 𝑃𝐶𝑋)
Theorem	lncmp 39785	If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝑀 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ (𝑀‘𝑌) ∈ 𝑁)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌))
Theorem	2lnat 39786	Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐹‘𝑋) ∈ 𝑁 ∧ (𝐹‘𝑌) ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴)
Theorem	2atm2atN 39787	Two joins with a common atom have a nonzero meet. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.)
⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) ≠ 0 )
Theorem	2llnma1b 39788	Generalization of 2llnma1 39789. (Contributed by NM, 26-Apr-2013.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃)
Theorem	2llnma1 39789	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 11-Oct-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → ((𝑄 ∨ 𝑃) ∧ (𝑄 ∨ 𝑅)) = 𝑄)
Theorem	2llnma3r 39790	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 30-Apr-2013.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ∨ 𝑅) ≠ (𝑄 ∨ 𝑅)) → ((𝑃 ∨ 𝑅) ∧ (𝑄 ∨ 𝑅)) = 𝑅)
Theorem	2llnma2 39791	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 28-May-2012.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑅 ∨ 𝑃) ∧ (𝑅 ∨ 𝑄)) = 𝑅)
Theorem	2llnma2rN 39792	Two different intersecting lines (expressed in terms of atoms) meet at their common point (atom). (Contributed by NM, 2-May-2013.) (New usage is discouraged.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑅) ∧ (𝑄 ∨ 𝑅)) = 𝑅)
21.28.13  Construction of a vector space from a Hilbert lattice
Theorem	cdlema1N 39793	A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 29-Apr-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ 𝑁 = (Lines‘𝐾)    &   ⊢ 𝐹 = (pmap‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ 𝑄 ≤ 𝑌) ∧ ((𝐹‘𝑌) ∈ 𝑁 ∧ (𝑋 ∧ 𝑌) ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑋 ∨ 𝑅) = (𝑋 ∨ 𝑌))
Theorem	cdlema2N 39794	A condition for required for proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 9-May-2012.) (New usage is discouraged.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 0 = (0.‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ((𝑅 ≠ 𝑃 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋))) → (𝑅 ∧ 𝑋) = 0 )
Theorem	cdlemblem 39795	Lemma for cdlemb 39796. (Contributed by NM, 8-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ < = (lt‘𝐾)    &   ⊢ ∧ = (meet‘𝐾)    &   ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑋)    ⇒   ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ (𝑃 ∨ 𝑢)))) → (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Theorem	cdlemb 39796*	Given two atoms not less than or equal to an element covered by 1, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 8-May-2012.)
⊢ 𝐵 = (Base‘𝐾)    &   ⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 1 = (1.‘𝐾)    &   ⊢ 𝐶 = ( ⋖ ‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    ⇒   ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄)))
Syntax	cpadd 39797	Extend class notation with projective subspace sum.
class +𝑃
Definition	df-padd 39798*	Define projective sum of two subspaces (or more generally two sets of atoms), which is the union of all lines generated by pairs of atoms from each subspace. Lemma 16.2 of [MaedaMaeda] p. 68. For convenience, our definition is generalized to apply to empty sets. (Contributed by NM, 29-Dec-2011.)
⊢ +𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙), 𝑛 ∈ 𝒫 (Atoms‘𝑙) ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ (Atoms‘𝑙) ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝(le‘𝑙)(𝑞(join‘𝑙)𝑟)})))
Theorem	paddfval 39799*	Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)})))
Theorem	paddval 39800*	Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.)
⊢ ≤ = (le‘𝐾)    &   ⊢ ∨ = (join‘𝐾)    &   ⊢ 𝐴 = (Atoms‘𝐾)    &   ⊢ + = (+𝑃‘𝐾)    ⇒   ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}))