![]() |
Metamath
Proof Explorer Theorem List (p. 379 of 473) | < 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-29860) |
![]() (29861-31383) |
![]() (31384-47242) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cvlcvr1 37801 | The covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 31297 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | cvlcvrp 37802 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31317 analog.) (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | cvlatcvr1 37803 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄))) | ||
Theorem | cvlatcvr2 37804 | An atom is covered by its join with a different atom. (Contributed by NM, 5-Nov-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃))) | ||
Theorem | cvlsupr2 37805 | Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄. (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄)))) | ||
Theorem | cvlsupr3 37806 | Two equivalent ways of expressing that 𝑅 is a superposition of 𝑃 and 𝑄, which can replace the superposition part of ishlat1 37814, (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴(𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦)) ), with the simpler ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) as shown in ishlat3N 37816. (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅) ↔ (𝑃 ≠ 𝑄 → (𝑅 ≠ 𝑃 ∧ 𝑅 ≠ 𝑄 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))))) | ||
Theorem | cvlsupr4 37807 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | cvlsupr5 37808 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑃) | ||
Theorem | cvlsupr6 37809 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 9-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → 𝑅 ≠ 𝑄) | ||
Theorem | cvlsupr7 37810 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑄)) | ||
Theorem | cvlsupr8 37811 | Consequence of superposition condition (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅). (Contributed by NM, 24-Nov-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∨ = (join‘𝐾) ⇒ ⊢ ((𝐾 ∈ CvLat ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅)) | ||
Syntax | chlt 37812 | Extend class notation with Hilbert lattices. |
class HL | ||
Definition | df-hlat 37813* | Define the class of Hilbert lattices, which are complete, atomic lattices satisfying the superposition principle and minimum height. (Contributed by NM, 5-Nov-2012.) |
⊢ HL = {𝑙 ∈ ((OML ∩ CLat) ∩ CvLat) ∣ (∀𝑎 ∈ (Atoms‘𝑙)∀𝑏 ∈ (Atoms‘𝑙)(𝑎 ≠ 𝑏 → ∃𝑐 ∈ (Atoms‘𝑙)(𝑐 ≠ 𝑎 ∧ 𝑐 ≠ 𝑏 ∧ 𝑐(le‘𝑙)(𝑎(join‘𝑙)𝑏))) ∧ ∃𝑎 ∈ (Base‘𝑙)∃𝑏 ∈ (Base‘𝑙)∃𝑐 ∈ (Base‘𝑙)(((0.‘𝑙)(lt‘𝑙)𝑎 ∧ 𝑎(lt‘𝑙)𝑏) ∧ (𝑏(lt‘𝑙)𝑐 ∧ 𝑐(lt‘𝑙)(1.‘𝑙))))} | ||
Theorem | ishlat1 37814* | The predicate "is a Hilbert lattice", which is: is orthomodular (𝐾 ∈ OML), complete (𝐾 ∈ CLat), atomic and satisfies the exchange (or covering) property (𝐾 ∈ CvLat), satisfies the superposition principle, and has a minimum height of 4 (witnessed here by 0, x, y, z, 1). (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 (𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) | ||
Theorem | ishlat2 37815* | The predicate "is a Hilbert lattice". Here we replace 𝐾 ∈ CvLat with the weaker 𝐾 ∈ AtLat and show the exchange property explicitly. (Contributed by NM, 5-Nov-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) | ||
Theorem | ishlat3N 37816* | The predicate "is a Hilbert lattice". Note that the superposition principle is expressed in the compact form ∃𝑧 ∈ 𝐴(𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧). The exchange property and atomicity are provided by 𝐾 ∈ CvLat, and "minimum height 4" is shown explicitly. (Contributed by NM, 8-Nov-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL ↔ ((𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat) ∧ (∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ∃𝑧 ∈ 𝐴 (𝑥 ∨ 𝑧) = (𝑦 ∨ 𝑧) ∧ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))))) | ||
Theorem | ishlatiN 37817* | Properties that determine a Hilbert lattice. (Contributed by NM, 13-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐾 ∈ OML & ⊢ 𝐾 ∈ CLat & ⊢ 𝐾 ∈ AtLat & ⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ ∀𝑥 ∈ 𝐴 ∀𝑦 ∈ 𝐴 ((𝑥 ≠ 𝑦 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑥 ∧ 𝑧 ≠ 𝑦 ∧ 𝑧 ≤ (𝑥 ∨ 𝑦))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑥 ≤ 𝑧 ∧ 𝑥 ≤ (𝑧 ∨ 𝑦)) → 𝑦 ≤ (𝑧 ∨ 𝑥))) & ⊢ ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 )) ⇒ ⊢ 𝐾 ∈ HL | ||
Theorem | hlomcmcv 37818 | A Hilbert lattice is orthomodular, complete, and has the covering (exchange) property. (Contributed by NM, 5-Nov-2012.) |
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ CvLat)) | ||
Theorem | hloml 37819 | A Hilbert lattice is orthomodular. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ OML) | ||
Theorem | hlclat 37820 | A Hilbert lattice is complete. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ CLat) | ||
Theorem | hlcvl 37821 | A Hilbert lattice is an atomic lattice with the covering property. (Contributed by NM, 5-Nov-2012.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ CvLat) | ||
Theorem | hlatl 37822 | A Hilbert lattice is atomic. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ AtLat) | ||
Theorem | hlol 37823 | A Hilbert lattice is an ortholattice. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ OL) | ||
Theorem | hlop 37824 | A Hilbert lattice is an orthoposet. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ OP) | ||
Theorem | hllat 37825 | A Hilbert lattice is a lattice. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ Lat) | ||
Theorem | hllatd 37826 | Deduction form of hllat 37825. A Hilbert lattice is a lattice. (Contributed by BJ, 14-Aug-2022.) |
⊢ (𝜑 → 𝐾 ∈ HL) ⇒ ⊢ (𝜑 → 𝐾 ∈ Lat) | ||
Theorem | hlomcmat 37827 | A Hilbert lattice is orthomodular, complete, and atomic. (Contributed by NM, 5-Nov-2012.) |
⊢ (𝐾 ∈ HL → (𝐾 ∈ OML ∧ 𝐾 ∈ CLat ∧ 𝐾 ∈ AtLat)) | ||
Theorem | hlpos 37828 | A Hilbert lattice is a poset. (Contributed by NM, 20-Oct-2011.) |
⊢ (𝐾 ∈ HL → 𝐾 ∈ Poset) | ||
Theorem | hlatjcl 37829 | Closure of join operation. Frequently-used special case of latjcl 18328 for atoms. (Contributed by NM, 15-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) ∈ 𝐵) | ||
Theorem | hlatjcom 37830 | Commutatitivity of join operation. Frequently-used special case of latjcom 18336 for atoms. (Contributed by NM, 15-Jun-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴 ∧ 𝑌 ∈ 𝐴) → (𝑋 ∨ 𝑌) = (𝑌 ∨ 𝑋)) | ||
Theorem | hlatjidm 37831 | Idempotence of join operation. Frequently-used special case of latjcom 18336 for atoms. (Contributed by NM, 15-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐴) → (𝑋 ∨ 𝑋) = 𝑋) | ||
Theorem | hlatjass 37832 | Lattice join is associative. Frequently-used special case of latjass 18372 for atoms. (Contributed by NM, 27-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = (𝑃 ∨ (𝑄 ∨ 𝑅))) | ||
Theorem | hlatj12 37833 | Swap 1st and 2nd members of lattice join. Frequently-used special case of latj32 18374 for atoms. (Contributed by NM, 4-Jun-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 ∨ (𝑄 ∨ 𝑅)) = (𝑄 ∨ (𝑃 ∨ 𝑅))) | ||
Theorem | hlatj32 37834 | Swap 2nd and 3rd members of lattice join. Frequently-used special case of latj32 18374 for atoms. (Contributed by NM, 21-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑃 ∨ 𝑅) ∨ 𝑄)) | ||
Theorem | hlatjrot 37835 | Rotate lattice join of 3 classes. Frequently-used special case of latjrot 18377 for atoms. (Contributed by NM, 2-Aug-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑅 ∨ 𝑃) ∨ 𝑄)) | ||
Theorem | hlatj4 37836 | Rearrangement of lattice join of 4 classes. Frequently-used special case of latj4 18378 for atoms. (Contributed by NM, 9-Aug-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ∨ (𝑅 ∨ 𝑆)) = ((𝑃 ∨ 𝑅) ∨ (𝑄 ∨ 𝑆))) | ||
Theorem | hlatlej1 37837 | A join's first argument is less than or equal to the join. Special case of latlej1 18337 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑃 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | hlatlej2 37838 | A join's second argument is less than or equal to the join. Special case of latlej2 18338 to show an atom is on a line. (Contributed by NM, 15-May-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → 𝑄 ≤ (𝑃 ∨ 𝑄)) | ||
Theorem | glbconN 37839* | De Morgan's law for GLB and LUB. This holds in any complete ortholattice, although we assume HL for convenience. (Contributed by NM, 17-Jan-2012.) New df-riota 7313. (Revised by SN, 3-Jan-2025.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}))) | ||
Theorem | glbconNOLD 37840* | Obsolete version of glbconN 37839 as of 3-Jan-2025. (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.) (Proof modification is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑆 ⊆ 𝐵) → (𝐺‘𝑆) = ( ⊥ ‘(𝑈‘{𝑥 ∈ 𝐵 ∣ ( ⊥ ‘𝑥) ∈ 𝑆}))) | ||
Theorem | glbconxN 37841* | De Morgan's law for GLB and LUB. Index-set version of glbconN 37839, where we read 𝑆 as 𝑆(𝑖). (Contributed by NM, 17-Jan-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐺 = (glb‘𝐾) & ⊢ ⊥ = (oc‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ ∀𝑖 ∈ 𝐼 𝑆 ∈ 𝐵) → (𝐺‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = 𝑆}) = ( ⊥ ‘(𝑈‘{𝑥 ∣ ∃𝑖 ∈ 𝐼 𝑥 = ( ⊥ ‘𝑆)}))) | ||
Theorem | atnlej1 37842 | If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) → 𝑃 ≠ 𝑄) | ||
Theorem | atnlej2 37843 | If an atom is not less than or equal to the join of two others, it is not equal to either. (This also holds for non-atoms, but in this form it is convenient.) (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) → 𝑃 ≠ 𝑅) | ||
Theorem | hlsuprexch 37844* | A Hilbert lattice has the superposition and exchange properties. (Contributed by NM, 13-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ((𝑃 ≠ 𝑄 → ∃𝑧 ∈ 𝐴 (𝑧 ≠ 𝑃 ∧ 𝑧 ≠ 𝑄 ∧ 𝑧 ≤ (𝑃 ∨ 𝑄))) ∧ ∀𝑧 ∈ 𝐵 ((¬ 𝑃 ≤ 𝑧 ∧ 𝑃 ≤ (𝑧 ∨ 𝑄)) → 𝑄 ≤ (𝑧 ∨ 𝑃)))) | ||
Theorem | hlexch1 37845 | A Hilbert lattice has the exchange property. (Contributed by NM, 13-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃))) | ||
Theorem | hlexch2 37846 | A Hilbert lattice has the exchange property. (Contributed by NM, 6-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) → 𝑄 ≤ (𝑃 ∨ 𝑋))) | ||
Theorem | hlexchb1 37847 | A Hilbert lattice has the exchange property. (Contributed by NM, 16-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄))) | ||
Theorem | hlexchb2 37848 | A Hilbert lattice has the exchange property. (Contributed by NM, 22-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ ¬ 𝑃 ≤ 𝑋) → (𝑃 ≤ (𝑄 ∨ 𝑋) ↔ (𝑃 ∨ 𝑋) = (𝑄 ∨ 𝑋))) | ||
Theorem | hlsupr 37849* | A Hilbert lattice has the superposition property. Theorem 13.2 in [Crawley] p. 107. (Contributed by NM, 30-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑃 ≠ 𝑄) → ∃𝑟 ∈ 𝐴 (𝑟 ≠ 𝑃 ∧ 𝑟 ≠ 𝑄 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄))) | ||
Theorem | hlsupr2 37850* | A Hilbert lattice has the superposition property. (Contributed by NM, 25-Nov-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ∃𝑟 ∈ 𝐴 (𝑃 ∨ 𝑟) = (𝑄 ∨ 𝑟)) | ||
Theorem | hlhgt4 37851* | A Hilbert lattice has a height of at least 4. (Contributed by NM, 4-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ 𝐵 ∃𝑦 ∈ 𝐵 ∃𝑧 ∈ 𝐵 (( 0 < 𝑥 ∧ 𝑥 < 𝑦) ∧ (𝑦 < 𝑧 ∧ 𝑧 < 1 ))) | ||
Theorem | hlhgt2 37852* | A Hilbert lattice has a height of at least 2. (Contributed by NM, 4-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∃𝑥 ∈ 𝐵 ( 0 < 𝑥 ∧ 𝑥 < 1 )) | ||
Theorem | hl0lt1N 37853 | Lattice 0 is less than lattice 1 in a Hilbert lattice. (Contributed by NM, 4-Dec-2011.) (New usage is discouraged.) |
⊢ < = (lt‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 1 = (1.‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → 0 < 1 ) | ||
Theorem | hlexch3 37854 | A Hilbert lattice has the exchange property. (atexch 31323 analog.) (Contributed by NM, 15-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) → 𝑄 ≤ (𝑋 ∨ 𝑃))) | ||
Theorem | hlexch4N 37855 | A Hilbert lattice has the exchange property. Part of Definition 7.8 of [MaedaMaeda] p. 32. (Contributed by NM, 15-Nov-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∧ 𝑋) = 0 ) → (𝑃 ≤ (𝑋 ∨ 𝑄) ↔ (𝑋 ∨ 𝑃) = (𝑋 ∨ 𝑄))) | ||
Theorem | hlatexchb1 37856 | A version of hlexchb1 37847 for atoms. (Contributed by NM, 15-Nov-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) ↔ (𝑅 ∨ 𝑃) = (𝑅 ∨ 𝑄))) | ||
Theorem | hlatexchb2 37857 | A version of hlexchb2 37848 for atoms. (Contributed by NM, 7-Feb-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) ↔ (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑅))) | ||
Theorem | hlatexch1 37858 | Atom exchange property. (Contributed by NM, 7-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑅 ∨ 𝑄) → 𝑄 ≤ (𝑅 ∨ 𝑃))) | ||
Theorem | hlatexch2 37859 | Atom exchange property. (Contributed by NM, 8-Jan-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 ≤ (𝑄 ∨ 𝑅) → 𝑄 ≤ (𝑃 ∨ 𝑅))) | ||
Theorem | hlatmstcOLDN 37860* | 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 31304 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋) | ||
Theorem | hlatle 37861* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 31313 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) | ||
Theorem | hlateq 37862* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 31315 analog.) (Contributed by NM, 24-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | hlrelat1 37863* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 31305, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌))) | ||
Theorem | hlrelat5N 37864* | An atomistic lattice with 0 is relatively atomic, using the definition in Remark 2 of [Kalmbach] p. 149. (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋 < (𝑋 ∨ 𝑝) ∧ 𝑝 ≤ 𝑌)) | ||
Theorem | hlrelat 37865* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 31306 analog.) (Contributed by NM, 4-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋 < (𝑋 ∨ 𝑝) ∧ (𝑋 ∨ 𝑝) ≤ 𝑌)) | ||
Theorem | hlrelat2 37866* | A consequence of relative atomicity. (chrelat2i 31307 analog.) (Contributed by NM, 5-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌))) | ||
Theorem | exatleN 37867 | A condition for an atom to be less than or equal to a lattice element. Part of proof of Lemma A in [Crawley] p. 112. (Contributed by NM, 28-Apr-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≤ 𝑋 ↔ 𝑅 = 𝑃)) | ||
Theorem | hl2at 37868* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 𝑝 ≠ 𝑞) | ||
Theorem | atex 37869 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → 𝐴 ≠ ∅) | ||
Theorem | intnatN 37870 | If the intersection with a non-majorizing element is an atom, the intersecting element is not an atom. (Contributed by NM, 26-Jun-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ (¬ 𝑌 ≤ 𝑋 ∧ (𝑋 ∧ 𝑌) ∈ 𝐴)) → ¬ 𝑌 ∈ 𝐴) | ||
Theorem | 2llnne2N 37871 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑄)) → (𝑅 ∨ 𝑃) ≠ (𝑅 ∨ 𝑄)) | ||
Theorem | 2llnneN 37872 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∨ 𝑃) ≠ (𝑅 ∨ 𝑄)) | ||
Theorem | cvr1 37873 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 31297 analog.) (Contributed by NM, 17-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | cvr2N 37874 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 31298 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 < (𝑋 ∨ 𝑃) ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | hlrelat3 37875* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 37865. (Contributed by NM, 2-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋𝐶(𝑋 ∨ 𝑝) ∧ (𝑋 ∨ 𝑝) ≤ 𝑌)) | ||
Theorem | cvrval3 37876* | Binary relation expressing 𝑌 covers 𝑋. (Contributed by NM, 16-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ (𝑋 ∨ 𝑝) = 𝑌))) | ||
Theorem | cvrval4N 37877* | Binary relation expressing 𝑌 covers 𝑋. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∃𝑝 ∈ 𝐴 (𝑋 ∨ 𝑝) = 𝑌))) | ||
Theorem | cvrval5 37878* | Binary relation expressing 𝑋 covers 𝑋 ∧ 𝑌. (Contributed by NM, 7-Dec-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑋 ↔ ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑌 ∧ (𝑝 ∨ (𝑋 ∧ 𝑌)) = 𝑋))) | ||
Theorem | cvrp 37879 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 31317 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | atcvr1 37880 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄))) | ||
Theorem | atcvr2 37881 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃))) | ||
Theorem | cvrexchlem 37882 | Lemma for cvrexch 37883. (cvexchlem 31310 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → 𝑋𝐶(𝑋 ∨ 𝑌))) | ||
Theorem | cvrexch 37883 | A Hilbert lattice satisfies the exchange axiom. Proposition 1(iii) of [Kalmbach] p. 140 and its converse. Originally proved by Garrett Birkhoff in 1933. (cvexchi 31311 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 ↔ 𝑋𝐶(𝑋 ∨ 𝑌))) | ||
Theorem | cvratlem 37884 | Lemma for cvrat 37885. (atcvatlem 31327 analog.) (Contributed by NM, 22-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴)) | ||
Theorem | cvrat 37885 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 31328 analog.) (Contributed by NM, 22-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋 ∈ 𝐴)) | ||
Theorem | ltltncvr 37886 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → ¬ 𝑋𝐶𝑍)) | ||
Theorem | ltcvrntr 37887 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌𝐶𝑍) → ¬ 𝑋𝐶𝑍)) | ||
Theorem | cvrntr 37888 | The covers relation is not transitive. (cvntr 31234 analog.) (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌𝐶𝑍) → ¬ 𝑋𝐶𝑍)) | ||
Theorem | atcvr0eq 37889 | The covers relation is not transitive. (atcv0eq 31321 analog.) (Contributed by NM, 29-Nov-2011.) |
⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ( 0 𝐶(𝑃 ∨ 𝑄) ↔ 𝑃 = 𝑄)) | ||
Theorem | lnnat 37890 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ ¬ (𝑃 ∨ 𝑄) ∈ 𝐴)) | ||
Theorem | atcvrj0 37891 | Two atoms covering the zero subspace are equal. (atcv1 31322 analog.) (Contributed by NM, 29-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑋𝐶(𝑃 ∨ 𝑄)) → (𝑋 = 0 ↔ 𝑃 = 𝑄)) | ||
Theorem | cvrat2 37892 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 31329 analog.) (Contributed by NM, 30-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑋𝐶(𝑃 ∨ 𝑄))) → 𝑋 ∈ 𝐴) | ||
Theorem | atcvrneN 37893 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃𝐶(𝑄 ∨ 𝑅)) → 𝑄 ≠ 𝑅) | ||
Theorem | atcvrj1 37894 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑅 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑃𝐶(𝑄 ∨ 𝑅)) | ||
Theorem | atcvrj2b 37895 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ((𝑄 ≠ 𝑅 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅)) ↔ 𝑃𝐶(𝑄 ∨ 𝑅))) | ||
Theorem | atcvrj2 37896 | Condition for an atom to be covered by the join of two others. (Contributed by NM, 7-Feb-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑃𝐶(𝑄 ∨ 𝑅)) | ||
Theorem | atleneN 37897 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑅 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑄 ≠ 𝑅) | ||
Theorem | atltcvr 37898 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 < (𝑄 ∨ 𝑅) ↔ 𝑃𝐶(𝑄 ∨ 𝑅))) | ||
Theorem | atle 37899* | Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑝 ∈ 𝐴 𝑝 ≤ 𝑋) | ||
Theorem | atlt 37900 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 < (𝑃 ∨ 𝑄) ↔ 𝑃 ≠ 𝑄)) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |