| Metamath
Proof Explorer Theorem List (p. 393 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 | oplecon3b 39201 | Contraposition law for orthoposets. (chsscon3 31519 analog.) (Contributed by NM, 4-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ ( ⊥ ‘𝑋))) | ||
| Theorem | oplecon1b 39202 | Contraposition law for strict ordering in orthoposets. (chsscon1 31520 analog.) (Contributed by NM, 6-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) ≤ 𝑌 ↔ ( ⊥ ‘𝑌) ≤ 𝑋)) | ||
| Theorem | opoc1 39203 | Orthocomplement of orthoposet unity. (Contributed by NM, 24-Jan-2012.) |
| ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 1 ) = 0 ) | ||
| Theorem | opoc0 39204 | Orthocomplement of orthoposet zero. (Contributed by NM, 24-Jan-2012.) |
| ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OP → ( ⊥ ‘ 0 ) = 1 ) | ||
| Theorem | opltcon3b 39205 | Contraposition law for strict ordering in orthoposets. (chpsscon3 31522 analog.) (Contributed by NM, 4-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 ↔ ( ⊥ ‘𝑌) < ( ⊥ ‘𝑋))) | ||
| Theorem | opltcon1b 39206 | Contraposition law for strict ordering in orthoposets. (chpsscon1 31523 analog.) (Contributed by NM, 5-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (( ⊥ ‘𝑋) < 𝑌 ↔ ( ⊥ ‘𝑌) < 𝑋)) | ||
| Theorem | opltcon2b 39207 | Contraposition law for strict ordering in orthoposets. (chsscon2 31521 analog.) (Contributed by NM, 5-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < ( ⊥ ‘𝑌) ↔ 𝑌 < ( ⊥ ‘𝑋))) | ||
| Theorem | opexmid 39208 | Law of excluded middle for orthoposets. (chjo 31534 analog.) (Contributed by NM, 13-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ ( ⊥ ‘𝑋)) = 1 ) | ||
| Theorem | opnoncon 39209 | Law of contradiction for orthoposets. (chocin 31514 analog.) (Contributed by NM, 13-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ ( ⊥ ‘𝑋)) = 0 ) | ||
| Theorem | riotaocN 39210* | The orthocomplement of the unique poset element such that 𝜓. (riotaneg 12247 analog.) (Contributed by NM, 16-Jan-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ (𝑥 = ( ⊥ ‘𝑦) → (𝜑 ↔ 𝜓)) ⇒ ⊢ ((𝐾 ∈ OP ∧ ∃!𝑥 ∈ 𝐵 𝜑) → (℩𝑥 ∈ 𝐵 𝜑) = ( ⊥ ‘(℩𝑦 ∈ 𝐵 𝜓))) | ||
| Theorem | cmtfvalN 39211* | Value of commutes relation. (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {〈𝑥, 𝑦〉 ∣ (𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵 ∧ 𝑥 = ((𝑥 ∧ 𝑦) ∨ (𝑥 ∧ ( ⊥ ‘𝑦))))}) | ||
| Theorem | cmtvalN 39212 | Equivalence for commutes relation. Definition of commutes in [Kalmbach] p. 20. (cmbr 31603 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ ( ⊥ ‘𝑌))))) | ||
| Theorem | isolat 39213 | The predicate "is an ortholattice." (Contributed by NM, 18-Sep-2011.) |
| ⊢ (𝐾 ∈ OL ↔ (𝐾 ∈ Lat ∧ 𝐾 ∈ OP)) | ||
| Theorem | ollat 39214 | An ortholattice is a lattice. (Contributed by NM, 18-Sep-2011.) |
| ⊢ (𝐾 ∈ OL → 𝐾 ∈ Lat) | ||
| Theorem | olop 39215 | An ortholattice is an orthoposet. (Contributed by NM, 18-Sep-2011.) |
| ⊢ (𝐾 ∈ OL → 𝐾 ∈ OP) | ||
| Theorem | olposN 39216 | An ortholattice is a poset. (Contributed by NM, 16-Oct-2011.) (New usage is discouraged.) |
| ⊢ (𝐾 ∈ OL → 𝐾 ∈ Poset) | ||
| Theorem | isolatiN 39217 | Properties that determine an ortholattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
| ⊢ 𝐾 ∈ Lat & ⊢ 𝐾 ∈ OP ⇒ ⊢ 𝐾 ∈ OL | ||
| Theorem | oldmm1 39218 | De Morgan's law for meet in an ortholattice. (chdmm1 31544 analog.) (Contributed by NM, 6-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ 𝑌)) = (( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) | ||
| Theorem | oldmm2 39219 | De Morgan's law for meet in an ortholattice. (chdmm2 31545 analog.) (Contributed by NM, 6-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) = (𝑋 ∨ ( ⊥ ‘𝑌))) | ||
| Theorem | oldmm3N 39220 | De Morgan's law for meet in an ortholattice. (chdmm3 31546 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∧ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∨ 𝑌)) | ||
| Theorem | oldmm4 39221 | De Morgan's law for meet in an ortholattice. (chdmm4 31547 analog.) (Contributed by NM, 6-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) = (𝑋 ∨ 𝑌)) | ||
| Theorem | oldmj1 39222 | De Morgan's law for join in an ortholattice. (chdmj1 31548 analog.) (Contributed by NM, 6-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ 𝑌)) = (( ⊥ ‘𝑋) ∧ ( ⊥ ‘𝑌))) | ||
| Theorem | oldmj2 39223 | De Morgan's law for join in an ortholattice. (chdmj2 31549 analog.) (Contributed by NM, 7-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ ( ⊥ ‘𝑌))) | ||
| Theorem | oldmj3 39224 | De Morgan's law for join in an ortholattice. (chdmj3 31550 analog.) (Contributed by NM, 7-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(𝑋 ∨ ( ⊥ ‘𝑌))) = (( ⊥ ‘𝑋) ∧ 𝑌)) | ||
| Theorem | oldmj4 39225 | De Morgan's law for join in an ortholattice. (chdmj4 31551 analog.) (Contributed by NM, 7-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ( ⊥ ‘(( ⊥ ‘𝑋) ∨ ( ⊥ ‘𝑌))) = (𝑋 ∧ 𝑌)) | ||
| Theorem | olj01 39226 | An ortholattice element joined with zero equals itself. (chj0 31516 analog.) (Contributed by NM, 19-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∨ 0 ) = 𝑋) | ||
| Theorem | olj02 39227 | An ortholattice element joined with zero equals itself. (Contributed by NM, 28-Jan-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∨ 𝑋) = 𝑋) | ||
| Theorem | olm11 39228 | The meet of an ortholattice element with one equals itself. (chm1i 31475 analog.) (Contributed by NM, 22-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 1 ) = 𝑋) | ||
| Theorem | olm12 39229 | The meet of an ortholattice element with one equals itself. (Contributed by NM, 22-May-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 1 ∧ 𝑋) = 𝑋) | ||
| Theorem | latmassOLD 39230 | Ortholattice meet is associative. (This can also be proved for lattices with a longer proof.) (inass 4228 analog.) (Contributed by NM, 7-Nov-2011.) (Proof modification is discouraged.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = (𝑋 ∧ (𝑌 ∧ 𝑍))) | ||
| Theorem | latm12 39231 | A rearrangement of lattice meet. (in12 4229 analog.) (Contributed by NM, 8-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = (𝑌 ∧ (𝑋 ∧ 𝑍))) | ||
| Theorem | latm32 39232 | A rearrangement of lattice meet. (in12 4229 analog.) (Contributed by NM, 13-Nov-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ 𝑌)) | ||
| Theorem | latmrot 39233 | Rotate lattice meet of 3 classes. (Contributed by NM, 9-Oct-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑍 ∧ 𝑋) ∧ 𝑌)) | ||
| Theorem | latm4 39234 | Rearrangement of lattice meet of 4 classes. (in4 4234 analog.) (Contributed by NM, 8-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (𝑍 ∈ 𝐵 ∧ 𝑊 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ (𝑍 ∧ 𝑊)) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑊))) | ||
| Theorem | latmmdiN 39235 | Lattice meet distributes over itself. (inindi 4235 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → (𝑋 ∧ (𝑌 ∧ 𝑍)) = ((𝑋 ∧ 𝑌) ∧ (𝑋 ∧ 𝑍))) | ||
| Theorem | latmmdir 39236 | Lattice meet distributes over itself. (inindir 4236 analog.) (Contributed by NM, 6-Jun-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 ∧ 𝑌) ∧ 𝑍) = ((𝑋 ∧ 𝑍) ∧ (𝑌 ∧ 𝑍))) | ||
| Theorem | olm01 39237 | Meet with lattice zero is zero. (chm0 31510 analog.) (Contributed by NM, 8-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → (𝑋 ∧ 0 ) = 0 ) | ||
| Theorem | olm02 39238 | Meet with lattice zero is zero. (Contributed by NM, 9-Oct-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OL ∧ 𝑋 ∈ 𝐵) → ( 0 ∧ 𝑋) = 0 ) | ||
| Theorem | isoml 39239* | The predicate "is an orthomodular lattice." (Contributed by NM, 18-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ (𝐾 ∈ OML ↔ (𝐾 ∈ OL ∧ ∀𝑥 ∈ 𝐵 ∀𝑦 ∈ 𝐵 (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥)))))) | ||
| Theorem | isomliN 39240* | Properties that determine an orthomodular lattice. (Contributed by NM, 18-Sep-2011.) (New usage is discouraged.) |
| ⊢ 𝐾 ∈ OL & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) → (𝑥 ≤ 𝑦 → 𝑦 = (𝑥 ∨ (𝑦 ∧ ( ⊥ ‘𝑥))))) ⇒ ⊢ 𝐾 ∈ OML | ||
| Theorem | omlol 39241 | An orthomodular lattice is an ortholattice. (Contributed by NM, 18-Sep-2011.) |
| ⊢ (𝐾 ∈ OML → 𝐾 ∈ OL) | ||
| Theorem | omlop 39242 | An orthomodular lattice is an orthoposet. (Contributed by NM, 6-Nov-2011.) |
| ⊢ (𝐾 ∈ OML → 𝐾 ∈ OP) | ||
| Theorem | omllat 39243 | An orthomodular lattice is a lattice. (Contributed by NM, 6-Nov-2011.) |
| ⊢ (𝐾 ∈ OML → 𝐾 ∈ Lat) | ||
| Theorem | omllaw 39244 | The orthomodular law. (Contributed by NM, 18-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑌 = (𝑋 ∨ (𝑌 ∧ ( ⊥ ‘𝑋))))) | ||
| Theorem | omllaw2N 39245 | Variation of orthomodular law. Definition of OML law in [Kalmbach] p. 22. (pjoml2i 31604 analog.) (Contributed by NM, 6-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ 𝑌)) = 𝑌)) | ||
| Theorem | omllaw3 39246 | Orthomodular law equivalent. Theorem 2(ii) of [Kalmbach] p. 22. (pjoml 31455 analog.) (Contributed by NM, 19-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 0 = (0.‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ≤ 𝑌 ∧ (𝑌 ∧ ( ⊥ ‘𝑋)) = 0 ) → 𝑋 = 𝑌)) | ||
| Theorem | omllaw4 39247 | Orthomodular law equivalent. Remark in [Holland95] p. 223. (Contributed by NM, 19-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → (( ⊥ ‘(( ⊥ ‘𝑋) ∧ 𝑌)) ∧ 𝑌) = 𝑋)) | ||
| Theorem | omllaw5N 39248 | The orthomodular law. Remark in [Kalmbach] p. 22. (pjoml5 31632 analog.) (Contributed by NM, 14-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ∨ (( ⊥ ‘𝑋) ∧ (𝑋 ∨ 𝑌))) = (𝑋 ∨ 𝑌)) | ||
| Theorem | cmtcomlemN 39249 | Lemma for cmtcomN 39250. (cmcmlem 31610 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 → 𝑌𝐶𝑋)) | ||
| Theorem | cmtcomN 39250 | Commutation is symmetric. Theorem 2(v) in [Kalmbach] p. 22. (cmcmi 31611 analog.) (Contributed by NM, 7-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑌𝐶𝑋)) | ||
| Theorem | cmt2N 39251 | Commutation with orthocomplement. Theorem 2.3(i) of [Beran] p. 39. (cmcm2i 31612 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋𝐶( ⊥ ‘𝑌))) | ||
| Theorem | cmt3N 39252 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31614 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶𝑌)) | ||
| Theorem | cmt4N 39253 | Commutation with orthocomplement. Remark in [Kalmbach] p. 23. (cmcm4i 31614 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑋)𝐶( ⊥ ‘𝑌))) | ||
| Theorem | cmtbr2N 39254 | Alternate definition of the commutes relation. Remark in [Kalmbach] p. 23. (cmbr2i 31615 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ 𝑋 = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ ( ⊥ ‘𝑌))))) | ||
| Theorem | cmtbr3N 39255 | Alternate definition for the commutes relation. Lemma 3 of [Kalmbach] p. 23. (cmbr3 31627 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) = (𝑋 ∧ 𝑌))) | ||
| Theorem | cmtbr4N 39256 | Alternate definition for the commutes relation. (cmbr4i 31620 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 ∧ (( ⊥ ‘𝑋) ∨ 𝑌)) ≤ 𝑌)) | ||
| Theorem | lecmtN 39257 | Ordered elements commute. (lecmi 31621 analog.) (Contributed by NM, 10-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 → 𝑋𝐶𝑌)) | ||
| Theorem | cmtidN 39258 | Any element commutes with itself. (cmidi 31629 analog.) (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ 𝑋 ∈ 𝐵) → 𝑋𝐶𝑋) | ||
| Theorem | omlfh1N 39259 | 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 31637 analog.) (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∧ (𝑌 ∨ 𝑍)) = ((𝑋 ∧ 𝑌) ∨ (𝑋 ∧ 𝑍))) | ||
| Theorem | omlfh3N 39260 | Foulis-Holland Theorem, part 3. Dual of omlfh1N 39259. (Contributed by NM, 8-Nov-2011.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋𝐶𝑌 ∧ 𝑋𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ (𝑋 ∨ 𝑍))) | ||
| Theorem | omlmod1i2N 39261 | Analogue of modular law atmod1i2 39861 that holds in any OML. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = (cm‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ (𝑋 ≤ 𝑍 ∧ 𝑌𝐶𝑍)) → (𝑋 ∨ (𝑌 ∧ 𝑍)) = ((𝑋 ∨ 𝑌) ∧ 𝑍)) | ||
| Theorem | omlspjN 39262 | Contraction of a Sasaki projection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ OML ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 ≤ 𝑌) → ((𝑋 ∨ ( ⊥ ‘𝑌)) ∧ 𝑌) = 𝑋) | ||
| Syntax | ccvr 39263 | Extend class notation with covers relation. |
| class ⋖ | ||
| Syntax | catm 39264 | Extend class notation with atoms. |
| class Atoms | ||
| Syntax | cal 39265 | Extend class notation with atomic lattices. |
| class AtLat | ||
| Syntax | clc 39266 | Extend class notation with lattices with the covering property. |
| class CvLat | ||
| Definition | df-covers 39267* | 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 39270 for the relation form. (Contributed by NM, 18-Sep-2011.) |
| ⊢ ⋖ = (𝑝 ∈ V ↦ {〈𝑎, 𝑏〉 ∣ ((𝑎 ∈ (Base‘𝑝) ∧ 𝑏 ∈ (Base‘𝑝)) ∧ 𝑎(lt‘𝑝)𝑏 ∧ ¬ ∃𝑧 ∈ (Base‘𝑝)(𝑎(lt‘𝑝)𝑧 ∧ 𝑧(lt‘𝑝)𝑏))}) | ||
| Definition | df-ats 39268* | Define the class of poset atoms. (Contributed by NM, 18-Sep-2011.) |
| ⊢ Atoms = (𝑝 ∈ V ↦ {𝑎 ∈ (Base‘𝑝) ∣ (0.‘𝑝)( ⋖ ‘𝑝)𝑎}) | ||
| Theorem | cvrfval 39269* | Value of covers relation "is covered by". (Contributed by NM, 18-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐴 → 𝐶 = {〈𝑥, 𝑦〉 ∣ ((𝑥 ∈ 𝐵 ∧ 𝑦 ∈ 𝐵) ∧ 𝑥 < 𝑦 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑥 < 𝑧 ∧ 𝑧 < 𝑦))}) | ||
| Theorem | cvrval 39270* | 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 32301 analog.) (Contributed by NM, 18-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ¬ ∃𝑧 ∈ 𝐵 (𝑋 < 𝑧 ∧ 𝑧 < 𝑌)))) | ||
| Theorem | cvrlt 39271 | The covers relation implies the less-than relation. (cvpss 32304 analog.) (Contributed by NM, 8-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 < 𝑌) | ||
| Theorem | cvrnbtwn 39272 | There is no element between the two arguments of the covers relation. (cvnbtwn 32305 analog.) (Contributed by NM, 18-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ¬ (𝑋 < 𝑍 ∧ 𝑍 < 𝑌)) | ||
| Theorem | ncvr1 39273 | No element covers the lattice unity. (Contributed by NM, 8-Jul-2013.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵) → ¬ 1 𝐶𝑋) | ||
| Theorem | cvrletrN 39274 | Property of an element above a covering. (Contributed by NM, 7-Dec-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌 ≤ 𝑍) → 𝑋 < 𝑍)) | ||
| Theorem | cvrval2 39275* | Binary relation expressing 𝑌 covers 𝑋. Definition of covers in [Kalmbach] p. 15. (cvbr2 32302 analog.) (Contributed by NM, 16-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∀𝑧 ∈ 𝐵 ((𝑋 < 𝑧 ∧ 𝑧 ≤ 𝑌) → 𝑧 = 𝑌)))) | ||
| Theorem | cvrnbtwn2 39276 | The covers relation implies no in-betweenness. (cvnbtwn2 32306 analog.) (Contributed by NM, 17-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 < 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ 𝑍 = 𝑌)) | ||
| Theorem | cvrnbtwn3 39277 | The covers relation implies no in-betweenness. (cvnbtwn3 32307 analog.) (Contributed by NM, 4-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 < 𝑌) ↔ 𝑋 = 𝑍)) | ||
| Theorem | cvrcon3b 39278 | Contraposition law for the covers relation. (cvcon3 32303 analog.) (Contributed by NM, 4-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ( ⊥ ‘𝑌)𝐶( ⊥ ‘𝑋))) | ||
| Theorem | cvrle 39279 | The covers relation implies the "less than or equal to" relation. (Contributed by NM, 12-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≤ 𝑌) | ||
| Theorem | cvrnbtwn4 39280 | The covers relation implies no in-betweenness. Part of proof of Lemma 7.5.1 of [MaedaMaeda] p. 31. (cvnbtwn4 32308 analog.) (Contributed by NM, 18-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ Poset ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → ((𝑋 ≤ 𝑍 ∧ 𝑍 ≤ 𝑌) ↔ (𝑋 = 𝑍 ∨ 𝑍 = 𝑌))) | ||
| Theorem | cvrnle 39281 | 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 39282 | The covers relation implies inequality. (Contributed by NM, 13-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ (((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋𝐶𝑌) → 𝑋 ≠ 𝑌) | ||
| Theorem | cvrnrefN 39283 | The covers relation is not reflexive. (cvnref 32310 analog.) (Contributed by NM, 1-Nov-2012.) (New usage is discouraged.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) → ¬ 𝑋𝐶𝑋) | ||
| Theorem | cvrcmp 39284 | 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 39285 | 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 39286* | The set of atoms in a poset. (Contributed by NM, 18-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → 𝐴 = {𝑥 ∈ 𝐵 ∣ 0 𝐶𝑥}) | ||
| Theorem | isat 39287 | The predicate "is an atom". (ela 32358 analog.) (Contributed by NM, 18-Sep-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ 𝐷 → (𝑃 ∈ 𝐴 ↔ (𝑃 ∈ 𝐵 ∧ 0 𝐶𝑃))) | ||
| Theorem | isat2 39288 | The predicate "is an atom". (elatcv0 32360 analog.) (Contributed by NM, 18-Jun-2012.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐵) → (𝑃 ∈ 𝐴 ↔ 0 𝐶𝑃)) | ||
| Theorem | atcvr0 39289 | An atom covers zero. (atcv0 32361 analog.) (Contributed by NM, 4-Nov-2011.) |
| ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐷 ∧ 𝑃 ∈ 𝐴) → 0 𝐶𝑃) | ||
| Theorem | atbase 39290 | An atom is a member of the lattice base set (i.e. a lattice element). (atelch 32363 analog.) (Contributed by NM, 10-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝑃 ∈ 𝐴 → 𝑃 ∈ 𝐵) | ||
| Theorem | atssbase 39291 | The set of atoms is a subset of the base set. (atssch 32362 analog.) (Contributed by NM, 21-Oct-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ 𝐴 ⊆ 𝐵 | ||
| Theorem | 0ltat 39292 | An atom is greater than zero. (Contributed by NM, 4-Jul-2012.) |
| ⊢ 0 = (0.‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑃 ∈ 𝐴) → 0 < 𝑃) | ||
| Theorem | leatb 39293 | A poset element less than or equal to an atom equals either zero or the atom. (atss 32365 analog.) (Contributed by NM, 17-Nov-2011.) |
| ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ OP ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 ≤ 𝑃 ↔ (𝑋 = 𝑃 ∨ 𝑋 = 0 ))) | ||
| Theorem | leat 39294 | 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 39295 | 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 39296 | 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 39297 | 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 39298 | 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 39299* | 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 39300* | 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 → ∃𝑦 ∈ 𝐴 𝑦 ≤ 𝑥))) | ||
| < Previous Next > |
| Copyright terms: Public domain | < Previous Next > |