Home | Metamath
Proof Explorer Theorem List (p. 365 of 450) | < 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-28695) |
Hilbert Space Explorer
(28696-30218) |
Users' Mathboxes
(30219-44926) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cmt2N 36401 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 29370 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌))) | ||
Theorem | cmt3N 36402 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 29372 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌)) | ||
Theorem | cmt4N 36403 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 29372 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶( ⊥ ‘𝑌))) | ||
Theorem | cmtbr2N 36404 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 29373 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ ( ⊥ ‘𝑌))))) | ||
Theorem | cmtbr3N 36405 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 29385 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌))) | ||
Theorem | cmtbr4N 36406 | Alternate definition for the commutes relation. (cmbr4i 29378 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) ≤ 𝑌)) | ||
Theorem | lecmtN 36407 | Ordered elements commute. (lecmi 29379 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌)) | ||
Theorem | cmtidN 36408 | Any element commutes with itself. (cmidi 29387 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → 𝑋𝐶𝑋) | ||
Theorem | omlfh1N 36409 | Foulis-Holland Theorem, part 1. If any 2 pairs in a triple of orthomodular lattice elements commute, the triple is distributive. Part of Theorem 5 in [Kalmbach] p. 25. (fh1 29395 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) | ||
Theorem | omlfh3N 36410 | Foulis-Holland Theorem, part 3. Dual of omlfh1N 36409. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍))) | ||
Theorem | omlmod1i2N 36411 | Analogue of modular law atmod1i2 37010 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ 𝑍)) | ||
Theorem | omlspjN 36412 | Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌) = 𝑋) | ||
Syntax | ccvr 36413 | Extend class notation with covers relation. |
class ⋖ | ||
Syntax | catm 36414 | Extend class notation with atoms. |
class Atoms | ||
Syntax | cal 36415 | Extend class notation with atomic lattices. |
class AtLat | ||
Syntax | clc 36416 | Extend class notation with lattices with the covering property. |
class CvLat | ||
Definition | df-covers 36417* | Define the covers relation ("is covered by") for posets. "𝑎 is covered by 𝑏 " means that 𝑎 is strictly less than 𝑏 and there is nothing in between. See cvrval 36420 for the relation form. (Contributed by NM, 18-Sep-2011.) |
⊢ ⋖ = (𝑝 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))}) | ||
Definition | df-ats 36418* | Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.) |
⊢ Atoms = (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎}) | ||
Theorem | cvrfval 36419* | Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 < 𝑦 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑥 < 𝑧 ∧ 𝑧 < 𝑦))}) | ||
Theorem | cvrval 36420* | Binary relation expressing 𝐵 covers 𝐴, which means that 𝐵 is larger than 𝐴 and there is nothing in between. Definition 3.2.18 of [PtakPulmannova] p. 68. (cvbr 30059 analog.) (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑋 < 𝑧 ∧ 𝑧 < 𝑌)))) | ||
Theorem | cvrlt 36421 | The covers relation implies the less-than relation. (cvpss 30062 analog.) (Contributed by NM, 8-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 < 𝑌) | ||
Theorem | cvrnbtwn 36422 | There is no element between the two arguments of the covers relation. (cvnbtwn 30063 analog.) (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ¬ (𝑋 < 𝑍 ∧ 𝑍 < 𝑌)) | ||
Theorem | ncvr1 36423 | No element covers the lattice unit. (Contributed by NM, 8-Jul-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ¬ 1 𝐶𝑋) | ||
Theorem | cvrletrN 36424 | Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍)) | ||
Theorem | cvrval2 36425* | Binary relation expressing 𝑌 covers 𝑋. Definition of covers in [Kalmbach] p. 15. (cvbr2 30060 analog.) (Contributed by NM, 16-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∀𝑧 ∈ 𝐵 ((𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌) → 𝑧 = 𝑌)))) | ||
Theorem | cvrnbtwn2 36426 | The covers relation implies no in-betweenness. (cvnbtwn2 30064 analog.) (Contributed by NM, 17-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 = 𝑌)) | ||
Theorem | cvrnbtwn3 36427 | The covers relation implies no in-betweenness. (cvnbtwn3 30065 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌) ↔ 𝑋 = 𝑍)) | ||
Theorem | cvrcon3b 36428 | Contraposition law for the covers relation. (cvcon3 30061 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑌)𝐶( ⊥ ‘𝑋))) | ||
Theorem | cvrle 36429 | The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≤ 𝑌) | ||
Theorem | cvrnbtwn4 36430 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 30066 analog.) (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ (𝑋 = 𝑍 ∨ 𝑍 = 𝑌))) | ||
Theorem | cvrnle 36431 | The covers relation implies the negation of the converse "less than or equal to" relation. (Contributed by NM, 18-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ Poset ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ¬ 𝑌 ≤ 𝑋) | ||
Theorem | cvrne 36432 | The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≠ 𝑌) | ||
Theorem | cvrnrefN 36433 | The covers relation is not reflexive. (cvnref 30068 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋𝐶𝑋) | ||
Theorem | cvrcmp 36434 | If two lattice elements that cover a third are comparable, then they are equal. (Contributed by NM, 6-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑍𝐶𝑋 ∧ 𝑍𝐶𝑌)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) | ||
Theorem | cvrcmp2 36435 | If two lattice elements covered by a third are comparable, then they are equal. (Contributed by NM, 20-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ≤ 𝑌 ↔ 𝑋 = 𝑌)) | ||
Theorem | pats 36436* | The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → 𝐴 = {𝑥 ∈ 𝐵 ∣ 0 𝐶𝑥}) | ||
Theorem | isat 36437 | The predicate "is an atom". (ela 30116 analog.) (Contributed by NM, 18-Sep-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 0 𝐶𝑃))) | ||
Theorem | isat2 36438 | The predicate "is an atom". (elatcv0 30118 analog.) (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ 0 𝐶𝑃)) | ||
Theorem | atcvr0 36439 | An atom covers zero. (atcv0 30119 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴) → 0 𝐶𝑃) | ||
Theorem | atbase 36440 | An atom is a member of the lattice base set (i.e. a lattice element). (atelch 30121 analog.) (Contributed by NM, 10-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) | ||
Theorem | atssbase 36441 | The set of atoms is a subset of the base set. (atssch 30120 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
Theorem | 0ltat 36442 | An atom is greater than zero. (Contributed by NM, 4-Jul-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴) → 0 < 𝑃) | ||
Theorem | leatb 36443 | A poset element less than or equal to an atom equals either zero or the atom. (atss 30123 analog.) (Contributed by NM, 17-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 ≤ 𝑃 ↔ (𝑋 = 𝑃 ∨ 𝑋 = 0 ))) | ||
Theorem | leat 36444 | A poset element less than or equal to an atom equals either zero or the atom. (Contributed by NM, 15-Oct-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ 𝑋 ≤ 𝑃) → (𝑋 = 𝑃 ∨ 𝑋 = 0 )) | ||
Theorem | leat2 36445 | A nonzero poset element less than or equal to an atom equals the atom. (Contributed by NM, 6-Mar-2013.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋 ≠ 0 ∧ 𝑋 ≤ 𝑃)) → 𝑋 = 𝑃) | ||
Theorem | leat3 36446 | A poset element less than or equal to an atom is either an atom or zero. (Contributed by NM, 2-Dec-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ 𝑋 ≤ 𝑃) → (𝑋 ∈ 𝐴 ∨ 𝑋 = 0 )) | ||
Theorem | meetat 36447 | The meet of any element with an atom is either the atom or zero. (Contributed by NM, 28-Aug-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 𝑃 ∨ (𝑋 ∧ 𝑃) = 0 )) | ||
Theorem | meetat2 36448 | The meet of any element with an atom is either the atom or zero. (Contributed by NM, 30-Aug-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) ∈ 𝐴 ∨ (𝑋 ∧ 𝑃) = 0 )) | ||
Definition | df-atl 36449* | Define the class of atomic lattices, in which every nonzero element is greater than or equal to an atom. We also ensure the existence of a lattice zero, since a lattice by itself may not have a zero. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.) |
⊢ AtLat = {𝑘 ∈ Lat ∣ ((Base‘𝑘) ∈ dom (glb‘𝑘) ∧ ∀𝑥 ∈ (Base‘𝑘)(𝑥 ≠ (0.‘𝑘) → ∃𝑝 ∈ (Atoms‘𝑘)𝑝(le‘𝑘)𝑥))} | ||
Theorem | isatl 36450* | The predicate "is an atomic lattice." Every nonzero element is less than or equal to an atom. (Contributed by NM, 18-Sep-2011.) (Revised by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ AtLat ↔ (𝐾 ∈ Lat ∧ 𝐵 ∈ dom 𝐺 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≠ 0 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))) | ||
Theorem | atllat 36451 | An atomic lattice is a lattice. (Contributed by NM, 21-Oct-2011.) |
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Lat) | ||
Theorem | atlpos 36452 | An atomic lattice is a poset. (Contributed by NM, 5-Nov-2012.) |
⊢ (𝐾 ∈ AtLat → 𝐾 ∈ Poset) | ||
Theorem | atl0dm 36453 | Condition necessary for zero element to exist. (Contributed by NM, 14-Sep-2018.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) ⇒ ⊢ (𝐾 ∈ AtLat → 𝐵 ∈ dom 𝐺) | ||
Theorem | atl0cl 36454 | An atomic lattice has a zero element. We can use this in place of op0cl 36335 for lattices without orthocomplements. (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ (𝐾 ∈ AtLat → 0 ∈ 𝐵) | ||
Theorem | atl0le 36455 | Orthoposet zero is less than or equal to any element. (ch0le 29218 analog.) (Contributed by NM, 12-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → 0 ≤ 𝑋) | ||
Theorem | atlle0 36456 | An element less than or equal to zero equals zero. (chle0 29220 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → (𝑋 ≤ 0 ↔ 𝑋 = 0 )) | ||
Theorem | atlltn0 36457 | A lattice element greater than zero is nonzero. (Contributed by NM, 1-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵) → ( 0 < 𝑋 ↔ 𝑋 ≠ 0 )) | ||
Theorem | isat3 36458* | The predicate "is an atom". (elat2 30117 analog.) (Contributed by NM, 27-Apr-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ AtLat → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 𝑃 ≠ 0 ∧ ∀𝑥 ∈ 𝐵 (𝑥 ≤ 𝑃 → (𝑥 = 𝑃 ∨ 𝑥 = 0 ))))) | ||
Theorem | atn0 36459 | An atom is not zero. (atne0 30122 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → 𝑃 ≠ 0 ) | ||
Theorem | atnle0 36460 | An atom is not less than or equal to zero. (Contributed by NM, 17-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴) → ¬ 𝑃 ≤ 0 ) | ||
Theorem | atlen0 36461 | A lattice element is nonzero if an atom is under it. (Contributed by NM, 26-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ 𝑃 ≤ 𝑋) → 𝑋 ≠ 0 ) | ||
Theorem | atcmp 36462 | If two atoms are comparable, they are equal. (atsseq 30124 analog.) (Contributed by NM, 13-Oct-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≤ 𝑄 ↔ 𝑃 = 𝑄)) | ||
Theorem | atncmp 36463 | Frequently-used variation of atcmp 36462. (Contributed by NM, 29-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑄 ↔ 𝑃 ≠ 𝑄)) | ||
Theorem | atnlt 36464 | Two atoms cannot satisfy the less than relation. (Contributed by NM, 7-Feb-2012.) |
⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃 < 𝑄) | ||
Theorem | atcvreq0 36465 | An element covered by an atom must be zero. (atcveq0 30125 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋𝐶𝑃 ↔ 𝑋 = 0 )) | ||
Theorem | atncvrN 36466 | Two atoms cannot satisfy the covering relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ¬ 𝑃𝐶𝑄) | ||
Theorem | atlex 36467* | Every nonzero element of an atomic lattice is greater than or equal to an atom. (hatomic 30137 analog.) (Contributed by NM, 21-Oct-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑋) | ||
Theorem | atnle 36468 | Two ways of expressing "an atom is not less than or equal to a lattice element." (atnssm0 30153 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → (¬ 𝑃 ≤ 𝑋 ↔ (𝑃 ∧ 𝑋) = 0 )) | ||
Theorem | atnem0 36469 | The meet of distinct atoms is zero. (atnemeq0 30154 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ AtLat ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ (𝑃 ∧ 𝑄) = 0 )) | ||
Theorem | atlatmstc 36470* | An atomic, complete, orthomodular lattice is atomistic i.e. every element is the join of the atoms under it. See remark before Proposition 1 in [Kalmbach] p. 140; also remark in [BeltramettiCassinelli] p. 98. (hatomistici 30139 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 1 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵) → ( 1 ‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋) | ||
Theorem | atlatle 36471* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 30148 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) | ||
Theorem | atlrelat1 36472* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 30140, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌))) | ||
Definition | df-cvlat 36473* | Define the class of atomic lattices with the covering property. (This is actually the exchange property, but they are equivalent. The literature usually uses the covering property terminology.) (Contributed by NM, 5-Nov-2012.) |
⊢ CvLat = {𝑘 ∈ AtLat ∣ ∀𝑎 ∈ (Atoms‘𝑘)∀𝑏 ∈ (Atoms‘𝑘)∀𝑐 ∈ (Base‘𝑘)((¬ 𝑎(le‘𝑘)𝑐 ∧ 𝑎(le‘𝑘)(𝑐(join‘𝑘)𝑏)) → 𝑏(le‘𝑘)(𝑐(join‘𝑘)𝑎))} | ||
Theorem | iscvlat 36474* | The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 ((¬ 𝑝 ≤ 𝑥 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝)))) | ||
Theorem | iscvlat2N 36475* | The predicate "is an atomic lattice with the covering (or exchange) property". (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ CvLat ↔ (𝐾 ∈ AtLat ∧ ∀𝑝 ∈ 𝐴 ∀𝑞 ∈ 𝐴 ∀𝑥 ∈ 𝐵 (((𝑝 ∧ 𝑥) = 0 ∧ 𝑝 ≤ (𝑥 ∨ 𝑞)) → 𝑞 ≤ (𝑥 ∨ 𝑝)))) | ||
Theorem | cvlatl 36476 | An atomic lattice with the covering property is an atomic lattice. (Contributed by NM, 5-Nov-2012.) |
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ AtLat) | ||
Theorem | cvllat 36477 | An atomic lattice with the covering property is a lattice. (Contributed by NM, 5-Nov-2012.) |
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Lat) | ||
Theorem | cvlposN 36478 | An atomic lattice with the covering property is a poset. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
⊢ (𝐾 ∈ CvLat → 𝐾 ∈ Poset) | ||
Theorem | cvlexch1 36479 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃))) | ||
Theorem | cvlexch2 36480 | An atomic covering lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋))) | ||
Theorem | cvlexchb1 36481 | An atomic covering lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄))) | ||
Theorem | cvlexchb2 36482 | An atomic covering lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋))) | ||
Theorem | cvlexch3 36483 | An atomic covering lattice has the exchange property. (atexch 30158 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃))) | ||
Theorem | cvlexch4N 36484 | An atomic covering lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 5-Nov-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄))) | ||
Theorem | cvlatexchb1 36485 | A version of cvlexchb1 36481 for atoms. (Contributed by NM, 5-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄))) | ||
Theorem | cvlatexchb2 36486 | A version of cvlexchb2 36482 for atoms. (Contributed by NM, 5-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) | ||
Theorem | cvlatexch1 36487 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃))) | ||
Theorem | cvlatexch2 36488 | Atom exchange property. (Contributed by NM, 5-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅))) | ||
Theorem | cvlatexch3 36489 | Atom exchange property. (Contributed by NM, 29-Nov-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≠ 𝑅)) → (𝑃 ≤ (𝑄 ∨ 𝑅) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))) | ||
Theorem | cvlcvr1 36490 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 30132 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | cvlcvrp 36491 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 30152 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | cvlatcvr1 36492 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄))) | ||
Theorem | cvlatcvr2 36493 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃))) | ||
Theorem | cvlsupr2 36494 | Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄. (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)))) | ||
Theorem | cvlsupr3 36495 | Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄, which can replace the superposition part of ishlat1 36503, (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ), with the simpler ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) as shown in ishlat3N 36505. (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑃 ≠ 𝑄 → (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))))) | ||
Theorem | cvlsupr4 36496 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | cvlsupr5 36497 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑃) | ||
Theorem | cvlsupr6 36498 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑄) | ||
Theorem | cvlsupr7 36499 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄)) | ||
Theorem | cvlsupr8 36500 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |