Home | Metamath
Proof Explorer Theorem List (p. 343 of 424) | < 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-27159) |
Hilbert Space Explorer
(27160-28684) |
Users' Mathboxes
(28685-42360) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pclbtwnN 34201 | 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 34202 | 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 34203 | 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 34204* | 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 34254. (Contributed by NM, 10-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ⊆ 𝐴) → (𝑈‘𝑋) = ∪ 𝑦 ∈ (Fin ∩ 𝒫 𝑋)(𝑈‘𝑦)) | ||
Theorem | pclcmpatN 34205* | 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 34206 | Extend class notation with polarity of projective subspace $m$. |
class ⊥𝑃 | ||
Definition | df-polarityN 34207* | 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 34208* | The projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑃 = (𝑚 ∈ 𝒫 𝐴 ↦ (𝐴 ∩ ∩ 𝑝 ∈ 𝑚 (𝑀‘( ⊥ ‘𝑝))))) | ||
Theorem | polvalN 34209* | Value of the projective subspace polarity function. (Contributed by NM, 23-Oct-2011.) (New usage is discouraged.) |
⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝑋 ⊆ 𝐴) → (𝑃‘𝑋) = (𝐴 ∩ ∩ 𝑝 ∈ 𝑋 (𝑀‘( ⊥ ‘𝑝)))) | ||
Theorem | polval2N 34210 | 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 34211 | 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 34212 | 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 34213 | The polarity of the empty projective subspace is the whole space. (Contributed by NM, 29-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → ( ⊥ ‘∅) = 𝐴) | ||
Theorem | pol1N 34214 | 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 34215 | The closed subspace closure of the empty set. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ( ⊥ ‘( ⊥ ‘∅)) = ∅) | ||
Theorem | polpmapN 34216 | The polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑃‘(𝑀‘𝑋)) = (𝑀‘( ⊥ ‘𝑋))) | ||
Theorem | 2polpmapN 34217 | Double polarity of a projective map. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → ( ⊥ ‘( ⊥ ‘(𝑀‘𝑋))) = (𝑀‘𝑋)) | ||
Theorem | 2polvalN 34218 | Value of double polarity. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘𝑋)) = (𝑀‘(𝑈‘𝑋))) | ||
Theorem | 2polssN 34219 | 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 34220 | Triple polarity cancels to a single polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → ( ⊥ ‘( ⊥ ‘( ⊥ ‘𝑆))) = ( ⊥ ‘𝑆)) | ||
Theorem | polcon3N 34221 | Contraposition law for polarity. Remark in [Holland95] p. 223. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ 𝑌) → ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | 2polcon4bN 34222 | Contraposition law for polarity. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (( ⊥ ‘( ⊥ ‘𝑋)) ⊆ ( ⊥ ‘( ⊥ ‘𝑌)) ↔ ( ⊥ ‘𝑌) ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | polcon2N 34223 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → 𝑌 ⊆ ( ⊥ ‘𝑋)) | ||
Theorem | polcon2bN 34224 | Contraposition law for polarity. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) → (𝑋 ⊆ ( ⊥ ‘𝑌) ↔ 𝑌 ⊆ ( ⊥ ‘𝑋))) | ||
Theorem | pclss2polN 34225 | 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 34226 | The projective subspace closure of the empty subspace. (Contributed by NM, 12-Sep-2013.) (New usage is discouraged.) |
⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → (𝑈‘∅) = ∅) | ||
Theorem | pcl0bN 34227 | The projective subspace closure of the empty subspace. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ⊆ 𝐴) → ((𝑈‘𝑃) = ∅ ↔ 𝑃 = ∅)) | ||
Theorem | pmaplubN 34228 | 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 34229 | 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 34230 | Double projective map of an LUB. (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴) → (𝑀‘(𝑈‘(𝑀‘(𝑈‘𝑆)))) = (𝑀‘(𝑈‘𝑆))) | ||
Theorem | paddunN 34231 | 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 6107.) (Contributed by NM, 6-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = ( ⊥ ‘(𝑆 ∪ 𝑇))) | ||
Theorem | poldmj1N 34232 | De Morgan's law for polarity of projective sum. (oldmj1 33526 analog.) (Contributed by NM, 7-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐴 ∧ 𝑇 ⊆ 𝐴) → ( ⊥ ‘(𝑆 + 𝑇)) = (( ⊥ ‘𝑆) ∩ ( ⊥ ‘𝑇))) | ||
Theorem | pmapj2N 34233 | 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 34234 | 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 34235 | 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 34236 | 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 34237 | 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 34238 | Extend class notation with set of all closed projective subspaces for a Hilbert lattice. |
class PSubCl | ||
Definition | df-psubclN 34239* | 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 34240* | The set of closed projective subspaces in a Hilbert lattice. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝐶 = {𝑠 ∣ (𝑠 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑠)) = 𝑠)}) | ||
Theorem | ispsubclN 34241 | The predicate "is a closed projective subspace". (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑋 ∈ 𝐶 ↔ (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋))) | ||
Theorem | psubcliN 34242 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → (𝑋 ⊆ 𝐴 ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋)) | ||
Theorem | psubcli2N 34243 | Property of a closed projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) | ||
Theorem | psubclsubN 34244 | A closed projective subspace is a projective subspace. (Contributed by NM, 23-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑆 = (PSubSp‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶) → 𝑋 ∈ 𝑆) | ||
Theorem | psubclssatN 34245 | A closed projective subspace is a set of atoms. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑋 ∈ 𝐶) → 𝑋 ⊆ 𝐴) | ||
Theorem | pmapidclN 34246 | 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 34247 | The empty set is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∅ ∈ 𝐶) | ||
Theorem | 1psubclN 34248 | 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 34249 | 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 34250 | 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 34251* | 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 34252 | The intersection of two closed subspaces is closed. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) → (𝑋 ∩ 𝑌) ∈ 𝐶) | ||
Theorem | paddatclN 34253 | 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 34254 | The projective subspace closure of a finite set of atoms is a closed subspace. Compare the (non-closed) subspace version pclfinN 34204 and also pclcmpatN 34205. (Contributed by NM, 13-Sep-2013.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑈 = (PCl‘𝐾) & ⊢ 𝑆 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑋 ∈ Fin) → (𝑈‘𝑋) ∈ 𝑆) | ||
Theorem | linepsubclN 34255 | A line is a closed projective subspace. (Contributed by NM, 25-Jan-2012.) (New usage is discouraged.) |
⊢ 𝑁 = (Lines‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝑁) → 𝑋 ∈ 𝐶) | ||
Theorem | polsubclN 34256 | A polarity is a closed projective subspace. (Contributed by NM, 24-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) → ( ⊥ ‘𝑋) ∈ 𝐶) | ||
Theorem | poml4N 34257 | 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 34258 | Orthomodular law for projective lattices. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ ( ⊥ ‘𝑌))) ∩ ( ⊥ ‘𝑌)) = ( ⊥ ‘( ⊥ ‘𝑋))) | ||
Theorem | poml6N 34259 | Orthomodular law for projective lattices. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ 𝑋 ⊆ 𝑌) → (( ⊥ ‘(( ⊥ ‘𝑋) ∩ 𝑌)) ∩ 𝑌) = 𝑋) | ||
Theorem | osumcllem1N 34260 | Lemma for osumclN 34271. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → (𝑈 ∩ 𝑀) = 𝑀) | ||
Theorem | osumcllem2N 34261 | Lemma for osumclN 34271. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝑈) → 𝑋 ⊆ (𝑈 ∩ 𝑀)) | ||
Theorem | osumcllem3N 34262 | Lemma for osumclN 34271. (Contributed by NM, 23-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑌 ∈ 𝐶 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) → (( ⊥ ‘𝑋) ∩ 𝑈) = 𝑌) | ||
Theorem | osumcllem4N 34263 | Lemma for osumclN 34271. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑌 ⊆ 𝐴 ∧ 𝑋 ⊆ ( ⊥ ‘𝑌)) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌)) → 𝑞 ≠ 𝑟) | ||
Theorem | osumcllem5N 34264 | Lemma for osumclN 34271. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
Theorem | osumcllem6N 34265 | Lemma for osumclN 34271. Use atom exchange hlatexch1 33699 to swap 𝑝 and 𝑞. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ 𝑌 ∧ 𝑞 ≤ (𝑟 ∨ 𝑝))) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
Theorem | osumcllem7N 34266* | Lemma for osumclN 34271. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ 𝑞 ∈ (𝑌 ∩ 𝑀)) → 𝑝 ∈ (𝑋 + 𝑌)) | ||
Theorem | osumcllem8N 34267 | Lemma for osumclN 34271. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝐴) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → (𝑌 ∩ 𝑀) = ∅) | ||
Theorem | osumcllem9N 34268 | Lemma for osumclN 34271. (Contributed by NM, 24-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅ ∧ 𝑝 ∈ 𝑈) ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 = 𝑋) | ||
Theorem | osumcllem10N 34269 | Lemma for osumclN 34271. Contradict osumcllem9N 34268. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) & ⊢ 𝑈 = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌))) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑌 ⊆ 𝐴) ∧ 𝑝 ∈ 𝐴 ∧ ¬ 𝑝 ∈ (𝑋 + 𝑌)) → 𝑀 ≠ 𝑋) | ||
Theorem | osumcllem11N 34270 | Lemma for osumclN 34271. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝐶 = (PSubCl‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐶 ∧ 𝑌 ∈ 𝐶) ∧ (𝑋 ⊆ ( ⊥ ‘𝑌) ∧ 𝑋 ≠ ∅)) → (𝑋 + 𝑌) = ( ⊥ ‘( ⊥ ‘(𝑋 + 𝑌)))) | ||
Theorem | osumclN 34271 | 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 34272 | For orthogonal elements, projective map of join equals projective sum. Compare pmapjoin 34156 where only one direction holds. (Contributed by NM, 11-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝑀 = (pmap‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ ( ⊥ ‘𝑌)) → (𝑀‘(𝑋 ∨ 𝑌)) = ((𝑀‘𝑋) + (𝑀‘𝑌))) | ||
Theorem | pexmidN 34273 | Excluded middle law for closed projective subspaces, which can be shown to be equivalent to (and derivable from) the orthomodular law poml4N 34257. Lemma 3.3(2) in [Holland95] p. 215, which we prove as a special case of osumclN 34271. (Contributed by NM, 25-Mar-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴) ∧ ( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋) → (𝑋 + ( ⊥ ‘𝑋)) = 𝐴) | ||
Theorem | pexmidlem1N 34274 | Lemma for pexmidN 34273. 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 34275 | Lemma for pexmidN 34273. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋) ∧ 𝑝 ≤ (𝑟 ∨ 𝑞))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
Theorem | pexmidlem3N 34276 | Lemma for pexmidN 34273. Use atom exchange hlatexch1 33699 to swap 𝑝 and 𝑞. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑟 ∈ 𝑋 ∧ 𝑞 ∈ ( ⊥ ‘𝑋)) ∧ 𝑞 ≤ (𝑟 ∨ 𝑝)) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
Theorem | pexmidlem4N 34277* | Lemma for pexmidN 34273. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ 𝑞 ∈ (( ⊥ ‘𝑋) ∩ 𝑀))) → 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋))) | ||
Theorem | pexmidlem5N 34278 | Lemma for pexmidN 34273. (Contributed by NM, 2-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → (( ⊥ ‘𝑋) ∩ 𝑀) = ∅) | ||
Theorem | pexmidlem6N 34279 | Lemma for pexmidN 34273. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 = 𝑋) | ||
Theorem | pexmidlem7N 34280 | Lemma for pexmidN 34273. Contradict pexmidlem6N 34279. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ + = (+𝑃‘𝐾) & ⊢ ⊥ = (⊥𝑃‘𝐾) & ⊢ 𝑀 = (𝑋 + {𝑝}) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ⊆ 𝐴 ∧ 𝑝 ∈ 𝐴) ∧ (( ⊥ ‘( ⊥ ‘𝑋)) = 𝑋 ∧ 𝑋 ≠ ∅ ∧ ¬ 𝑝 ∈ (𝑋 + ( ⊥ ‘𝑋)))) → 𝑀 ≠ 𝑋) | ||
Theorem | pexmidlem8N 34281 | Lemma for pexmidN 34273. The contradiction of pexmidlem6N 34279 and pexmidlem7N 34280 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 34282 | Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 34257. 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 34283 | Lemma for pl42N 34287. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) = (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)))) | ||
Theorem | pl42lem2N 34284 | Lemma for pl42N 34287. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((𝐹‘𝑋) + (𝐹‘𝑌)) + (((𝐹‘𝑋) + (𝐹‘𝑊)) ∩ ((𝐹‘𝑌) + (𝐹‘𝑉)))) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉))))) | ||
Theorem | pl42lem3N 34285 | Lemma for pl42N 34287. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → (((((𝐹‘𝑋) + (𝐹‘𝑌)) ∩ (𝐹‘𝑍)) + (𝐹‘𝑊)) ∩ (𝐹‘𝑉)) ⊆ ((((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑊)) ∩ (((𝐹‘𝑋) + (𝐹‘𝑌)) + (𝐹‘𝑉)))) | ||
Theorem | pl42lem4N 34286 | Lemma for pl42N 34287. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐹 = (pmap‘𝐾) & ⊢ + = (+𝑃‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵 ∧ 𝑉 ∈ 𝐵)) → ((𝑋 ≤ ( ⊥ ‘𝑌) ∧ 𝑍 ≤ ( ⊥ ‘𝑊)) → (𝐹‘((((𝑋 ∨ 𝑌) ∧ 𝑍) ∨ 𝑊) ∧ 𝑉)) ⊆ (𝐹‘((𝑋 ∨ 𝑌) ∨ ((𝑋 ∨ 𝑊) ∧ (𝑌 ∨ 𝑉)))))) | ||
Theorem | pl42N 34287 | 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 34288 | Extend class notation with set of all co-atoms (lattice hyperplanes). |
class LHyp | ||
Syntax | claut 34289 | Extend class notation with set of all lattice automorphisms. |
class LAut | ||
Syntax | cwpointsN 34290 | Extend class notation with W points. |
class WAtoms | ||
Syntax | cpautN 34291 | Extend class notation with set of all projective automorphisms. |
class PAut | ||
Definition | df-lhyp 34292* | 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 34293* | 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 34294* | 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 34295* | 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 34296* | The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) & ⊢ 𝑊 = (WAtoms‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐵 → 𝑊 = (𝑑 ∈ 𝐴 ↦ (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝑑})))) | ||
Theorem | watvalN 34297 | Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) & ⊢ 𝑊 = (WAtoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑊‘𝐷) = (𝐴 ∖ ((⊥𝑃‘𝐾)‘{𝐷}))) | ||
Theorem | iswatN 34298 | The predicate "is a W atom" (corresponding to fiducial atom 𝐷). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝑃 = (⊥𝑃‘𝐾) & ⊢ 𝑊 = (WAtoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐵 ∧ 𝐷 ∈ 𝐴) → (𝑃 ∈ (𝑊‘𝐷) ↔ (𝑃 ∈ 𝐴 ∧ ¬ 𝑃 ∈ ((⊥𝑃‘𝐾)‘{𝐷})))) | ||
Theorem | lhpset 34299* | The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐻 = {𝑤 ∈ 𝐵 ∣ 𝑤𝐶 1 }) | ||
Theorem | islhp 34300 | The predicate "is a co-atom (lattice hyperplane)." (Contributed by NM, 11-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐻 = (LHyp‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → (𝑊 ∈ 𝐻 ↔ (𝑊 ∈ 𝐵 ∧ 𝑊𝐶 1 ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |