![]() |
Metamath
Proof Explorer Theorem List (p. 397 of 485) | < 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-30800) |
![]() (30801-32323) |
![]() (32324-48424) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | lhpbase 39601 | A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) | ||
Theorem | lhp1cvr 39602 | The lattice unity covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012.) |
⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐻) → 𝑊𝐶 1 ) | ||
Theorem | lhplt 39603 | An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊)) → 𝑃 < 𝑊) | ||
Theorem | lhp2lt 39604 | The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑄 ≤ 𝑊)) → (𝑃 ∨ 𝑄) < 𝑊) | ||
Theorem | lhpexlt 39605* | There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑊) | ||
Theorem | lhp0lt 39606 | A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
⊢ < = (lt‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 0 < 𝑊) | ||
Theorem | lhpn0 39607 | A co-atom is nonzero. TODO: is this needed? (Contributed by NM, 26-Apr-2013.) |
⊢ 0 = (0.‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → 𝑊 ≠ 0 ) | ||
Theorem | lhpexle 39608* | There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 𝑝 ≤ 𝑊) | ||
Theorem | lhpexnle 39609* | There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 ¬ 𝑝 ≤ 𝑊) | ||
Theorem | lhpexle1lem 39610* | Lemma for lhpexle1 39611 and others that eliminates restrictions on 𝑋. (Contributed by NM, 24-Jul-2013.) |
⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝜓)) & ⊢ ((𝜑 ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋)) ⇒ ⊢ (𝜑 → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝜓 ∧ 𝑝 ≠ 𝑋)) | ||
Theorem | lhpexle1 39611* | There exists an atom under a co-atom different from any given element. (Contributed by NM, 24-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋)) | ||
Theorem | lhpexle2lem 39612* | Lemma for lhpexle2 39613. (Contributed by NM, 19-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐴 ∧ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐴 ∧ 𝑌 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌)) | ||
Theorem | lhpexle2 39613* | There exists atom under a co-atom different from any two other elements. (Contributed by NM, 24-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌)) | ||
Theorem | lhpexle3lem 39614* | There exists atom under a co-atom different from any three other atoms. TODO: study if adant*, simp* usage can be improved. (Contributed by NM, 9-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴 ∧ 𝑍 ∈ 𝐴) ∧ (𝑋 ≤ 𝑊 ∧ 𝑌 ≤ 𝑊 ∧ 𝑍 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | ||
Theorem | lhpexle3 39615* | There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ (𝑝 ≠ 𝑋 ∧ 𝑝 ≠ 𝑌 ∧ 𝑝 ≠ 𝑍))) | ||
Theorem | lhpex2leN 39616* | There exist at least two different atoms under a co-atom. This allows to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝 ≤ 𝑊 ∧ 𝑞 ≤ 𝑊 ∧ 𝑝 ≠ 𝑞)) | ||
Theorem | lhpoc 39617 | The orthocomplement of a co-atom (lattice hyperplane) is an atom. (Contributed by NM, 18-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵) → (𝑊 ∈ 𝐻 ↔ ( ⊥ ‘𝑊) ∈ 𝐴)) | ||
Theorem | lhpoc2N 39618 | The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐵) → (𝑊 ∈ 𝐴 ↔ ( ⊥ ‘𝑊) ∈ 𝐻)) | ||
Theorem | lhpocnle 39619 | The orthocomplement of a co-atom is not under it. (Contributed by NM, 22-May-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ¬ ( ⊥ ‘𝑊) ≤ 𝑊) | ||
Theorem | lhpocat 39620 | The orthocomplement of a co-atom is an atom. (Contributed by NM, 9-Feb-2013.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → ( ⊥ ‘𝑊) ∈ 𝐴) | ||
Theorem | lhpocnel 39621 | The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 25-May-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (( ⊥ ‘𝑊) ∈ 𝐴 ∧ ¬ ( ⊥ ‘𝑊) ≤ 𝑊)) | ||
Theorem | lhpocnel2 39622 | The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑃 = ((oc‘𝐾)‘𝑊) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) | ||
Theorem | lhpjat1 39623 | The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 18-May-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑊 ∨ 𝑃) = 1 ) | ||
Theorem | lhpjat2 39624 | The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 4-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∨ 𝑊) = 1 ) | ||
Theorem | lhpj1 39625 | The join of a co-atom (hyperplane) and an element not under it is the lattice unity. (Contributed by NM, 7-Dec-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → (𝑊 ∨ 𝑋) = 1 ) | ||
Theorem | lhpmcvr 39626 | The meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 7-Dec-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → (𝑋 ∧ 𝑊)𝐶𝑋) | ||
Theorem | lhpmcvr2 39627* | Alternate way to express that the meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 9-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ (𝑝 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) | ||
Theorem | lhpmcvr3 39628 | Specialization of lhpmcvr2 39627. TODO: Use this to simplify many uses of (𝑃 ∨ (𝑋 ∧ 𝑊)) = 𝑋 to become 𝑃 ≤ 𝑋. (Contributed by NM, 6-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ≤ 𝑋 ↔ (𝑃 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) | ||
Theorem | lhpmcvr4N 39629 | Specialization of lhpmcvr2 39627. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊 ∧ 𝑃 ≤ 𝑋)) → ¬ 𝑃 ≤ 𝑌) | ||
Theorem | lhpmcvr5N 39630* | Specialization of lhpmcvr2 39627. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ (𝑝 ∨ (𝑋 ∧ 𝑊)) = 𝑋)) | ||
Theorem | lhpmcvr6N 39631* | Specialization of lhpmcvr2 39627. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ ¬ 𝑋 ≤ 𝑊) ∧ (𝑌 ∈ 𝐵 ∧ (𝑋 ∧ 𝑌) ≤ 𝑊)) → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑊 ∧ ¬ 𝑝 ≤ 𝑌 ∧ 𝑝 ≤ 𝑋)) | ||
Theorem | lhpm0atN 39632 | If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ∧ (𝑋 ∧ 𝑊) = 0 )) → 𝑋 ∈ 𝐴) | ||
Theorem | lhpmat 39633 | An element covered by the lattice unity, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) → (𝑃 ∧ 𝑊) = 0 ) | ||
Theorem | lhpmatb 39634 | An element covered by the lattice unity, when conjoined with an atom, equals zero iff the atom is not under it. (Contributed by NM, 15-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑊 ↔ (𝑃 ∧ 𝑊) = 0 )) | ||
Theorem | lhp2at0 39635 | Join and meet with different atoms under co-atom 𝑊. (Contributed by NM, 15-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ((𝑃 ∨ 𝑈) ∧ 𝑉) = 0 ) | ||
Theorem | lhp2atnle 39636 | Inequality for 2 different atoms under co-atom 𝑊. (Contributed by NM, 17-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ¬ 𝑉 ≤ (𝑃 ∨ 𝑈)) | ||
Theorem | lhp2atne 39637 | Inequality for joins with 2 different atoms under co-atom 𝑊. (Contributed by NM, 22-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ ((𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉)) | ||
Theorem | lhp2at0nle 39638 | Inequality for 2 different atoms (or an atom and zero) under co-atom 𝑊. (Contributed by NM, 28-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑈 ≠ 𝑉) ∧ ((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) → ¬ 𝑉 ≤ (𝑃 ∨ 𝑈)) | ||
Theorem | lhp2at0ne 39639 | Inequality for joins with 2 different atoms (or an atom and zero) under co-atom 𝑊. (Contributed by NM, 28-Jul-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑄 ∈ 𝐴) ∧ (((𝑈 ∈ 𝐴 ∨ 𝑈 = 0 ) ∧ 𝑈 ≤ 𝑊) ∧ (𝑉 ∈ 𝐴 ∧ 𝑉 ≤ 𝑊)) ∧ 𝑈 ≠ 𝑉) → (𝑃 ∨ 𝑈) ≠ (𝑄 ∨ 𝑉)) | ||
Theorem | lhpelim 39640 | Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat 39633 to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ 𝑋 ∈ 𝐵) → ((𝑃 ∨ (𝑋 ∧ 𝑊)) ∧ 𝑊) = (𝑋 ∧ 𝑊)) | ||
Theorem | lhpmod2i2 39641 | Modular law for hyperplanes analogous to atmod2i2 39465 for atoms. (Contributed by NM, 9-Feb-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑌 ≤ 𝑋) → ((𝑋 ∧ 𝑊) ∨ 𝑌) = (𝑋 ∧ (𝑊 ∨ 𝑌))) | ||
Theorem | lhpmod6i1 39642 | Modular law for hyperplanes analogous to complement of atmod2i1 39464 for atoms. (Contributed by NM, 1-Jun-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑊) → (𝑋 ∨ (𝑌 ∧ 𝑊)) = ((𝑋 ∨ 𝑌) ∧ 𝑊)) | ||
Theorem | lhprelat3N 39643* | The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 39015. (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑤 ∈ 𝐻 (𝑋 ≤ (𝑌 ∧ 𝑤) ∧ (𝑌 ∧ 𝑤)𝐶𝑌)) | ||
Theorem | cdlemb2 39644* | Given two atoms not under the fiducial (reference) co-atom 𝑊, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 30-May-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑄))) | ||
Theorem | lhple 39645 | Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑋 ∈ 𝐵 ∧ 𝑋 ≤ 𝑊)) → ((𝑃 ∨ 𝑋) ∧ 𝑊) = 𝑋) | ||
Theorem | lhpat 39646 | Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → ((𝑃 ∨ 𝑄) ∧ 𝑊) ∈ 𝐴) | ||
Theorem | lhpat4N 39647 | Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑈 ∈ 𝐴 ∧ 𝑈 ≤ 𝑊)) → ((𝑃 ∨ 𝑈) ∧ 𝑊) = 𝑈) | ||
Theorem | lhpat2 39648 | Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 21-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑅 = ((𝑃 ∨ 𝑄) ∧ 𝑊) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄)) → 𝑅 ∈ 𝐴) | ||
Theorem | lhpat3 39649 | There is only one atom under both 𝑃 ∨ 𝑄 and co-atom 𝑊. (Contributed by NM, 21-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑅 = ((𝑃 ∨ 𝑄) ∧ 𝑊) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) ∧ (𝑄 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑆 ≤ (𝑃 ∨ 𝑄))) → (¬ 𝑆 ≤ 𝑊 ↔ 𝑆 ≠ 𝑅)) | ||
Theorem | 4atexlemk 39650 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝐾 ∈ HL) | ||
Theorem | 4atexlemw 39651 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝑊 ∈ 𝐻) | ||
Theorem | 4atexlempw 39652 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊)) | ||
Theorem | 4atexlemp 39653 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝑃 ∈ 𝐴) | ||
Theorem | 4atexlemq 39654 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝑄 ∈ 𝐴) | ||
Theorem | 4atexlems 39655 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝑆 ∈ 𝐴) | ||
Theorem | 4atexlemt 39656 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝑇 ∈ 𝐴) | ||
Theorem | 4atexlemutvt 39657 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇)) | ||
Theorem | 4atexlempnq 39658 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝑃 ≠ 𝑄) | ||
Theorem | 4atexlemnslpq 39659 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | 4atexlemkl 39660 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝐾 ∈ Lat) | ||
Theorem | 4atexlemkc 39661 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) ⇒ ⊢ (𝜑 → 𝐾 ∈ CvLat) | ||
Theorem | 4atexlemwb 39662 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝜑 → 𝑊 ∈ (Base‘𝐾)) | ||
Theorem | 4atexlempsb 39663 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → (𝑃 ∨ 𝑆) ∈ (Base‘𝐾)) | ||
Theorem | 4atexlemqtb 39664 | Lemma for 4atexlem7 39678. (Contributed by NM, 24-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → (𝑄 ∨ 𝑇) ∈ (Base‘𝐾)) | ||
Theorem | 4atexlempns 39665 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝜑 → 𝑃 ≠ 𝑆) | ||
Theorem | 4atexlemswapqr 39666 | Lemma for 4atexlem7 39678. Swap 𝑄 and 𝑅, so that theorems involving 𝐶 can be reused for 𝐷. Note that 𝑈 must be expanded because it involves 𝑄. (Contributed by NM, 25-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) ⇒ ⊢ (𝜑 → (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊 ∧ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄)) ∧ (𝑇 ∈ 𝐴 ∧ (((𝑃 ∨ 𝑅) ∧ 𝑊) ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑅)))) | ||
Theorem | 4atexlemu 39667 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) ⇒ ⊢ (𝜑 → 𝑈 ∈ 𝐴) | ||
Theorem | 4atexlemv 39668 | Lemma for 4atexlem7 39678. (Contributed by NM, 23-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (𝜑 → 𝑉 ∈ 𝐴) | ||
Theorem | 4atexlemunv 39669 | Lemma for 4atexlem7 39678. (Contributed by NM, 21-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (𝜑 → 𝑈 ≠ 𝑉) | ||
Theorem | 4atexlemtlw 39670 | Lemma for 4atexlem7 39678. (Contributed by NM, 24-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (𝜑 → 𝑇 ≤ 𝑊) | ||
Theorem | 4atexlemntlpq 39671 | Lemma for 4atexlem7 39678. (Contributed by NM, 24-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) ⇒ ⊢ (𝜑 → ¬ 𝑇 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | 4atexlemc 39672 | Lemma for 4atexlem7 39678. (Contributed by NM, 24-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ⇒ ⊢ (𝜑 → 𝐶 ∈ 𝐴) | ||
Theorem | 4atexlemnclw 39673 | Lemma for 4atexlem7 39678. (Contributed by NM, 24-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ⇒ ⊢ (𝜑 → ¬ 𝐶 ≤ 𝑊) | ||
Theorem | 4atexlemex2 39674* | Lemma for 4atexlem7 39678. Show that when 𝐶 ≠ 𝑆, 𝐶 satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝐶 ≠ 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) | ||
Theorem | 4atexlemcnd 39675 | Lemma for 4atexlem7 39678. (Contributed by NM, 24-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) & ⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ⇒ ⊢ (𝜑 → 𝐶 ≠ 𝐷) | ||
Theorem | 4atexlemex4 39676* | Lemma for 4atexlem7 39678. Show that when 𝐶 = 𝑆, 𝐷 satisfies the existence condition of the consequent. (Contributed by NM, 26-Nov-2012.) |
⊢ (𝜑 ↔ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ (𝑆 ∈ 𝐴 ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅)) ∧ (𝑇 ∈ 𝐴 ∧ (𝑈 ∨ 𝑇) = (𝑉 ∨ 𝑇))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄)))) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) & ⊢ 𝑈 = ((𝑃 ∨ 𝑄) ∧ 𝑊) & ⊢ 𝑉 = ((𝑃 ∨ 𝑆) ∧ 𝑊) & ⊢ 𝐶 = ((𝑄 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) & ⊢ 𝐷 = ((𝑅 ∨ 𝑇) ∧ (𝑃 ∨ 𝑆)) ⇒ ⊢ ((𝜑 ∧ 𝐶 = 𝑆) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) | ||
Theorem | 4atexlemex6 39677* | Lemma for 4atexlem7 39678. (Contributed by NM, 25-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊)) ∧ ((𝑅 ∈ 𝐴 ∧ ¬ 𝑅 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) | ||
Theorem | 4atexlem7 39678* | Whenever there are at least 4 atoms under 𝑃 ∨ 𝑄 (specifically, 𝑃, 𝑄, 𝑟, and (𝑃 ∨ 𝑄) ∧ 𝑊), there are also at least 4 atoms under 𝑃 ∨ 𝑆. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p ∨ q/0 and hence p ∨ s/0 contains at least four atoms..." Note that by cvlsupr2 38945, our (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟) is a shorter way to express 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄). With a longer proof, the condition ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) could be eliminated (see 4atex 39679), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) | ||
Theorem | 4atex 39679* | Whenever there are at least 4 atoms under 𝑃 ∨ 𝑄 (specifically, 𝑃, 𝑄, 𝑟, and (𝑃 ∨ 𝑄) ∧ 𝑊), there are also at least 4 atoms under 𝑃 ∨ 𝑆. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p ∨ q/0 and hence p ∨ s/0 contains at least four atoms..." Note that by cvlsupr2 38945, our (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟) is a shorter way to express 𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄). (Contributed by NM, 27-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑃 ∨ 𝑧) = (𝑆 ∨ 𝑧))) | ||
Theorem | 4atex2 39680* | More general version of 4atex 39679 for a line 𝑆 ∨ 𝑇 not necessarily connected to 𝑃 ∨ 𝑄. (Contributed by NM, 27-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 ∈ 𝐴 ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧))) | ||
Theorem | 4atex2-0aOLDN 39681* | Same as 4atex2 39680 except that 𝑆 is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑇 ∈ 𝐴 ∧ ¬ 𝑇 ≤ 𝑊) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧))) | ||
Theorem | 4atex2-0bOLDN 39682* | Same as 4atex2 39680 except that 𝑇 is zero. (Contributed by NM, 27-May-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 = (0.‘𝐾) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧))) | ||
Theorem | 4atex2-0cOLDN 39683* | Same as 4atex2 39680 except that 𝑆 and 𝑇 are zero. TODO: do we need this one or 4atex2-0aOLDN 39681 or 4atex2-0bOLDN 39682? (Contributed by NM, 27-May-2013.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ 𝑆 = (0.‘𝐾)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑇 = (0.‘𝐾) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑆 ∨ 𝑧) = (𝑇 ∨ 𝑧))) | ||
Theorem | 4atex3 39684* | More general version of 4atex 39679 for a line 𝑆 ∨ 𝑇 not necessarily connected to 𝑃 ∨ 𝑄. (Contributed by NM, 29-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑊 ∈ 𝐻) ∧ ((𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ≤ 𝑊) ∧ (𝑄 ∈ 𝐴 ∧ ¬ 𝑄 ≤ 𝑊) ∧ (𝑆 ∈ 𝐴 ∧ ¬ 𝑆 ≤ 𝑊)) ∧ (𝑃 ≠ 𝑄 ∧ (𝑇 ∈ 𝐴 ∧ 𝑆 ≠ 𝑇) ∧ ∃𝑟 ∈ 𝐴 (¬ 𝑟 ≤ 𝑊 ∧ (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)))) → ∃𝑧 ∈ 𝐴 (¬ 𝑧 ≤ 𝑊 ∧ (𝑧 ≠ 𝑆 ∧ 𝑧 ≠ 𝑇 ∧ 𝑧 ≤ (𝑆 ∨ 𝑇)))) | ||
Theorem | lautset 39685* | The set of lattice automorphisms. (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐼 = {𝑓 ∣ (𝑓:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝑓‘𝑥) ≤ (𝑓‘𝑦)))}) | ||
Theorem | islaut 39686* | The predicate "is a lattice automorphism". (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → (𝐹 ∈ 𝐼 ↔ (𝐹:𝐵–1-1-onto→𝐵 ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 ↔ (𝐹‘𝑥) ≤ (𝐹‘𝑦))))) | ||
Theorem | lautle 39687 | Less-than or equal property of a lattice automorphism. (Contributed by NM, 19-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (𝐹‘𝑋) ≤ (𝐹‘𝑌))) | ||
Theorem | laut1o 39688 | A lattice automorphism is one-to-one and onto. (Contributed by NM, 19-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝐹 ∈ 𝐼) → 𝐹:𝐵–1-1-onto→𝐵) | ||
Theorem | laut11 39689 | One-to-one property of a lattice automorphism. (Contributed by NM, 20-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → ((𝐹‘𝑋) = (𝐹‘𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | lautcl 39690 | A lattice automorphism value belongs to the base set. (Contributed by NM, 20-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (𝐹‘𝑋) ∈ 𝐵) | ||
Theorem | lautcnvclN 39691 | Reverse closure of a lattice automorphism. (Contributed by NM, 25-May-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ 𝑋 ∈ 𝐵) → (◡𝐹‘𝑋) ∈ 𝐵) | ||
Theorem | lautcnvle 39692 | Less-than or equal property of lattice automorphism converse. (Contributed by NM, 19-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 ≤ 𝑌 ↔ (◡𝐹‘𝑋) ≤ (◡𝐹‘𝑌))) | ||
Theorem | lautcnv 39693 | The converse of a lattice automorphism is a lattice automorphism. (Contributed by NM, 10-May-2013.) |
⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼) → ◡𝐹 ∈ 𝐼) | ||
Theorem | lautlt 39694 | Less-than property of a lattice automorphism. (Contributed by NM, 20-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋 < 𝑌 ↔ (𝐹‘𝑋) < (𝐹‘𝑌))) | ||
Theorem | lautcvr 39695 | Covering property of a lattice automorphism. (Contributed by NM, 20-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝑋𝐶𝑌 ↔ (𝐹‘𝑋)𝐶(𝐹‘𝑌))) | ||
Theorem | lautj 39696 | Meet property of a lattice automorphism. (Contributed by NM, 25-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∨ 𝑌)) = ((𝐹‘𝑋) ∨ (𝐹‘𝑌))) | ||
Theorem | lautm 39697 | Meet property of a lattice automorphism. (Contributed by NM, 19-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ Lat ∧ (𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵)) → (𝐹‘(𝑋 ∧ 𝑌)) = ((𝐹‘𝑋) ∧ (𝐹‘𝑌))) | ||
Theorem | lauteq 39698* | A lattice automorphism argument is equal to its value if all atoms are equal to their values. (Contributed by NM, 24-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝐹 ∈ 𝐼 ∧ 𝑋 ∈ 𝐵) ∧ ∀𝑝 ∈ 𝐴 (𝐹‘𝑝) = 𝑝) → (𝐹‘𝑋) = 𝑋) | ||
Theorem | idlaut 39699 | The identity function is a lattice automorphism. (Contributed by NM, 18-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → ( I ↾ 𝐵) ∈ 𝐼) | ||
Theorem | lautco 39700 | The composition of two lattice automorphisms is a lattice automorphism. (Contributed by NM, 19-Apr-2013.) |
⊢ 𝐼 = (LAut‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝐹 ∈ 𝐼 ∧ 𝐺 ∈ 𝐼) → (𝐹 ∘ 𝐺) ∈ 𝐼) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |