Home | Metamath
Proof Explorer Theorem List (p. 370 of 449) | < 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: | Metamath Proof Explorer
(1-28622) |
Hilbert Space Explorer
(28623-30145) |
Users' Mathboxes
(30146-44834) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dalawlem15 36901 | Lemma for dalaw 36902. Swap variable triples 𝑃𝑄𝑅 and 𝑆𝑇𝑈 in dalawlem14 36900, to obtain the elimination of the remaining conditions in dalawlem1 36887. (Contributed by NM, 6-Oct-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑂 = (LPlanes‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ ¬ (((𝑆 ∨ 𝑇) ∨ 𝑈) ∈ 𝑂 ∧ (¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑆 ∨ 𝑇) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑇 ∨ 𝑈) ∧ ¬ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑈 ∨ 𝑆))) ∧ ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈)) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆)))) | ||
Theorem | dalaw 36902 | Desargues's law, derived from Desargues's theorem dath 36752 and with no conditions on the atoms. If triples 〈𝑃, 𝑄, 𝑅〉 and 〈𝑆, 𝑇, 𝑈〉 are centrally perspective, i.e. ((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈), then they are axially perspective. Theorem 13.3 of [Crawley] p. 110. (Contributed by NM, 7-Oct-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) → (((𝑃 ∨ 𝑆) ∧ (𝑄 ∨ 𝑇)) ≤ (𝑅 ∨ 𝑈) → ((𝑃 ∨ 𝑄) ∧ (𝑆 ∨ 𝑇)) ≤ (((𝑄 ∨ 𝑅) ∧ (𝑇 ∨ 𝑈)) ∨ ((𝑅 ∨ 𝑃) ∧ (𝑈 ∨ 𝑆))))) | ||
Syntax | cpclN 36903 | Extend class notation with projective subspace closure. |
class PCl | ||
Definition | df-pclN 36904* | Projective subspace closure, which is the smallest projective subspace containing an arbitrary set of atoms. The subspace closure of the union of a set of projective subspaces is their supremum in PSubSp. Related to an analogous definition of closure used in Lemma 3.1.4 of [PtakPulmannova] p. 68. (Note that this closure is not necessarily one of the closed projective subspaces PSubCl of df-psubclN 36951.) (Contributed by NM, 7-Sep-2013.) |
⊢ PCl = (𝑘 ∈ V ↦ (𝑥 ∈ 𝒫 (Atoms‘𝑘) ↦ ∩ {𝑦 ∈ (PSubSp‘𝑘) ∣ 𝑥 ⊆ 𝑦})) | ||
Theorem | pclfvalN 36905* | The projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝑉 → 𝑈 = (𝑥 ∈ 𝒫 𝐴 ↦ ∩ {𝑦 ∈ 𝑆 ∣ 𝑥 ⊆ 𝑦})) | ||
Theorem | pclvalN 36906* | Value of the projective subspace closure function. (Contributed by NM, 7-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∩ {𝑦 ∈ 𝑆 ∣ 𝑋 ⊆ 𝑦}) | ||
Theorem | pclclN 36907 | Closure of the projective subspace closure function. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ∈ 𝑆) | ||
Theorem | elpclN 36908* | Membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) & ⊢ 𝑄 ∈ V ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → (𝑄 ∈ (𝑈‘𝑋) ↔ ∀𝑦 ∈ 𝑆 (𝑋 ⊆ 𝑦 → 𝑄 ∈ 𝑦))) | ||
Theorem | elpcliN 36909 | Implication of membership in the projective subspace closure function. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ∈ 𝑆) ∧ 𝑄 ∈ (𝑈‘𝑋)) → 𝑄 ∈ 𝑌) | ||
Theorem | pclssN 36910 | Ordering is preserved by subspace closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝑌 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘𝑋) ⊆ (𝑈‘𝑌)) | ||
Theorem | pclssidN 36911 | A set of atoms is included in its projective subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ (𝑈‘𝑋)) | ||
Theorem | pclidN 36912 | The projective subspace closure of a projective subspace is itself. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆) → (𝑈‘𝑋) = 𝑋) | ||
Theorem | pclbtwnN 36913 | A projective subspace sandwiched between a set of atoms and the set's projective subspace closure equals the closure. (Contributed by NM, 8-Sep-2013.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝑉 ∧ 𝑋 ∈ 𝑆) ∧ (𝑌 ⊆ 𝑋 ∧ 𝑋 ⊆ (𝑈‘𝑌))) → 𝑋 = (𝑈‘𝑌)) | ||
Theorem | pclunN 36914 | The projective subspace closure of the union of two sets of atoms equals the closure of their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝑉 ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑈‘(𝑋 + 𝑌))) | ||
Theorem | pclun2N 36915 | The projective subspace closure of the union of two subspaces equals their projective sum. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑆 ∧ 𝑌 ∈ 𝑆) → (𝑈‘(𝑋 ∪ 𝑌)) = (𝑋 + 𝑌)) | ||
Theorem | pclfinN 36916* | The projective subspace closure of a set equals the union of the closures of its finite subsets. Analogous to Lemma 3.3.6 of [PtakPulmannova] p. 72. Compare the closed subspace version pclfinclN 36966. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) | ||
Theorem | pclcmpatN 36917* | The set of projective subspaces is compactly atomistic: if an atom is in the projective subspace closure of a set of atoms, it also belongs to the projective subspace closure of a finite subset of that set. Analogous to Lemma 3.3.10 of [PtakPulmannova] p. 74. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴 ∧ 𝑃 ∈ (𝑈‘𝑋)) → ∃𝑦 ∈ Fin (𝑦 ⊆ 𝑋 ∧ 𝑃 ∈ (𝑈‘𝑦))) | ||
Syntax | cpolN 36918 | Extend class notation with polarity of projective subspace $m$. |
class ⊥𝑃 | ||
Definition | df-polarityN 36919* | Define polarity of projective subspace, which is a kind of complement of the subspace. Item 2 in [Holland95] p. 222 bottom. For more generality, we define it for all subsets of atoms, not just projective subspaces. The intersection with Atoms‘𝑙 ensures it is defined when 𝑚 = ∅. (Contributed by NM, 23-Oct-2011.) |
⊢ ⊥𝑃 = (𝑙 ∈ V ↦ (𝑚 ∈ 𝒫 (Atoms‘𝑙) ↦ ((Atoms‘𝑙) ∩ ∩ 𝑝 ∈ 𝑚 ((pmap‘𝑙)‘((oc‘𝑙)‘𝑝))))) | ||
Theorem | polfvalN 36920* | The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝))))) | ||
Theorem | polvalN 36921* | Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝)))) | ||
Theorem | polval2N 36922 | Alternate expression for value of the projective subspace polarity function. Equation for polarity in [Holland95] p. 223. (Contributed by NM, 22-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝑀‘( ⊥ ‘(𝑈‘𝑋)))) | ||
Theorem | polsubN 36923 | The polarity of a set of atoms is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝑆) | ||
Theorem | polssatN 36924 | The polarity of a set of atoms is a set of atoms. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ⊆ 𝐴) | ||
Theorem | pol0N 36925 | The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴) | ||
Theorem | pol1N 36926 | The polarity of the whole projective subspace is the empty space. Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ( ⊥ ‘𝐴) = ∅) | ||
Theorem | 2pol0N 36927 | The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅) | ||
Theorem | polpmapN 36928 | The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋))) | ||
Theorem | 2polpmapN 36929 | Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋)) | ||
Theorem | 2polvalN 36930 | Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋))) | ||
Theorem | 2polssN 36931 | A set of atoms is a subset of its double polarity. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → 𝑋 ⊆ ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | 3polN 36932 | Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆)) | ||
Theorem | polcon3N 36933 | Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | 2polcon4bN 36934 | Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | polcon2N 36935 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | polcon2bN 36936 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | pclss2polN 36937 | The projective subspace closure is a subset of closed subspace closure. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) ⊆ ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | pcl0N 36938 | The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅) | ||
Theorem | pcl0bN 36939 | The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅)) | ||
Theorem | pmaplubN 36940 | The LUB of a projective map is the projective map's argument. (Contributed by NM, 13-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑈‘(𝑀‘𝑋)) = 𝑋) | ||
Theorem | sspmaplubN 36941 | A set of atoms is a subset of the projective map of its LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → 𝑆 ⊆ (𝑀‘(𝑈‘𝑆))) | ||
Theorem | 2pmaplubN 36942 | Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆))) | ||
Theorem | paddunN 36943 | The closure of the projective sum of two sets of atoms is the same as the closure of their union. (Closure is actually double polarity, which can be trivially inferred from this theorem using fveq2d 6667.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇))) | ||
Theorem | poldmj1N 36944 | De Morgan's law for polarity of projective sum. (oldmj1 36237 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇))) | ||
Theorem | pmapj2N 36945 | The projective map of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑀‘(𝑋 ∨ 𝑌)) = ( ⊥ ‘( ⊥ ‘((𝑀‘𝑋) + (𝑀‘𝑌))))) | ||
Theorem | pmapocjN 36946 | The projective map of the orthocomplement of the join of two lattice elements. (Contributed by NM, 14-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ 𝑁 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝐹‘( ⊥ ‘(𝑋 ∨ 𝑌))) = (𝑁‘((𝐹‘𝑋) + (𝐹‘𝑌)))) | ||
Theorem | polatN 36947 | The polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 14-Jan-2012.) (New usage is discouraged.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑄 ∈ 𝐴) → (𝑃‘{𝑄}) = (𝑀‘( ⊥ ‘𝑄))) | ||
Theorem | 2polatN 36948 | Double polarity of the singleton of an atom (i.e. a point). (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → (𝑃‘(𝑃‘{𝑄})) = {𝑄}) | ||
Theorem | pnonsingN 36949 | The intersection of a set of atoms and its polarity is empty. Definition of nonsingular in [Holland95] p. 214. (Contributed by NM, 29-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → (𝑋 ∩ (𝑃‘𝑋)) = ∅) | ||
Syntax | cpscN 36950 | Extend class notation with set of all closed projective subspaces for a Hilbert lattice. |
class PSubCl | ||
Definition | df-psubclN 36951* | Define set of all closed projective subspaces, which are those sets of atoms that equal their double polarity. Based on definition in [Holland95] p. 223. (Contributed by NM, 23-Jan-2012.) |
⊢ PSubCl = (𝑘 ∈ V ↦ {𝑠 ∣ (𝑠 ⊆ (Atoms‘𝑘) ∧ ((⊥𝑃‘𝑘)‘((⊥𝑃‘𝑘)‘𝑠)) = 𝑠)}) | ||
Theorem | psubclsetN 36952* | The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)}) | ||
Theorem | ispsubclN 36953 | The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))) | ||
Theorem | psubcliN 36954 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) | ||
Theorem | psubcli2N 36955 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | psubclsubN 36956 | A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆) | ||
Theorem | psubclssatN 36957 | A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴) | ||
Theorem | pmapidclN 36958 | Projective map of the LUB of a closed subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → (𝑀‘(𝑈‘𝑋)) = 𝑋) | ||
Theorem | 0psubclN 36959 | The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶) | ||
Theorem | 1psubclN 36960 | The set of all atoms is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → 𝐴 ∈ 𝐶) | ||
Theorem | atpsubclN 36961 | A point (singleton of an atom) is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑄 ∈ 𝐴) → {𝑄} ∈ 𝐶) | ||
Theorem | pmapsubclN 36962 | A projective map value is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑀‘𝑋) ∈ 𝐶) | ||
Theorem | ispsubcl2N 36963* | Alternate predicate for "is a closed projective subspace". Remark in [Holland95] p. 223. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → (𝑋 ∈ 𝐶 ↔ ∃𝑦 ∈ 𝐵 𝑋 = (𝑀‘𝑦))) | ||
Theorem | psubclinN 36964 | The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶) | ||
Theorem | paddatclN 36965 | The projective sum of a closed subspace and an atom is a closed projective subspace. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑄 ∈ 𝐴) → (𝑋 + {𝑄}) ∈ 𝐶) | ||
Theorem | pclfinclN 36966 | The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 36916 and also pclcmpatN 36917. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) & ⊢ 𝑆 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆) | ||
Theorem | linepsubclN 36967 | A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶) | ||
Theorem | polsubclN 36968 | A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶) | ||
Theorem | poml4N 36969 | Orthomodular law for projective lattices. Lemma 3.3(1) in [Holland95] p. 215. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → ((𝑋 ⊆ 𝑌 ∧ ( ⊥ ‘( ⊥ ‘𝑌)) = 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = ( ⊥ ‘( ⊥ ‘𝑋)))) | ||
Theorem | poml5N 36970 | Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | poml6N 36971 | Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋) | ||
Theorem | osumcllem1N 36972 | Lemma for osumclN 36983. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀) | ||
Theorem | osumcllem2N 36973 | Lemma for osumclN 36983. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀)) | ||
Theorem | osumcllem3N 36974 | Lemma for osumclN 36983. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌) | ||
Theorem | osumcllem4N 36975 | Lemma for osumclN 36983. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟) | ||
Theorem | osumcllem5N 36976 | Lemma for osumclN 36983. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
Theorem | osumcllem6N 36977 | Lemma for osumclN 36983. Use atom exchange hlatexch1 36411 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
Theorem | osumcllem7N 36978* | Lemma for osumclN 36983. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
Theorem | osumcllem8N 36979 | Lemma for osumclN 36983. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅) | ||
Theorem | osumcllem9N 36980 | Lemma for osumclN 36983. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋) | ||
Theorem | osumcllem10N 36981 | Lemma for osumclN 36983. Contradict osumcllem9N 36980. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 ≠ 𝑋) | ||
Theorem | osumcllem11N 36982 | Lemma for osumclN 36983. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))) | ||
Theorem | osumclN 36983 | Closure of orthogonal sum. If 𝑋 and 𝑌 are orthogonal closed projective subspaces, then their sum is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (𝑋 + 𝑌) ∈ 𝐶) | ||
Theorem | pmapojoinN 36984 | For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 36868 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌))) | ||
Theorem | pexmidN 36985 | Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 36969. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 36983. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴) | ||
Theorem | pexmidlem1N 36986 | Lemma for pexmidN 36985. Holland's proof implicitly requires 𝑞 ≠ 𝑟, which we prove here. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋))) → 𝑞 ≠ 𝑟) | ||
Theorem | pexmidlem2N 36987 | Lemma for pexmidN 36985. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋) ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
Theorem | pexmidlem3N 36988 | Lemma for pexmidN 36985. Use atom exchange hlatexch1 36411 to swap 𝑝 and 𝑞. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
Theorem | pexmidlem4N 36989* | Lemma for pexmidN 36985. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
Theorem | pexmidlem5N 36990 | Lemma for pexmidN 36985. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → (( ⊥ ‘𝑋) ∩ 𝑀) = ∅) | ||
Theorem | pexmidlem6N 36991 | Lemma for pexmidN 36985. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 = 𝑋) | ||
Theorem | pexmidlem7N 36992 | Lemma for pexmidN 36985. Contradict pexmidlem6N 36991. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 ≠ 𝑋) | ||
Theorem | pexmidlem8N 36993 | Lemma for pexmidN 36985. The contradiction of pexmidlem6N 36991 and pexmidlem7N 36992 shows that there can be no atom 𝑝 that is not in 𝑋 + ( ⊥ ‘𝑋), which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅)) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴) | ||
Theorem | pexmidALTN 36994 | Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 36969. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables 𝑋, 𝑀, 𝑝, 𝑞, 𝑟 in place of Hollands' l, m, P, Q, L respectively. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴) | ||
Theorem | pl42lem1N 36995 | Lemma for pl42N 36999. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)))) | ||
Theorem | pl42lem2N 36996 | Lemma for pl42N 36999. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((𝐹‘𝑋) + (𝐹‘𝑌)) + (((𝐹‘𝑋) + (𝐹‘𝑊)) ∩ ((𝐹‘𝑌) + (𝐹‘𝑉)))) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉))))) | ||
Theorem | pl42lem3N 36997 | Lemma for pl42N 36999. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)) ⊆ ((((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑊)) ∩ (((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑉)))) | ||
Theorem | pl42lem4N 36998 | Lemma for pl42N 36999. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉)))))) | ||
Theorem | pl42N 36999 | Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in [MegPav2000] p. 2366). (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → ((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉) ≤ ((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉))))) | ||
Syntax | clh 37000 | Extend class notation with set of all co-atoms (lattice hyperplanes). |
class LHyp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |