| Metamath
Proof Explorer Theorem List (p. 400 of 494) | < 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-30937) |
(30938-32460) |
(32461-49324) |
| Type | Label | Description |
|---|---|---|
| Statement | ||
| Theorem | pclun2N 39901 | 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 39902* | 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 39952. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) | ||
| Theorem | pclcmpatN 39903* | 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 39904 | Extend class notation with polarity of projective subspace $m$. |
| class ⊥𝑃 | ||
| Definition | df-polarityN 39905* | 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 39906* | The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
| ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝))))) | ||
| Theorem | polvalN 39907* | Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
| ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝)))) | ||
| Theorem | polval2N 39908 | 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 39909 | 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 39910 | 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 39911 | The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴) | ||
| Theorem | pol1N 39912 | 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 39913 | The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
| ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅) | ||
| Theorem | polpmapN 39914 | The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋))) | ||
| Theorem | 2polpmapN 39915 | Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋)) | ||
| Theorem | 2polvalN 39916 | Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋))) | ||
| Theorem | 2polssN 39917 | 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 39918 | Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆)) | ||
| Theorem | polcon3N 39919 | Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) | ||
| Theorem | 2polcon4bN 39920 | Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | ||
| Theorem | polcon2N 39921 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋)) | ||
| Theorem | polcon2bN 39922 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋))) | ||
| Theorem | pclss2polN 39923 | 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 39924 | The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
| ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅) | ||
| Theorem | pcl0bN 39925 | The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅)) | ||
| Theorem | pmaplubN 39926 | 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 39927 | 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 39928 | Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆))) | ||
| Theorem | paddunN 39929 | 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 6910.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇))) | ||
| Theorem | poldmj1N 39930 | De Morgan's law for polarity of projective sum. (oldmj1 39222 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇))) | ||
| Theorem | pmapj2N 39931 | 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 39932 | 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 39933 | 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 39934 | 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 39935 | 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 39936 | Extend class notation with set of all closed projective subspaces for a Hilbert lattice. |
| class PSubCl | ||
| Definition | df-psubclN 39937* | 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 39938* | The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)}) | ||
| Theorem | ispsubclN 39939 | The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))) | ||
| Theorem | psubcliN 39940 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) | ||
| Theorem | psubcli2N 39941 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
| ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
| Theorem | psubclsubN 39942 | A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆) | ||
| Theorem | psubclssatN 39943 | A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴) | ||
| Theorem | pmapidclN 39944 | 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 39945 | The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶) | ||
| Theorem | 1psubclN 39946 | 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 39947 | 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 39948 | 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 39949* | 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 39950 | The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶) | ||
| Theorem | paddatclN 39951 | 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 39952 | The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 39902 and also pclcmpatN 39903. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) & ⊢ 𝑆 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆) | ||
| Theorem | linepsubclN 39953 | A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶) | ||
| Theorem | polsubclN 39954 | A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶) | ||
| Theorem | poml4N 39955 | 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 39956 | Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋))) | ||
| Theorem | poml6N 39957 | Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋) | ||
| Theorem | osumcllem1N 39958 | Lemma for osumclN 39969. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀) | ||
| Theorem | osumcllem2N 39959 | Lemma for osumclN 39969. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀)) | ||
| Theorem | osumcllem3N 39960 | Lemma for osumclN 39969. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌) | ||
| Theorem | osumcllem4N 39961 | Lemma for osumclN 39969. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟) | ||
| Theorem | osumcllem5N 39962 | Lemma for osumclN 39969. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
| Theorem | osumcllem6N 39963 | Lemma for osumclN 39969. Use atom exchange hlatexch1 39397 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
| Theorem | osumcllem7N 39964* | Lemma for osumclN 39969. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
| Theorem | osumcllem8N 39965 | Lemma for osumclN 39969. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅) | ||
| Theorem | osumcllem9N 39966 | Lemma for osumclN 39969. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋) | ||
| Theorem | osumcllem10N 39967 | Lemma for osumclN 39969. Contradict osumcllem9N 39966. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 ≠ 𝑋) | ||
| Theorem | osumcllem11N 39968 | Lemma for osumclN 39969. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))) | ||
| Theorem | osumclN 39969 | 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 39970 | For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 39854 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌))) | ||
| Theorem | pexmidN 39971 | Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 39955. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 39969. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴) | ||
| Theorem | pexmidlem1N 39972 | Lemma for pexmidN 39971. 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 39973 | Lemma for pexmidN 39971. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋) ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
| Theorem | pexmidlem3N 39974 | Lemma for pexmidN 39971. Use atom exchange hlatexch1 39397 to swap 𝑝 and 𝑞. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
| Theorem | pexmidlem4N 39975* | Lemma for pexmidN 39971. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
| Theorem | pexmidlem5N 39976 | Lemma for pexmidN 39971. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → (( ⊥ ‘𝑋) ∩ 𝑀) = ∅) | ||
| Theorem | pexmidlem6N 39977 | Lemma for pexmidN 39971. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 = 𝑋) | ||
| Theorem | pexmidlem7N 39978 | Lemma for pexmidN 39971. Contradict pexmidlem6N 39977. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
| ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 ≠ 𝑋) | ||
| Theorem | pexmidlem8N 39979 | Lemma for pexmidN 39971. The contradiction of pexmidlem6N 39977 and pexmidlem7N 39978 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 39980 | Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 39955. 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 39981 | Lemma for pl42N 39985. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)))) | ||
| Theorem | pl42lem2N 39982 | Lemma for pl42N 39985. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((𝐹‘𝑋) + (𝐹‘𝑌)) + (((𝐹‘𝑋) + (𝐹‘𝑊)) ∩ ((𝐹‘𝑌) + (𝐹‘𝑉)))) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉))))) | ||
| Theorem | pl42lem3N 39983 | Lemma for pl42N 39985. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)) ⊆ ((((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑊)) ∩ (((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑉)))) | ||
| Theorem | pl42lem4N 39984 | Lemma for pl42N 39985. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉)))))) | ||
| Theorem | pl42N 39985 | 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 39986 | Extend class notation with set of all co-atoms (lattice hyperplanes). |
| class LHyp | ||
| Syntax | claut 39987 | Extend class notation with set of all lattice automorphisms. |
| class LAut | ||
| Syntax | cwpointsN 39988 | Extend class notation with W points. |
| class WAtoms | ||
| Syntax | cpautN 39989 | Extend class notation with set of all projective automorphisms. |
| class PAut | ||
| Definition | df-lhyp 39990* | Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e., all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.) |
| ⊢ LHyp = (𝑘 ∈ V ↦ {𝑥 ∈ (Base‘𝑘) ∣ 𝑥( ⋖ ‘𝑘)(1.‘𝑘)}) | ||
| Definition | df-laut 39991* | Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.) |
| ⊢ LAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(Base‘𝑘)–1-1-onto→(Base‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)∀𝑦 ∈ (Base‘𝑘)(𝑥(le‘𝑘)𝑦 ↔ (𝑓‘𝑥)(le‘𝑘)(𝑓‘𝑦)))}) | ||
| Definition | df-watsN 39992* | Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" 𝑑. These are all atoms not in the polarity of {𝑑}), which is the hyperplane determined by 𝑑. Definition of set W in [Crawley] p. 111. (Contributed by NM, 26-Jan-2012.) |
| ⊢ WAtoms = (𝑘 ∈ V ↦ (𝑑 ∈ (Atoms‘𝑘) ↦ ((Atoms‘𝑘) ∖ ((⊥𝑃‘𝑘)‘{𝑑})))) | ||
| Definition | df-pautN 39993* | Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.) |
| ⊢ PAut = (𝑘 ∈ V ↦ {𝑓 ∣ (𝑓:(PSubSp‘𝑘)–1-1-onto→(PSubSp‘𝑘) ∧ ∀𝑥 ∈ (PSubSp‘𝑘)∀𝑦 ∈ (PSubSp‘𝑘)(𝑥 ⊆ 𝑦 ↔ (𝑓‘𝑥) ⊆ (𝑓‘𝑦)))}) | ||
| Theorem | watfvalN 39994* | The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) & ⊢ 𝑊 = (WAtoms‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑊 = (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑})))) | ||
| Theorem | watvalN 39995 | Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) & ⊢ 𝑊 = (WAtoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑊‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷}))) | ||
| Theorem | iswatN 39996 | The predicate "is a W atom" (corresponding to fiducial atom 𝐷). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) & ⊢ 𝑊 = (WAtoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑃 ∈ (𝑊‘𝐷) ↔ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ((⊥𝑃‘𝐾)‘{𝐷})))) | ||
| Theorem | lhpset 39997* | The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐻 = {𝑤 ∈ 𝐵 ∣ 𝑤𝐶 1 }) | ||
| Theorem | islhp 39998 | The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊𝐶 1 ))) | ||
| Theorem | islhp2 39999 | The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 18-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑊 ∈ 𝐵) → (𝑊 ∈ 𝐻 ↔ 𝑊𝐶 1 )) | ||
| Theorem | lhpbase 40000 | A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝑊 ∈ 𝐻 → 𝑊 ∈ 𝐵) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |