![]() |
Metamath
Proof Explorer Theorem List (p. 395 of 486) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30851) |
![]() (30852-32374) |
![]() (32375-48553) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dalem30 39401 | Lemma for dath 39435. Analogue of dalem24 39396 for 𝐻. (Contributed by NM, 3-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐻 ≤ 𝑌) | ||
Theorem | dalem31N 39402 | Lemma for dath 39435. Analogue of dalem25 39397 for 𝐻. (Contributed by NM, 4-Aug-2012.) (New usage is discouraged.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≠ 𝐻) | ||
Theorem | dalem32 39403 | Lemma for dath 39435. Analogue of dalem27 39398 for 𝐻. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐻 ∨ 𝑄)) | ||
Theorem | dalem33 39404 | Lemma for dath 39435. Analogue of dalem28 39399 for 𝐻. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑄 ≤ (𝐻 ∨ 𝑐)) | ||
Theorem | dalem34 39405 | Lemma for dath 39435. Analogue of dalem23 39395 for 𝐼. (Contributed by NM, 2-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐼 ∈ 𝐴) | ||
Theorem | dalem35 39406 | Lemma for dath 39435. Analogue of dalem24 39396 for 𝐼. (Contributed by NM, 3-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐼 ≤ 𝑌) | ||
Theorem | dalem36 39407 | Lemma for dath 39435. Analogue of dalem27 39398 for 𝐼. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐼 ∨ 𝑅)) | ||
Theorem | dalem37 39408 | Lemma for dath 39435. Analogue of dalem28 39399 for 𝐼. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑅 ≤ (𝐼 ∨ 𝑐)) | ||
Theorem | dalem38 39409 | Lemma for dath 39435. Plane 𝑌 belongs to the 3-dimensional volume 𝐺𝐻𝐼𝑐. (Contributed by NM, 5-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑌 ≤ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∨ 𝑐)) | ||
Theorem | dalem39 39410 | Lemma for dath 39435. Auxiliary atoms 𝐺, 𝐻, and 𝐼 are not colinear. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐻 ≤ (𝐼 ∨ 𝐺)) | ||
Theorem | dalem40 39411 | Lemma for dath 39435. Analogue of dalem39 39410 for 𝐼. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐼 ≤ (𝐺 ∨ 𝐻)) | ||
Theorem | dalem41 39412 | Lemma for dath 39435. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ≠ 𝐻) | ||
Theorem | dalem42 39413 | Lemma for dath 39435. Auxiliary atoms 𝐺𝐻𝐼 form a plane. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂) | ||
Theorem | dalem43 39414 | Lemma for dath 39435. Planes 𝐺𝐻𝐼 and 𝑌 are different. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌) | ||
Theorem | dalem44 39415 | Lemma for dath 39435. Dummy center of perspectivity 𝑐 lies outside of plane 𝐺𝐻𝐼. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ ((𝐺 ∨ 𝐻) ∨ 𝐼)) | ||
Theorem | dalem45 39416 | Lemma for dath 39435. Dummy center of perspectivity 𝑐 is not on the line 𝐺𝐻. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻)) | ||
Theorem | dalem46 39417 | Lemma for dath 39435. Analogue of dalem45 39416 for 𝐻𝐼. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐻 ∨ 𝐼)) | ||
Theorem | dalem47 39418 | Lemma for dath 39435. Analogue of dalem45 39416 for 𝐼𝐺. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) | ||
Theorem | dalem48 39419 | Lemma for dath 39435. Analogue of dalem45 39416 for 𝑃𝑄. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | dalem49 39420 | Lemma for dath 39435. Analogue of dalem45 39416 for 𝑄𝑅. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑄 ∨ 𝑅)) | ||
Theorem | dalem50 39421 | Lemma for dath 39435. Analogue of dalem45 39416 for 𝑅𝑃. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) | ||
Theorem | dalem51 39422 | Lemma for dath 39435. 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 39423 | Lemma for dath 39435. Lines 𝐺𝐻 and 𝑃𝑄 intersect at an atom. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴) | ||
Theorem | dalem53 39424 | Lemma for dath 39435. The auxiliary axis of perspectivity 𝐵 is a line (analogous to the actual axis of perspectivity 𝑋 in dalem15 39377. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐵 ∈ 𝑁) | ||
Theorem | dalem54 39425 | Lemma for dath 39435. Line 𝐺𝐻 intersects the auxiliary axis of perspectivity 𝐵. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ 𝐴) | ||
Theorem | dalem55 39426 | Lemma for dath 39435. Lines 𝐺𝐻 and 𝑃𝑄 intersect at the auxiliary line 𝐵 (later shown to be an axis of perspectivity; see dalem60 39431). (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) = ((𝐺 ∨ 𝐻) ∧ 𝐵)) | ||
Theorem | dalem56 39427 | Lemma for dath 39435. Analogue of dalem55 39426 for line 𝑆𝑇. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑆 ∨ 𝑇)) = ((𝐺 ∨ 𝐻) ∧ 𝐵)) | ||
Theorem | dalem57 39428 | Lemma for dath 39435. Axis of perspectivity point 𝐷 is on the auxiliary line 𝐵. (Contributed by NM, 9-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐷 ≤ 𝐵) | ||
Theorem | dalem58 39429 | Lemma for dath 39435. Analogue of dalem57 39428 for 𝐸. (Contributed by NM, 10-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐸 ≤ 𝐵) | ||
Theorem | dalem59 39430 | Lemma for dath 39435. Analogue of dalem57 39428 for 𝐹. (Contributed by NM, 10-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐹 ≤ 𝐵) | ||
Theorem | dalem60 39431 | Lemma for dath 39435. 𝐵 is an axis of perspectivity (almost). (Contributed by NM, 11-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐷 ∨ 𝐸) = 𝐵) | ||
Theorem | dalem61 39432 | Lemma for dath 39435. 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 39433 | Lemma for dath 39435. Eliminate the condition 𝜓 containing dummy variables 𝑐 and 𝑑. (Contributed by NM, 11-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝐹 ≤ (𝐷 ∨ 𝐸)) | ||
Theorem | dalem63 39434 | Lemma for dath 39435. 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 39435 |
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 39359. For a visual demonstration, see the "Desargues's theorem" applet at http://www.dynamicgeometry.com/JavaSketchpad/Gallery.html 39359. The points I, J, and K there define the axis of perspectivity. See Theorems dalaw 39585 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 39436 | Version of Desargues's theorem dath 39435 with a different variable ordering. (Contributed by NM, 7-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → 𝐷 ≤ (𝐸 ∨ 𝐹)) | ||
Theorem | lineset 39437* | The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) | ||
Theorem | isline 39438* | The predicate "is a line". (Contributed by NM, 19-Sep-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑁 ↔ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑋 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) | ||
Theorem | islinei 39439* | Condition implying "is a line". (Contributed by NM, 3-Feb-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ 𝑋 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑄 ∨ 𝑅)})) → 𝑋 ∈ 𝑁) | ||
Theorem | pointsetN 39440* | The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑃 = {𝑝 ∣ ∃𝑎 ∈ 𝐴 𝑝 = {𝑎}}) | ||
Theorem | ispointN 39441* | The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝐴 𝑋 = {𝑎})) | ||
Theorem | atpointN 39442 | The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴) → {𝑋} ∈ 𝑃) | ||
Theorem | psubspset 39443* | The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑆 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑠))}) | ||
Theorem | ispsubsp 39444* | The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ 𝑋 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑋)))) | ||
Theorem | ispsubsp2 39445* | The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝐴 (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑝 ≤ (𝑞 ∨ 𝑟) → 𝑝 ∈ 𝑋)))) | ||
Theorem | psubspi 39446* | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑃 ≤ (𝑞 ∨ 𝑟)) → 𝑃 ∈ 𝑋) | ||
Theorem | psubspi2N 39447 | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑃 ∈ 𝑋) | ||
Theorem | 0psubN 39448 | 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 39449 | The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → {𝑃} ∈ 𝑆) | ||
Theorem | pointpsubN 39450 | 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 39451 | A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝑆) | ||
Theorem | atpsubN 39452 | 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 39453 | A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ⊆ 𝐴) | ||
Theorem | psubatN 39454 | A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋) → 𝑌 ∈ 𝐴) | ||
Theorem | pmapfval 39455* | The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐶 → 𝑀 = (𝑥 ∈ 𝐵 ↦ {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥})) | ||
Theorem | pmapval 39456* | 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 39457 | Member of a projective map. (Contributed by NM, 27-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∈ (𝑀‘𝑋) ↔ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋))) | ||
Theorem | pmapssat 39458 | The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴) | ||
Theorem | pmapssbaN 39459 | A weakening of pmapssat 39458 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐵) | ||
Theorem | pmaple 39460 | 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 39461 | 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 39462 | The projective map of an atom. (Contributed by NM, 25-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑀‘𝑃) = {𝑃}) | ||
Theorem | elpmapat 39463 | Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ (𝑀‘𝑃) ↔ 𝑋 = 𝑃)) | ||
Theorem | pmap0 39464 | 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 39465 | 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 39466 | 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 39467 | 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 39468* | The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb 39469, where we read 𝑆 as 𝑆(𝑖). Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆)) | ||
Theorem | pmapglb 39469* | 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 39470* | 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 39471* | The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N 39470, 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 39472 | The projective map of a meet. (Contributed by NM, 25-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑃‘(𝑋 ∧ 𝑌)) = ((𝑃‘𝑋) ∩ (𝑃‘𝑌))) | ||
Theorem | isline2 39473* | Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (𝑋 ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑀‘(𝑝 ∨ 𝑞))))) | ||
Theorem | linepmap 39474 | A line described with a projective map. (Contributed by NM, 3-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑀‘(𝑃 ∨ 𝑄)) ∈ 𝑁) | ||
Theorem | isline3 39475* | Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑝 ∨ 𝑞)))) | ||
Theorem | isline4N 39476* | 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 39477 | 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 39478* | 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 39479* | 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 39480 | 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 39481 | A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → 𝑃𝐶𝑋) | ||
Theorem | lncmp 39482 | If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ (𝑀‘𝑌) ∈ 𝑁)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) | ||
Theorem | 2lnat 39483 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐹‘𝑋) ∈ 𝑁 ∧ (𝐹‘𝑌) ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴) | ||
Theorem | 2atm2atN 39484 | 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 39485 | Generalization of 2llnma1 39486. (Contributed by NM, 26-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃) | ||
Theorem | 2llnma1 39486 | 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 39487 | 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 39488 | 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 39489 | 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 ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ((𝑃 ∨ 𝑅) ∧ (𝑄 ∨ 𝑅)) = 𝑅) | ||
Theorem | cdlema1N 39490 | 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 39491 | 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 39492 | Lemma for cdlemb 39493. (Contributed by NM, 8-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑋) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ (𝑃 ∨ 𝑢)))) → (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄))) | ||
Theorem | cdlemb 39493* | 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 39494 | Extend class notation with projective subspace sum. |
class +𝑃 | ||
Definition | df-padd 39495* | 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 39496* | Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) | ||
Theorem | paddval 39497* | Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) | ||
Theorem | elpadd 39498* | Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟))))) | ||
Theorem | elpaddn0 39499* | Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟)))) | ||
Theorem | paddvaln0N 39500* | Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑋 + 𝑌) = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |