![]() |
Metamath
Proof Explorer Theorem List (p. 358 of 437) | < 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-28347) |
![]() (28348-29872) |
![]() (29873-43639) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lplnexatN 35701* | Given a lattice line on a lattice plane, there is an atom whose join with the line equals the plane. (Contributed by NM, 29-Jun-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑁) ∧ 𝑌 ≤ 𝑋) → ∃𝑞 ∈ 𝐴 (¬ 𝑞 ≤ 𝑌 ∧ 𝑋 = (𝑌 ∨ 𝑞))) | ||
Theorem | lplnexllnN 35702* | Given an atom on a lattice plane, there is a lattice line whose join with the atom equals the plane. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ 𝑄 ≤ 𝑋) → ∃𝑦 ∈ 𝑁 (¬ 𝑄 ≤ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑄))) | ||
Theorem | lplnnlt 35703 | Two lattice planes cannot satisfy the less than relation. (Contributed by NM, 7-Jul-2012.) |
⊢ < = (lt‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ¬ 𝑋 < 𝑌) | ||
Theorem | 2llnjaN 35704 | The join of two different lattice lines in a lattice plane equals the plane (version of 2llnjN 35705 in terms of atoms). (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑃) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑄 ≠ 𝑅) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇)) ∧ ((𝑄 ∨ 𝑅) ≤ 𝑊 ∧ (𝑆 ∨ 𝑇) ≤ 𝑊 ∧ (𝑄 ∨ 𝑅) ≠ (𝑆 ∨ 𝑇))) → ((𝑄 ∨ 𝑅) ∨ (𝑆 ∨ 𝑇)) = 𝑊) | ||
Theorem | 2llnjN 35705 | The join of two different lattice lines in a lattice plane equals the plane. (Contributed by NM, 4-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∨ 𝑌) = 𝑊) | ||
Theorem | 2llnm2N 35706 | The meet of two different lattice lines in a lattice plane is an atom. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∧ 𝑌) ∈ 𝐴) | ||
Theorem | 2llnm3N 35707 | Two lattice lines in a lattice plane always meet. (Contributed by NM, 5-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑊 ∈ 𝑃) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊)) → (𝑋 ∧ 𝑌) ≠ 0 ) | ||
Theorem | 2llnm4 35708 | Two lattice lines that majorize the same atom always meet. (Contributed by NM, 20-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁) ∧ (𝑃 ≤ 𝑋 ∧ 𝑃 ≤ 𝑌)) → (𝑋 ∧ 𝑌) ≠ 0 ) | ||
Theorem | 2llnmeqat 35709 | An atom equals the intersection of two majorizing lines. (Contributed by NM, 3-Apr-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑁 ∧ 𝑌 ∈ 𝑁 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋 ≠ 𝑌 ∧ 𝑃 ≤ (𝑋 ∧ 𝑌))) → 𝑃 = (𝑋 ∧ 𝑌)) | ||
Theorem | lvolset 35710* | The set of 3-dim lattice volumes in a Hilbert lattice. (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝑉 = {𝑥 ∈ 𝐵 ∣ ∃𝑦 ∈ 𝑃 𝑦𝐶𝑥}) | ||
Theorem | islvol 35711* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑦 ∈ 𝑃 𝑦𝐶𝑋))) | ||
Theorem | islvol4 35712* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝑉 ↔ ∃𝑦 ∈ 𝑃 𝑦𝐶𝑋)) | ||
Theorem | lvoli 35713 | Condition implying a 3-dim lattice volume. (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐷 ∧ 𝑌 ∈ 𝐵 ∧ 𝑋 ∈ 𝑃) ∧ 𝑋𝐶𝑌) → 𝑌 ∈ 𝑉) | ||
Theorem | islvol3 35714* | The predicate "is a 3-dim lattice volume". (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝑉 ↔ ∃𝑦 ∈ 𝑃 ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑦 ∧ 𝑋 = (𝑦 ∨ 𝑝)))) | ||
Theorem | lvoli3 35715 | Condition implying a 3-dim lattice volume. (Contributed by NM, 2-Aug-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑄 ∈ 𝐴) ∧ ¬ 𝑄 ≤ 𝑋) → (𝑋 ∨ 𝑄) ∈ 𝑉) | ||
Theorem | lvolbase 35716 | A 3-dim lattice volume is a lattice element. (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (𝑋 ∈ 𝑉 → 𝑋 ∈ 𝐵) | ||
Theorem | islvol5 35717* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∈ 𝑉 ↔ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ 𝑋 = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))) | ||
Theorem | islvol2 35718* | The predicate "is a 3-dim lattice volume" in terms of atoms. (Contributed by NM, 1-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝑉 ↔ (𝑋 ∈ 𝐵 ∧ ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 ((𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟)) ∧ 𝑋 = (((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠))))) | ||
Theorem | lvoli2 35719 | The join of 4 different atoms is a lattice volume. (Contributed by NM, 8-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉) | ||
Theorem | lvolnle3at 35720 | A lattice plane (or lattice line or atom) cannot majorize a lattice volume. (Contributed by NM, 8-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ 𝑋 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | ||
Theorem | lvolnleat 35721 | An atom cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑃 ∈ 𝐴) → ¬ 𝑋 ≤ 𝑃) | ||
Theorem | lvolnlelln 35722 | A lattice line cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑁) → ¬ 𝑋 ≤ 𝑌) | ||
Theorem | lvolnlelpln 35723 | A lattice plane cannot majorize a lattice volume. (Contributed by NM, 14-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑃) → ¬ 𝑋 ≤ 𝑌) | ||
Theorem | 3atnelvolN 35724 | The join of 3 atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ¬ ((𝑃 ∨ 𝑄) ∨ 𝑅) ∈ 𝑉) | ||
Theorem | 2atnelvolN 35725 | The join of two atoms is not a lattice volume. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ (𝑃 ∨ 𝑄) ∈ 𝑉) | ||
Theorem | lvolneatN 35726 | No lattice volume is an atom. (Contributed by NM, 15-Jul-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) → ¬ 𝑋 ∈ 𝐴) | ||
Theorem | lvolnelln 35727 | No lattice volume is a lattice line. (Contributed by NM, 15-Jul-2012.) |
⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) → ¬ 𝑋 ∈ 𝑁) | ||
Theorem | lvolnelpln 35728 | No lattice volume is a lattice plane. (Contributed by NM, 19-Jun-2012.) |
⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) → ¬ 𝑋 ∈ 𝑃) | ||
Theorem | lvoln0N 35729 | A lattice volume is nonzero. (Contributed by NM, 17-Jul-2012.) (New usage is discouraged.) |
⊢ 0 = (0.‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉) → 𝑋 ≠ 0 ) | ||
Theorem | islvol2aN 35730 | The predicate "is a lattice volume". (Contributed by NM, 16-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ∈ 𝑉 ↔ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)))) | ||
Theorem | 4atlem0a 35731 | Lemma for 4at 35751. (Contributed by NM, 10-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ¬ 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑆)) | ||
Theorem | 4atlem0ae 35732 | Lemma for 4at 35751. (Contributed by NM, 10-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑄 ≤ (𝑃 ∨ 𝑅)) | ||
Theorem | 4atlem0be 35733 | Lemma for 4at 35751. (Contributed by NM, 10-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄)) → 𝑃 ≠ 𝑅) | ||
Theorem | 4atlem3 35734 | Lemma for 4at 35751. Break inequality into 4 cases. (Contributed by NM, 8-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((¬ 𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ 𝑉) ∨ ¬ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ 𝑉)) ∨ (¬ 𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ 𝑉) ∨ ¬ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ 𝑉)))) | ||
Theorem | 4atlem3a 35735 | Lemma for 4at 35751. Break inequality into 3 cases. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ 𝑉) ∨ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ 𝑉) ∨ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ 𝑉))) | ||
Theorem | 4atlem3b 35736 | Lemma for 4at 35751. Break inequality into 2 cases. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (¬ 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑉) ∨ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑉))) | ||
Theorem | 4atlem4a 35737 | Lemma for 4at 35751. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = (𝑃 ∨ ((𝑄 ∨ 𝑅) ∨ 𝑆))) | ||
Theorem | 4atlem4b 35738 | Lemma for 4at 35751. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = (𝑄 ∨ ((𝑃 ∨ 𝑅) ∨ 𝑆))) | ||
Theorem | 4atlem4c 35739 | Lemma for 4at 35751. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = (𝑅 ∨ ((𝑃 ∨ 𝑄) ∨ 𝑆))) | ||
Theorem | 4atlem4d 35740 | Lemma for 4at 35751. Frequently used associative law. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = (𝑆 ∨ ((𝑃 ∨ 𝑄) ∨ 𝑅))) | ||
Theorem | 4atlem9 35741 | Lemma for 4at 35751. Substitute 𝑊 for 𝑆. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) → (𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑊)) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑊)))) | ||
Theorem | 4atlem10a 35742 | Lemma for 4at 35751. Substitute 𝑉 for 𝑅. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑊)) → (𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑊)) = ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4atlem10b 35743 | Lemma for 4at 35751. Substitute 𝑉 for 𝑅 (cont.). (Contributed by NM, 10-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴) ∧ (𝑊 ∈ 𝐴 ∧ ¬ 𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑊) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) ∧ (𝑅 ≤ ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊))) | ||
Theorem | 4atlem10 35744 | Lemma for 4at 35751. Combine both possible cases. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ ((𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑅 ∨ 𝑆) ≤ ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4atlem11a 35745 | Lemma for 4at 35751. Substitute 𝑈 for 𝑄. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)) → (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑉 ∨ 𝑊)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4atlem11b 35746 | Lemma for 4at 35751. Substitute 𝑈 for 𝑄 (cont.). (Contributed by NM, 10-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑄 ≤ ((𝑃 ∨ 𝑉) ∨ 𝑊)) ∧ (𝑄 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑅 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) | ||
Theorem | 4atlem11 35747 | Lemma for 4at 35751. Combine all three possible cases. (Contributed by NM, 10-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((𝑄 ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4atlem12a 35748 | Lemma for 4at 35751. Substitute 𝑇 for 𝑃. (Contributed by NM, 9-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) → (𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ↔ ((𝑃 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4atlem12b 35749 | Lemma for 4at 35751. Substitute 𝑇 for 𝑃 (cont.). (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ ((𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑈 ∨ 𝑉) ∨ 𝑊)) ∧ ((𝑃 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑄 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) ∧ (𝑅 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ∧ 𝑆 ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))))) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊))) | ||
Theorem | 4atlem12 35750 | Lemma for 4at 35751. Combine all four possible cases. (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4at 35751 | Four atoms determine a lattice volume uniquely. Three-dimensional analogue of ps-1 35615 and 3at 35628. (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) ≤ ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)) ↔ ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑇 ∨ 𝑈) ∨ (𝑉 ∨ 𝑊)))) | ||
Theorem | 4at2 35752 | Four atoms determine a lattice volume uniquely. (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (𝑈 ∈ 𝐴 ∧ 𝑉 ∈ 𝐴 ∧ 𝑊 ∈ 𝐴)) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → ((((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) ≤ (((𝑇 ∨ 𝑈) ∨ 𝑉) ∨ 𝑊) ↔ (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ 𝑆) = (((𝑇 ∨ 𝑈) ∨ 𝑉) ∨ 𝑊))) | ||
Theorem | lplncvrlvol2 35753 | A lattice line under a lattice plane is covered by it. (Contributed by NM, 12-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑉) ∧ 𝑋 ≤ 𝑌) → 𝑋𝐶𝑌) | ||
Theorem | lplncvrlvol 35754 | An element covering a lattice plane is a lattice volume and vice-versa. (Contributed by NM, 15-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → (𝑋 ∈ 𝑃 ↔ 𝑌 ∈ 𝑉)) | ||
Theorem | lvolcmp 35755 | If two lattice planes are comparable, they are equal. (Contributed by NM, 12-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) | ||
Theorem | lvolnltN 35756 | Two lattice volumes cannot satisfy the less than relation. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
⊢ < = (lt‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑉 ∧ 𝑌 ∈ 𝑉) → ¬ 𝑋 < 𝑌) | ||
Theorem | 2lplnja 35757 | The join of two different lattice planes in a lattice volume equals the volume (version of 2lplnj 35758 in terms of atoms). (Contributed by NM, 12-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝑉) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) ∧ ((𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑆 ≠ 𝑇 ∧ ¬ 𝑈 ≤ (𝑆 ∨ 𝑇))) ∧ (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ 𝑊 ∧ ((𝑆 ∨ 𝑇) ∨ 𝑈) ≤ 𝑊 ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≠ ((𝑆 ∨ 𝑇) ∨ 𝑈))) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ∨ ((𝑆 ∨ 𝑇) ∨ 𝑈)) = 𝑊) | ||
Theorem | 2lplnj 35758 | The join of two different lattice planes in a (3-dimensional) lattice volume equals the volume. (Contributed by NM, 12-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∨ 𝑌) = 𝑊) | ||
Theorem | 2lplnm2N 35759 | The meet of two different lattice planes in a lattice volume is a lattice line. (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃 ∧ 𝑊 ∈ 𝑉) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑋 ≠ 𝑌)) → (𝑋 ∧ 𝑌) ∈ 𝑁) | ||
Theorem | 2lplnmj 35760 | The meet of two lattice planes is a lattice line iff their join is a lattice volume. (Contributed by NM, 13-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑁 = (LLines‘𝐾) & ⊢ 𝑃 = (LPlanes‘𝐾) & ⊢ 𝑉 = (LVols‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑃 ∧ 𝑌 ∈ 𝑃) → ((𝑋 ∧ 𝑌) ∈ 𝑁 ↔ (𝑋 ∨ 𝑌) ∈ 𝑉)) | ||
Theorem | dalemkehl 35761 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝐾 ∈ HL) | ||
Theorem | dalemkelat 35762 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝐾 ∈ Lat) | ||
Theorem | dalemkeop 35763 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝐾 ∈ OP) | ||
Theorem | dalempea 35764 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑃 ∈ 𝐴) | ||
Theorem | dalemqea 35765 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐴) | ||
Theorem | dalemrea 35766 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑅 ∈ 𝐴) | ||
Theorem | dalemsea 35767 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐴) | ||
Theorem | dalemtea 35768 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐴) | ||
Theorem | dalemuea 35769 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐴) | ||
Theorem | dalemyeo 35770 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑌 ∈ 𝑂) | ||
Theorem | dalemzeo 35771 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝑍 ∈ 𝑂) | ||
Theorem | dalemclpjs 35772 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝐶 ≤ (𝑃 ∨ 𝑆)) | ||
Theorem | dalemclqjt 35773 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝐶 ≤ (𝑄 ∨ 𝑇)) | ||
Theorem | dalemclrju 35774 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → 𝐶 ≤ (𝑅 ∨ 𝑈)) | ||
Theorem | dalem-clpjq 35775 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) ⇒ ⊢ (𝜑 → ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | dalemceb 35776 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝐶 ∈ (Base‘𝐾)) | ||
Theorem | dalempeb 35777 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑃 ∈ (Base‘𝐾)) | ||
Theorem | dalemqeb 35778 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑄 ∈ (Base‘𝐾)) | ||
Theorem | dalemreb 35779 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑅 ∈ (Base‘𝐾)) | ||
Theorem | dalemseb 35780 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑆 ∈ (Base‘𝐾)) | ||
Theorem | dalemteb 35781 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑇 ∈ (Base‘𝐾)) | ||
Theorem | dalemueb 35782 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑈 ∈ (Base‘𝐾)) | ||
Theorem | dalempjqeb 35783 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → (𝑃 ∨ 𝑄) ∈ (Base‘𝐾)) | ||
Theorem | dalemsjteb 35784 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → (𝑆 ∨ 𝑇) ∈ (Base‘𝐾)) | ||
Theorem | dalemtjueb 35785 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → (𝑇 ∨ 𝑈) ∈ (Base‘𝐾)) | ||
Theorem | dalemqrprot 35786 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → ((𝑄 ∨ 𝑅) ∨ 𝑃) = ((𝑃 ∨ 𝑄) ∨ 𝑅)) | ||
Theorem | dalemyeb 35787 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ 𝑂 = (LPlanes‘𝐾) ⇒ ⊢ (𝜑 → 𝑌 ∈ (Base‘𝐾)) | ||
Theorem | dalemcnes 35788 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝑆) | ||
Theorem | dalempnes 35789 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → 𝑃 ≠ 𝑆) | ||
Theorem | dalemqnet 35790 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → 𝑄 ≠ 𝑇) | ||
Theorem | dalempjsen 35791 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (LLines‘𝐾)) | ||
Theorem | dalemply 35792 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 13-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → 𝑃 ≤ 𝑌) | ||
Theorem | dalemsly 35793 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 15-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍) → 𝑆 ≤ 𝑌) | ||
Theorem | dalemswapyz 35794 | Lemma for dath 35874. Swap the role of planes 𝑌 and 𝑍 to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) ∧ (𝑍 ∈ 𝑂 ∧ 𝑌 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (𝐶 ≤ (𝑆 ∨ 𝑃) ∧ 𝐶 ≤ (𝑇 ∨ 𝑄) ∧ 𝐶 ≤ (𝑈 ∨ 𝑅))))) | ||
Theorem | dalemrot 35795 | Lemma for dath 35874. Rotate triangles 𝑌 = 𝑃𝑄𝑅 and 𝑍 = 𝑆𝑇𝑈 to allow reuse of analogous proofs. (Contributed by NM, 14-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) ⇒ ⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴 ∧ 𝑃 ∈ 𝐴) ∧ (𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) ∧ (((𝑄 ∨ 𝑅) ∨ 𝑃) ∈ 𝑂 ∧ ((𝑇 ∨ 𝑈) ∨ 𝑆) ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃) ∧ ¬ 𝐶 ≤ (𝑃 ∨ 𝑄)) ∧ (¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆) ∧ ¬ 𝐶 ≤ (𝑆 ∨ 𝑇)) ∧ (𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈) ∧ 𝐶 ≤ (𝑃 ∨ 𝑆))))) | ||
Theorem | dalemrotyz 35796 | Lemma for dath 35874. Rotate triangles 𝑌 = 𝑃𝑄𝑅 and 𝑍 = 𝑆𝑇𝑈 to allow reuse of analogous proofs. (Contributed by NM, 19-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) ⇒ ⊢ ((𝜑 ∧ 𝑌 = 𝑍) → ((𝑄 ∨ 𝑅) ∨ 𝑃) = ((𝑇 ∨ 𝑈) ∨ 𝑆)) | ||
Theorem | dalem1 35797 | Lemma for dath 35874. Show the lines 𝑃𝑆 and 𝑄𝑇 are different. (Contributed by NM, 9-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → (𝑃 ∨ 𝑆) ≠ (𝑄 ∨ 𝑇)) | ||
Theorem | dalemcea 35798 | Lemma for dath 35874. Frequently-used utility lemma. Here we show that 𝐶 must be an atom. This is an assumption in most presentations of Desargues's theorem; instead, we assume only the 𝐶 is a lattice element, in order to make later substitutions for 𝐶 easier. (Contributed by NM, 23-Sep-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐴) | ||
Theorem | dalem2 35799 | Lemma for dath 35874. Show the lines 𝑃𝑄 and 𝑆𝑇 form a plane. (Contributed by NM, 11-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) ⇒ ⊢ (𝜑 → ((𝑃 ∨ 𝑄) ∨ (𝑆 ∨ 𝑇)) ∈ 𝑂) | ||
Theorem | dalemdea 35800 | Lemma for dath 35874. Frequently-used utility lemma. (Contributed by NM, 11-Aug-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝐶 ∈ (Base‘𝐾)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (𝑌 ∈ 𝑂 ∧ 𝑍 ∈ 𝑂) ∧ ((¬ 𝐶 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝐶 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝐶 ≤ (𝑅 ∨ 𝑃)) ∧ (¬ 𝐶 ≤ (𝑆 ∨ 𝑇) ∧ ¬ 𝐶 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝐶 ≤ (𝑈 ∨ 𝑆)) ∧ (𝐶 ≤ (𝑃 ∨ 𝑆) ∧ 𝐶 ≤ (𝑄 ∨ 𝑇) ∧ 𝐶 ≤ (𝑅 ∨ 𝑈))))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) & ⊢ 𝑌 = ((𝑃 ∨ 𝑄) ∨ 𝑅) & ⊢ 𝑍 = ((𝑆 ∨ 𝑇) ∨ 𝑈) & ⊢ 𝐷 = ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ⇒ ⊢ (𝜑 → 𝐷 ∈ 𝐴) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |