![]() |
Metamath
Proof Explorer Theorem List (p. 371 of 454) | < 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-28701) |
![]() (28702-30224) |
![]() (30225-45333) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dalem33 37001 | Lemma for dath 37032. Analogue of dalem28 36996 for 𝐻. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑄 ≤ (𝐻 ∨ 𝑐)) | ||
Theorem | dalem34 37002 | Lemma for dath 37032. Analogue of dalem23 36992 for 𝐼. (Contributed by NM, 2-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐼 ∈ 𝐴) | ||
Theorem | dalem35 37003 | Lemma for dath 37032. Analogue of dalem24 36993 for 𝐼. (Contributed by NM, 3-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐼 ≤ 𝑌) | ||
Theorem | dalem36 37004 | Lemma for dath 37032. Analogue of dalem27 36995 for 𝐼. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑐 ≤ (𝐼 ∨ 𝑅)) | ||
Theorem | dalem37 37005 | Lemma for dath 37032. Analogue of dalem28 36996 for 𝐼. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑅 ≤ (𝐼 ∨ 𝑐)) | ||
Theorem | dalem38 37006 | Lemma for dath 37032. Plane 𝑌 belongs to the 3-dimensional volume 𝐺𝐻𝐼𝑐. (Contributed by NM, 5-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝑌 ≤ (((𝐺 ∨ 𝐻) ∨ 𝐼) ∨ 𝑐)) | ||
Theorem | dalem39 37007 | Lemma for dath 37032. Auxiliary atoms 𝐺, 𝐻, and 𝐼 are not colinear. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐻 ≤ (𝐼 ∨ 𝐺)) | ||
Theorem | dalem40 37008 | Lemma for dath 37032. Analogue of dalem39 37007 for 𝐼. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝐼 ≤ (𝐺 ∨ 𝐻)) | ||
Theorem | dalem41 37009 | Lemma for dath 37032. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐺 ≠ 𝐻) | ||
Theorem | dalem42 37010 | Lemma for dath 37032. Auxiliary atoms 𝐺𝐻𝐼 form a plane. (Contributed by NM, 4-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ∈ 𝑂) | ||
Theorem | dalem43 37011 | Lemma for dath 37032. Planes 𝐺𝐻𝐼 and 𝑌 are different. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∨ 𝐼) ≠ 𝑌) | ||
Theorem | dalem44 37012 | Lemma for dath 37032. Dummy center of perspectivity 𝑐 lies outside of plane 𝐺𝐻𝐼. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ ((𝐺 ∨ 𝐻) ∨ 𝐼)) | ||
Theorem | dalem45 37013 | Lemma for dath 37032. Dummy center of perspectivity 𝑐 is not on the line 𝐺𝐻. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐺 ∨ 𝐻)) | ||
Theorem | dalem46 37014 | Lemma for dath 37032. Analogue of dalem45 37013 for 𝐻𝐼. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐻 ∨ 𝐼)) | ||
Theorem | dalem47 37015 | Lemma for dath 37032. Analogue of dalem45 37013 for 𝐼𝐺. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ¬ 𝑐 ≤ (𝐼 ∨ 𝐺)) | ||
Theorem | dalem48 37016 | Lemma for dath 37032. Analogue of dalem45 37013 for 𝑃𝑄. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | dalem49 37017 | Lemma for dath 37032. Analogue of dalem45 37013 for 𝑄𝑅. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑄 ∨ 𝑅)) | ||
Theorem | dalem50 37018 | Lemma for dath 37032. Analogue of dalem45 37013 for 𝑅𝑃. (Contributed by NM, 16-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝜓) → ¬ 𝑐 ≤ (𝑅 ∨ 𝑃)) | ||
Theorem | dalem51 37019 | Lemma for dath 37032. 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 37020 | Lemma for dath 37032. Lines 𝐺𝐻 and 𝑃𝑄 intersect at an atom. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴) | ||
Theorem | dalem53 37021 | Lemma for dath 37032. The auxliary axis of perspectivity 𝐵 is a line (analogous to the actual axis of perspectivity 𝑋 in dalem15 36974. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐵 ∈ 𝑁) | ||
Theorem | dalem54 37022 | Lemma for dath 37032. Line 𝐺𝐻 intersects the auxiliary axis of perspectivity 𝐵. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ 𝐵) ∈ 𝐴) | ||
Theorem | dalem55 37023 | Lemma for dath 37032. Lines 𝐺𝐻 and 𝑃𝑄 intersect at the auxiliary line 𝐵 (later shown to be an axis of perspectivity; see dalem60 37028). (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑃 ∨ 𝑄)) = ((𝐺 ∨ 𝐻) ∧ 𝐵)) | ||
Theorem | dalem56 37024 | Lemma for dath 37032. Analogue of dalem55 37023 for line 𝑆𝑇. (Contributed by NM, 8-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → ((𝐺 ∨ 𝐻) ∧ (𝑆 ∨ 𝑇)) = ((𝐺 ∨ 𝐻) ∧ 𝐵)) | ||
Theorem | dalem57 37025 | Lemma for dath 37032. Axis of perspectivity point 𝐷 is on the auxiliary line 𝐵. (Contributed by NM, 9-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐷 ≤ 𝐵) | ||
Theorem | dalem58 37026 | Lemma for dath 37032. Analogue of dalem57 37025 for 𝐸. (Contributed by NM, 10-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐸 ≤ 𝐵) | ||
Theorem | dalem59 37027 | Lemma for dath 37032. Analogue of dalem57 37025 for 𝐹. (Contributed by NM, 10-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → 𝐹 ≤ 𝐵) | ||
Theorem | dalem60 37028 | Lemma for dath 37032. 𝐵 is an axis of perspectivity (almost). (Contributed by NM, 11-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ (𝜓 ↔ ((𝑐 ∈ 𝐴 ∧ 𝑑 ∈ 𝐴) ∧ ¬ 𝑐 ≤ 𝑌 ∧ (𝑑 ≠ 𝑐 ∧ ¬ 𝑑 ≤ 𝑌 ∧ 𝐶 ≤ (𝑐 ∨ 𝑑)))) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐺 = ((𝑐 ∨ 𝑃) ∧ (𝑑 ∨ 𝑆)) & ⊢ 𝐻 = ((𝑐 ∨ 𝑄) ∧ (𝑑 ∨ 𝑇)) & ⊢ 𝐼 = ((𝑐 ∨ 𝑅) ∧ (𝑑 ∨ 𝑈)) & ⊢ 𝐵 = (((𝐺 ∨ 𝐻) ∨ 𝐼) ∧ 𝑌) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍 ∧ 𝜓) → (𝐷 ∨ 𝐸) = 𝐵) | ||
Theorem | dalem61 37029 | Lemma for dath 37032. 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 37030 | Lemma for dath 37032. Eliminate the condition 𝜓 containing dummy variables 𝑐 and 𝑑. (Contributed by NM, 11-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝐹 ≤ (𝐷 ∨ 𝐸)) | ||
Theorem | dalem63 37031 | Lemma for dath 37032. 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 37032 |
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 36956. For a visual demonstration, see the "Desargues's theorem" applet at http://www.dynamicgeometry.com/JavaSketchpad/Gallery.html 36956. The points I, J, and K there define the axis of perspectivity. See theorem dalaw 37182 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 37033 | Version of Desargues's theorem dath 37032 with a different variable ordering. (Contributed by NM, 7-Oct-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) & ⊢ 𝐸 = ((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) & ⊢ 𝐹 = ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝐶 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑂 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈)))) → 𝐷 ≤ (𝐸 ∨ 𝐹)) | ||
Theorem | lineset 37034* | The set of lines in a Hilbert lattice. (Contributed by NM, 19-Sep-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑁 = {𝑠 ∣ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑠 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)})}) | ||
Theorem | isline 37035* | The predicate "is a line". (Contributed by NM, 19-Sep-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑁 ↔ ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑞 ≠ 𝑟 ∧ 𝑋 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑞 ∨ 𝑟)}))) | ||
Theorem | islinei 37036* | Condition implying "is a line". (Contributed by NM, 3-Feb-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ 𝑋 = {𝑝 ∈ 𝐴 ∣ 𝑝 ≤ (𝑄 ∨ 𝑅)})) → 𝑋 ∈ 𝑁) | ||
Theorem | pointsetN 37037* | The set of points in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑃 = {𝑝 ∣ ∃𝑎 ∈ 𝐴 𝑝 = {𝑎}}) | ||
Theorem | ispointN 37038* | The predicate "is a point". (Contributed by NM, 2-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑃 ↔ ∃𝑎 ∈ 𝐴 𝑋 = {𝑎})) | ||
Theorem | atpointN 37039 | The singleton of an atom is a point. (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (Points‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐴) → {𝑋} ∈ 𝑃) | ||
Theorem | psubspset 37040* | The set of projective subspaces in a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑆 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑠 ∀𝑞 ∈ 𝑠 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑠))}) | ||
Theorem | ispsubsp 37041* | The predicate "is a projective subspace". (Contributed by NM, 2-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝑋 ∀𝑞 ∈ 𝑋 ∀𝑟 ∈ 𝐴 (𝑟 ≤ (𝑝 ∨ 𝑞) → 𝑟 ∈ 𝑋)))) | ||
Theorem | ispsubsp2 37042* | The predicate "is a projective subspace". (Contributed by NM, 13-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝑆 ↔ (𝑋 ⊆ 𝐴 ∧ ∀𝑝 ∈ 𝐴 (∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑝 ≤ (𝑞 ∨ 𝑟) → 𝑝 ∈ 𝑋)))) | ||
Theorem | psubspi 37043* | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑋 𝑃 ≤ (𝑞 ∨ 𝑟)) → 𝑃 ∈ 𝑋) | ||
Theorem | psubspi2N 37044 | Property of a projective subspace. (Contributed by NM, 13-Jan-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝑆 ∧ 𝑃 ∈ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑃 ∈ 𝑋) | ||
Theorem | 0psubN 37045 | 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 37046 | The singleton of an atom is a projective subspace. (Contributed by NM, 9-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → {𝑃} ∈ 𝑆) | ||
Theorem | pointpsubN 37047 | 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 37048 | A line is a projective subspace. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝑆) | ||
Theorem | atpsubN 37049 | 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 37050 | A projective subspace consists of atoms. (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆) → 𝑋 ⊆ 𝐴) | ||
Theorem | psubatN 37051 | A member of a projective subspace is an atom. (Contributed by NM, 4-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑋) → 𝑌 ∈ 𝐴) | ||
Theorem | pmapfval 37052* | The projective map of a Hilbert lattice. (Contributed by NM, 2-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐶 → 𝑀 = (𝑥 ∈ 𝐵 ↦ {𝑎 ∈ 𝐴 ∣ 𝑎 ≤ 𝑥})) | ||
Theorem | pmapval 37053* | 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 37054 | Member of a projective map. (Contributed by NM, 27-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑃 ∈ (𝑀‘𝑋) ↔ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑋))) | ||
Theorem | pmapssat 37055 | The projective map of a Hilbert lattice is a set of atoms. (Contributed by NM, 14-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐴) | ||
Theorem | pmapssbaN 37056 | A weakening of pmapssat 37055 to shorten some proofs. (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐶 ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ⊆ 𝐵) | ||
Theorem | pmaple 37057 | 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 37058 | 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 37059 | The projective map of an atom. (Contributed by NM, 25-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑀‘𝑃) = {𝑃}) | ||
Theorem | elpmapat 37060 | Member of the projective map of an atom. (Contributed by NM, 27-Jan-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → (𝑋 ∈ (𝑀‘𝑃) ↔ 𝑋 = 𝑃)) | ||
Theorem | pmap0 37061 | 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 37062 | 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 37063 | Value of the projective map of a Hilbert lattice at lattice unit. 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 37064 | 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 37065* | The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb 37066, where we read 𝑆 as 𝑆(𝑖). Theorem 15.5.2 of [MaedaMaeda] p. 62. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵 ∧ 𝐼 ≠ ∅) → (𝑀‘(𝐺‘{𝑦 ∣ ∃𝑖 ∈ 𝐼 𝑦 = 𝑆})) = ∩ 𝑖 ∈ 𝐼 (𝑀‘𝑆)) | ||
Theorem | pmapglb 37066* | 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 37067* | 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 37068* | The projective map of the GLB of a set of lattice elements. Index-set version of pmapglb2N 37067, 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 37069 | The projective map of a meet. (Contributed by NM, 25-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑃‘(𝑋 ∧ 𝑌)) = ((𝑃‘𝑋) ∩ (𝑃‘𝑌))) | ||
Theorem | isline2 37070* | Definition of line in terms of projective map. (Contributed by NM, 25-Jan-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (𝐾 ∈ Lat → (𝑋 ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑀‘(𝑝 ∨ 𝑞))))) | ||
Theorem | linepmap 37071 | A line described with a projective map. (Contributed by NM, 3-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → (𝑀‘(𝑃 ∨ 𝑄)) ∈ 𝑁) | ||
Theorem | isline3 37072* | Definition of line in terms of original lattice elements. (Contributed by NM, 29-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ((𝑀‘𝑋) ∈ 𝑁 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ 𝑋 = (𝑝 ∨ 𝑞)))) | ||
Theorem | isline4N 37073* | 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 37074 | 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 37075* | 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 37076* | 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 37077 | 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 37078 | A line covers the atoms it contains. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ 𝑃 ≤ 𝑋)) → 𝑃𝐶𝑋) | ||
Theorem | lncmp 37079 | If two lines are comparable, they are equal. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝑀‘𝑋) ∈ 𝑁 ∧ (𝑀‘𝑌) ∈ 𝑁)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) | ||
Theorem | 2lnat 37080 | Two intersecting lines intersect at an atom. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ ((𝐹‘𝑋) ∈ 𝑁 ∧ (𝐹‘𝑌) ∈ 𝑁) ∧ (𝑋 ≠ 𝑌 ∧ (𝑋 ∧ 𝑌) ≠ 0 )) → (𝑋 ∧ 𝑌) ∈ 𝐴) | ||
Theorem | 2atm2atN 37081 | 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 37082 | Generalization of 2llnma1 37083. (Contributed by NM, 26-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑋)) → ((𝑃 ∨ 𝑋) ∧ (𝑃 ∨ 𝑄)) = 𝑃) | ||
Theorem | 2llnma1 37083 | 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 37084 | 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 37085 | 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 37086 | 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 37087 | 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 37088 | 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 37089 | Lemma for cdlemb 37090. (Contributed by NM, 8-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑉 = ((𝑃 ∨ 𝑄) ∧ 𝑋) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≠ 𝑄) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) ∧ (𝑢 ∈ 𝐴 ∧ (𝑢 ≠ 𝑉 ∧ 𝑢 < 𝑋)) ∧ (𝑟 ∈ 𝐴 ∧ (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑢 ∧ 𝑟 ≤ (𝑃 ∨ 𝑢)))) → (¬ 𝑟 ≤ 𝑋 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄))) | ||
Theorem | cdlemb 37090* | 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 37091 | Extend class notation with projective subspace sum. |
class +𝑃 | ||
Definition | df-padd 37092* | 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 37093* | Projective subspace sum operation. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → + = (𝑚 ∈ 𝒫 𝐴, 𝑛 ∈ 𝒫 𝐴 ↦ ((𝑚 ∪ 𝑛) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑚 ∃𝑟 ∈ 𝑛 𝑝 ≤ (𝑞 ∨ 𝑟)}))) | ||
Theorem | paddval 37094* | Projective subspace sum operation value. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 + 𝑌) = ((𝑋 ∪ 𝑌) ∪ {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)})) | ||
Theorem | elpadd 37095* | Member of a projective subspace sum. (Contributed by NM, 29-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑆 ∈ (𝑋 + 𝑌) ↔ ((𝑆 ∈ 𝑋 ∨ 𝑆 ∈ 𝑌) ∨ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟))))) | ||
Theorem | elpaddn0 37096* | Member of projective subspace sum of nonempty sets. (Contributed by NM, 3-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑆 ∈ (𝑋 + 𝑌) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑆 ≤ (𝑞 ∨ 𝑟)))) | ||
Theorem | paddvaln0N 37097* | Projective subspace sum operation value for nonempty sets. (Contributed by NM, 27-Jan-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑌 ≠ ∅)) → (𝑋 + 𝑌) = {𝑝 ∈ 𝐴 ∣ ∃𝑞 ∈ 𝑋 ∃𝑟 ∈ 𝑌 𝑝 ≤ (𝑞 ∨ 𝑟)}) | ||
Theorem | elpaddri 37098 | Condition implying membership in a projective subspace sum. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑄 ∈ 𝑋 ∧ 𝑅 ∈ 𝑌) ∧ (𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑄 ∨ 𝑅))) → 𝑆 ∈ (𝑋 + 𝑌)) | ||
Theorem | elpaddatriN 37099 | Condition implying membership in a projective subspace sum with a point. (Contributed by NM, 1-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝑋 ∧ 𝑆 ∈ 𝐴 ∧ 𝑆 ≤ (𝑅 ∨ 𝑄))) → 𝑆 ∈ (𝑋 + {𝑄})) | ||
Theorem | elpaddat 37100* | Membership in a projective subspace sum with a point. (Contributed by NM, 29-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ Lat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑋 ≠ ∅) → (𝑆 ∈ (𝑋 + {𝑄}) ↔ (𝑆 ∈ 𝐴 ∧ ∃𝑝 ∈ 𝑋 𝑆 ≤ (𝑝 ∨ 𝑄)))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |