Home | Metamath
Proof Explorer Theorem List (p. 338 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 | hlatmstcOLDN 33701* | 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 28605 analog.) (Contributed by NM, 21-Oct-2011.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝑈 = (lub‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑈‘{𝑦 ∈ 𝐴 ∣ 𝑦 ≤ 𝑋}) = 𝑋) | ||
Theorem | hlatle 33702* | The ordering of two Hilbert lattice elements is determined by the atoms under them. (chrelat3 28614 analog.) (Contributed by NM, 4-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 ≤ 𝑌 ↔ ∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 → 𝑝 ≤ 𝑌))) | ||
Theorem | hlateq 33703* | The equality of two Hilbert lattice elements is determined by the atoms under them. (chrelat4i 28616 analog.) (Contributed by NM, 24-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (∀𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 ↔ 𝑝 ≤ 𝑌) ↔ 𝑋 = 𝑌)) | ||
Theorem | hlrelat1 33704* | An atomistic lattice with 0 is relatively atomic. Part of Lemma 7.2 of [MaedaMaeda] p. 30. (chpssati 28606, with ∧ swapped, analog.) (Contributed by NM, 4-Dec-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋 < 𝑌 → ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ 𝑝 ≤ 𝑌))) | ||
Theorem | hlrelat5N 33705* | 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 33706* | A Hilbert lattice is relatively atomic. Remark 2 of [Kalmbach] p. 149. (chrelati 28607 analog.) (Contributed by NM, 4-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋 < (𝑋 ∨ 𝑝) ∧ (𝑋 ∨ 𝑝) ≤ 𝑌)) | ||
Theorem | hlrelat2 33707* | A consequence of relative atomicity. (chrelat2i 28608 analog.) (Contributed by NM, 5-Feb-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (¬ 𝑋 ≤ 𝑌 ↔ ∃𝑝 ∈ 𝐴 (𝑝 ≤ 𝑋 ∧ ¬ 𝑝 ≤ 𝑌))) | ||
Theorem | exatleN 33708 | 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 33709* | A Hilbert lattice has at least 2 atoms. (Contributed by NM, 5-Dec-2011.) |
⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 𝑝 ≠ 𝑞) | ||
Theorem | atex 33710 | At least one atom exists. (Contributed by NM, 15-Jul-2012.) |
⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → 𝐴 ≠ ∅) | ||
Theorem | intnatN 33711 | 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 33712 | Condition implying that two intersecting lines are different. (Contributed by NM, 13-Jun-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑄)) → (𝑅 ∨ 𝑃) ≠ (𝑅 ∨ 𝑄)) | ||
Theorem | 2llnneN 33713 | Condition implying that two intersecting lines are different. (Contributed by NM, 29-May-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ∨ 𝑃) ≠ (𝑅 ∨ 𝑄)) | ||
Theorem | cvr1 33714 | A Hilbert lattice has the covering property. Proposition 1(ii) in [Kalmbach] p. 140 (and its converse). (chcv1 28598 analog.) (Contributed by NM, 17-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (¬ 𝑃 ≤ 𝑋 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | cvr2N 33715 | Less-than and covers equivalence in a Hilbert lattice. (chcv2 28599 analog.) (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → (𝑋 < (𝑋 ∨ 𝑃) ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | hlrelat3 33716* | The Hilbert lattice is relatively atomic. Stronger version of hlrelat 33706. (Contributed by NM, 2-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) ∧ 𝑋 < 𝑌) → ∃𝑝 ∈ 𝐴 (𝑋𝐶(𝑋 ∨ 𝑝) ∧ (𝑋 ∨ 𝑝) ≤ 𝑌)) | ||
Theorem | cvrval3 33717* | Binary relation expressing 𝑌 covers 𝑋. (Contributed by NM, 16-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑋 ∧ (𝑋 ∨ 𝑝) = 𝑌))) | ||
Theorem | cvrval4N 33718* | Binary relation expressing 𝑌 covers 𝑋. (Contributed by NM, 16-Jun-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → (𝑋𝐶𝑌 ↔ (𝑋 < 𝑌 ∧ ∃𝑝 ∈ 𝐴 (𝑋 ∨ 𝑝) = 𝑌))) | ||
Theorem | cvrval5 33719* | Binary relation expressing 𝑋 covers 𝑋 ∧ 𝑌. (Contributed by NM, 7-Dec-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑋 ↔ ∃𝑝 ∈ 𝐴 (¬ 𝑝 ≤ 𝑌 ∧ (𝑝 ∨ (𝑋 ∧ 𝑌)) = 𝑋))) | ||
Theorem | cvrp 33720 | A Hilbert lattice satisfies the covering property of Definition 7.4 of [MaedaMaeda] p. 31 and its converse. (cvp 28618 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) → ((𝑋 ∧ 𝑃) = 0 ↔ 𝑋𝐶(𝑋 ∨ 𝑃))) | ||
Theorem | atcvr1 33721 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑃 ∨ 𝑄))) | ||
Theorem | atcvr2 33722 | An atom is covered by its join with a different atom. (Contributed by NM, 7-Feb-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ 𝑃𝐶(𝑄 ∨ 𝑃))) | ||
Theorem | cvrexchlem 33723 | Lemma for cvrexch 33724. (cvexchlem 28611 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 → 𝑋𝐶(𝑋 ∨ 𝑌))) | ||
Theorem | cvrexch 33724 | 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 28612 analog.) (Contributed by NM, 18-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵) → ((𝑋 ∧ 𝑌)𝐶𝑌 ↔ 𝑋𝐶(𝑋 ∨ 𝑌))) | ||
Theorem | cvratlem 33725 | Lemma for cvrat 33726. (atcvatlem 28628 analog.) (Contributed by NM, 22-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) ∧ (𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄))) → (¬ 𝑃(le‘𝐾)𝑋 → 𝑋 ∈ 𝐴)) | ||
Theorem | cvrat 33726 | A nonzero Hilbert lattice element less than the join of two atoms is an atom. (atcvati 28629 analog.) (Contributed by NM, 22-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑋 < (𝑃 ∨ 𝑄)) → 𝑋 ∈ 𝐴)) | ||
Theorem | ltltncvr 33727 | A chained strong ordering is not a covers relation. (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌 < 𝑍) → ¬ 𝑋𝐶𝑍)) | ||
Theorem | ltcvrntr 33728 | Non-transitive condition for the covers relation. (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋 < 𝑌 ∧ 𝑌𝐶𝑍) → ¬ 𝑋𝐶𝑍)) | ||
Theorem | cvrntr 33729 | The covers relation is not transitive. (cvntr 28535 analog.) (Contributed by NM, 18-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ 𝐴 ∧ (𝑋 ∈ 𝐵 ∧ 𝑌 ∈ 𝐵 ∧ 𝑍 ∈ 𝐵)) → ((𝑋𝐶𝑌 ∧ 𝑌𝐶𝑍) → ¬ 𝑋𝐶𝑍)) | ||
Theorem | atcvr0eq 33730 | The covers relation is not transitive. (atcv0eq 28622 analog.) (Contributed by NM, 29-Nov-2011.) |
⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ( 0 𝐶(𝑃 ∨ 𝑄) ↔ 𝑃 = 𝑄)) | ||
Theorem | lnnat 33731 | A line (the join of two distinct atoms) is not an atom. (Contributed by NM, 14-Jun-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 ≠ 𝑄 ↔ ¬ (𝑃 ∨ 𝑄) ∈ 𝐴)) | ||
Theorem | atcvrj0 33732 | Two atoms covering the zero subspace are equal. (atcv1 28623 analog.) (Contributed by NM, 29-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ 𝑋𝐶(𝑃 ∨ 𝑄)) → (𝑋 = 0 ↔ 𝑃 = 𝑄)) | ||
Theorem | cvrat2 33733 | A Hilbert lattice element covered by the join of two distinct atoms is an atom. (atcvat2i 28630 analog.) (Contributed by NM, 30-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ 𝑋𝐶(𝑃 ∨ 𝑄))) → 𝑋 ∈ 𝐴) | ||
Theorem | atcvrneN 33734 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃𝐶(𝑄 ∨ 𝑅)) → 𝑄 ≠ 𝑅) | ||
Theorem | atcvrj1 33735 | 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 33736 | 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 33737 | 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 33738 | Inequality derived from atom condition. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑅 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → 𝑄 ≠ 𝑅) | ||
Theorem | atltcvr 33739 | An equivalence of less-than ordering and covers relation. (Contributed by NM, 7-Feb-2012.) |
⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → (𝑃 < (𝑄 ∨ 𝑅) ↔ 𝑃𝐶(𝑄 ∨ 𝑅))) | ||
Theorem | atle 33740* | Any nonzero element has an atom under it. (Contributed by NM, 28-Jun-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋 ≠ 0 ) → ∃𝑝 ∈ 𝐴 𝑝 ≤ 𝑋) | ||
Theorem | atlt 33741 | Two atoms are unequal iff their join is greater than one of them. (Contributed by NM, 6-May-2012.) |
⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → (𝑃 < (𝑃 ∨ 𝑄) ↔ 𝑃 ≠ 𝑄)) | ||
Theorem | atlelt 33742 | Transfer less-than relation from one atom to another. (Contributed by NM, 7-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ≤ 𝑋 ∧ 𝑄 < 𝑋)) → 𝑃 < 𝑋) | ||
Theorem | 2atlt 33743* | Given an atom less than an element, there is another atom less than the element. (Contributed by NM, 6-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ 𝑃 < 𝑋) → ∃𝑞 ∈ 𝐴 (𝑞 ≠ 𝑃 ∧ 𝑞 < 𝑋)) | ||
Theorem | atexchcvrN 33744 | Atom exchange property. Version of hlatexch2 33700 with covers relation. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃𝐶(𝑄 ∨ 𝑅) → 𝑄𝐶(𝑃 ∨ 𝑅))) | ||
Theorem | atexchltN 33745 | Atom exchange property. Version of hlatexch2 33700 with less-than ordering. (Contributed by NM, 7-Feb-2012.) (New usage is discouraged.) |
⊢ < = (lt‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ 𝑃 ≠ 𝑅) → (𝑃 < (𝑄 ∨ 𝑅) → 𝑄 < (𝑃 ∨ 𝑅))) | ||
Theorem | cvrat3 33746 | A condition implying that a certain lattice element is an atom. Part of Lemma 3.2.20 of [PtakPulmannova] p. 68. (atcvat3i 28639 analog.) (Contributed by NM, 30-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → (𝑋 ∧ (𝑃 ∨ 𝑄)) ∈ 𝐴)) | ||
Theorem | cvrat4 33747* | A condition implying existence of an atom with the properties shown. Lemma 3.2.20 in [PtakPulmannova] p. 68. Also Lemma 9.2(delta) in [MaedaMaeda] p. 41. (atcvat4i 28640 analog.) (Contributed by NM, 30-Nov-2011.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟)))) | ||
Theorem | cvrat42 33748* | Commuted version of cvrat4 33747. (Contributed by NM, 28-Jan-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴)) → ((𝑋 ≠ 0 ∧ 𝑃 ≤ (𝑋 ∨ 𝑄)) → ∃𝑟 ∈ 𝐴 (𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑟 ∨ 𝑄)))) | ||
Theorem | 2atjm 33749 | The meet of a line (expressed with 2 atoms) and a lattice element. (Contributed by NM, 30-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) → ((𝑃 ∨ 𝑄) ∧ 𝑋) = 𝑃) | ||
Theorem | atbtwn 33750 | Property of a 3rd atom 𝑅 on a line 𝑃 ∨ 𝑄 intersecting element 𝑋 at 𝑃. (Contributed by NM, 30-Jul-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋 ∧ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≠ 𝑃 ↔ ¬ 𝑅 ≤ 𝑋)) | ||
Theorem | atbtwnexOLDN 33751* | There exists a 3rd atom 𝑟 on a line 𝑃 ∨ 𝑄 intersecting element 𝑋 at 𝑃, such that 𝑟 is different from 𝑄 and not in 𝑋. (Contributed by NM, 30-Jul-2012.) (New usage is discouraged.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) → ∃𝑟 ∈ 𝐴 (𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑟 ≤ (𝑃 ∨ 𝑄))) | ||
Theorem | atbtwnex 33752* | Given atoms 𝑃 in 𝑋 and 𝑄 not in 𝑋, there exists an atom 𝑟 not in 𝑋 such that the line 𝑄 ∨ 𝑟 intersects 𝑋 at 𝑃. (Contributed by NM, 1-Aug-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑋 ∈ 𝐵 ∧ 𝑃 ≤ 𝑋 ∧ ¬ 𝑄 ≤ 𝑋)) → ∃𝑟 ∈ 𝐴 (𝑟 ≠ 𝑄 ∧ ¬ 𝑟 ≤ 𝑋 ∧ 𝑃 ≤ (𝑄 ∨ 𝑟))) | ||
Theorem | 3noncolr2 33753 | Two ways to express 3 non-colinear atoms (rotated right 2 places). (Contributed by NM, 12-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑄 ≠ 𝑅 ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅))) | ||
Theorem | 3noncolr1N 33754 | Two ways to express 3 non-colinear atoms (rotated right 1 place). (Contributed by NM, 12-Jul-2012.) (New usage is discouraged.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → (𝑅 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑅 ∨ 𝑃))) | ||
Theorem | hlatcon3 33755 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) | ||
Theorem | hlatcon2 33756 | Atom exchange combined with contraposition. (Contributed by NM, 13-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄))) → ¬ 𝑃 ≤ (𝑅 ∨ 𝑄)) | ||
Theorem | 4noncolr3 33757 | A way to express 4 non-colinear atoms (rotated right 3 places). (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) | ||
Theorem | 4noncolr2 33758 | A way to express 4 non-colinear atoms (rotated right 2 places). (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑅 ≠ 𝑆 ∧ ¬ 𝑃 ≤ (𝑅 ∨ 𝑆) ∧ ¬ 𝑄 ≤ ((𝑅 ∨ 𝑆) ∨ 𝑃))) | ||
Theorem | 4noncolr1 33759 | A way to express 4 non-colinear atoms (rotated right 1 places). (Contributed by NM, 11-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) → (𝑆 ≠ 𝑃 ∧ ¬ 𝑄 ≤ (𝑆 ∨ 𝑃) ∧ ¬ 𝑅 ≤ ((𝑆 ∨ 𝑃) ∨ 𝑄))) | ||
Theorem | athgt 33760* | A Hilbert lattice, whose height is at least 4, has a chain of 4 successively covering atom joins. (Contributed by NM, 3-May-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 (𝑝𝐶(𝑝 ∨ 𝑞) ∧ ∃𝑟 ∈ 𝐴 ((𝑝 ∨ 𝑞)𝐶((𝑝 ∨ 𝑞) ∨ 𝑟) ∧ ∃𝑠 ∈ 𝐴 ((𝑝 ∨ 𝑞) ∨ 𝑟)𝐶(((𝑝 ∨ 𝑞) ∨ 𝑟) ∨ 𝑠)))) | ||
Theorem | 3dim0 33761* | There exists a 3-dimensional (height-4) element i.e. a volume. (Contributed by NM, 25-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (𝐾 ∈ HL → ∃𝑝 ∈ 𝐴 ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (𝑝 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑝 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑝 ∨ 𝑞) ∨ 𝑟))) | ||
Theorem | 3dimlem1 33762 | Lemma for 3dim1 33771. (Contributed by NM, 25-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑇 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)) ∧ 𝑃 = 𝑄) → (𝑃 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑅) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑅) ∨ 𝑆))) | ||
Theorem | 3dimlem2 33763 | Lemma for 3dim1 33771. (Contributed by NM, 25-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑇 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)) ∧ (𝑃 ≠ 𝑄 ∧ 𝑃 ≤ (𝑄 ∨ 𝑅))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑆 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑆))) | ||
Theorem | 3dimlem3a 33764 | Lemma for 3dim3 33773. (Contributed by NM, 27-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (¬ 𝑇 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) → ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | ||
Theorem | 3dimlem3 33765 | Lemma for 3dim1 33771. (Contributed by NM, 25-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) | ||
Theorem | 3dimlem3OLDN 33766 | Lemma for 3dim1 33771. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑇 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑇 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) | ||
Theorem | 3dimlem4a 33767 | Lemma for 3dim3 33773. (Contributed by NM, 27-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (¬ 𝑆 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆))) → ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | ||
Theorem | 3dimlem4 33768 | Lemma for 3dim1 33771. (Contributed by NM, 25-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) | ||
Theorem | 3dimlem4OLDN 33769 | Lemma for 3dim1 33771. (Contributed by NM, 25-Jul-2012.) (Proof modification is discouraged.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ ¬ 𝑆 ≤ (𝑄 ∨ 𝑅))) ∧ (𝑃 ≠ 𝑄 ∧ ¬ 𝑃 ≤ (𝑄 ∨ 𝑅)) ∧ ¬ 𝑃 ≤ ((𝑄 ∨ 𝑅) ∨ 𝑆)) → (𝑃 ≠ 𝑄 ∧ ¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑆 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅))) | ||
Theorem | 3dim1lem5 33770* | Lemma for 3dim1 33771. (Contributed by NM, 26-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝑢 ∈ 𝐴 ∧ 𝑣 ∈ 𝐴 ∧ 𝑤 ∈ 𝐴) ∧ (𝑃 ≠ 𝑢 ∧ ¬ 𝑣 ≤ (𝑃 ∨ 𝑢) ∧ ¬ 𝑤 ≤ ((𝑃 ∨ 𝑢) ∨ 𝑣))) → ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑟))) | ||
Theorem | 3dim1 33771* | Construct a 3-dimensional volume (height-4 element) on top of a given atom 𝑃. (Contributed by NM, 25-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (𝑃 ≠ 𝑞 ∧ ¬ 𝑟 ≤ (𝑃 ∨ 𝑞) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑞) ∨ 𝑟))) | ||
Theorem | 3dim2 33772* | Construct 2 new layers on top of 2 given atoms. (Contributed by NM, 27-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) → ∃𝑟 ∈ 𝐴 ∃𝑠 ∈ 𝐴 (¬ 𝑟 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑟))) | ||
Theorem | 3dim3 33773* | Construct a new layer on top of 3 given atoms. (Contributed by NM, 27-Jul-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴)) → ∃𝑠 ∈ 𝐴 ¬ 𝑠 ≤ ((𝑃 ∨ 𝑄) ∨ 𝑅)) | ||
Theorem | 2dim 33774* | Generate a height-3 element (2-dimensional plane) from an atom. (Contributed by NM, 3-May-2012.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → ∃𝑞 ∈ 𝐴 ∃𝑟 ∈ 𝐴 (𝑃𝐶(𝑃 ∨ 𝑞) ∧ (𝑃 ∨ 𝑞)𝐶((𝑃 ∨ 𝑞) ∨ 𝑟))) | ||
Theorem | 1dimN 33775* | An atom is covered by a height-2 element (1-dimensional line). (Contributed by NM, 3-May-2012.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴) → ∃𝑞 ∈ 𝐴 𝑃𝐶(𝑃 ∨ 𝑞)) | ||
Theorem | 1cvrco 33776 | The orthocomplement of an element covered by 1 is an atom. (Contributed by NM, 7-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ ⊥ = (oc‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵) → (𝑋𝐶 1 ↔ ( ⊥ ‘𝑋) ∈ 𝐴)) | ||
Theorem | 1cvratex 33777* | There exists an atom less than an element covered by 1. (Contributed by NM, 7-May-2012.) (Revised by Mario Carneiro, 13-Jun-2014.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑋𝐶 1 ) → ∃𝑝 ∈ 𝐴 𝑝 < 𝑋) | ||
Theorem | 1cvratlt 33778 | An atom less than or equal to an element covered by 1 is less than the element. (Contributed by NM, 7-May-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ < = (lt‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑋𝐶 1 ∧ 𝑃 ≤ 𝑋)) → 𝑃 < 𝑋) | ||
Theorem | 1cvrjat 33779 | An element covered by the lattice unit, when joined with an atom not under it, equals the lattice unit. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑋 ∈ 𝐵 ∧ 𝑃 ∈ 𝐴) ∧ (𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → (𝑋 ∨ 𝑃) = 1 ) | ||
Theorem | 1cvrat 33780 | Create an atom under an element covered by the lattice unit. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 30-Apr-2012.) |
⊢ 𝐵 = (Base‘𝐾) & ⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 1 = (1.‘𝐾) & ⊢ 𝐶 = ( ⋖ ‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑋 ∈ 𝐵) ∧ (𝑃 ≠ 𝑄 ∧ 𝑋𝐶 1 ∧ ¬ 𝑃 ≤ 𝑋)) → ((𝑃 ∨ 𝑄) ∧ 𝑋) ∈ 𝐴) | ||
Theorem | ps-1 33781 | The join of two atoms 𝑅 ∨ 𝑆 (specifying a projective geometry line) is determined uniquely by any two atoms (specifying two points) less than or equal to that join. Part of Lemma 16.4 of [MaedaMaeda] p. 69, showing projective space postulate PS1 in [MaedaMaeda] p. 67. (Contributed by NM, 15-Nov-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴)) → ((𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆) ↔ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆))) | ||
Theorem | ps-2 33782* | Lattice analogue for the projective geometry axiom, "if a line intersects two sides of a triangle at different points then it also intersects the third side." Projective space condition PS2 in [MaedaMaeda] p. 68 and part of Theorem 16.4 in [MaedaMaeda] p. 69. (Contributed by NM, 1-Dec-2011.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ ((¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇) ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → ∃𝑢 ∈ 𝐴 (𝑢 ≤ (𝑃 ∨ 𝑅) ∧ 𝑢 ≤ (𝑆 ∨ 𝑇))) | ||
Theorem | 2atjlej 33783 | Two atoms are different if their join majorizes the join of two different atoms. (Contributed by NM, 4-Jun-2013.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑃 ≠ 𝑄) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ (𝑃 ∨ 𝑄) ≤ (𝑅 ∨ 𝑆))) → 𝑅 ≠ 𝑆) | ||
Theorem | hlatexch3N 33784 | Rearrange join of atoms in an equality. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ ((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑄 ≠ 𝑅 ∧ (𝑃 ∨ 𝑄) = (𝑃 ∨ 𝑅))) → (𝑃 ∨ 𝑄) = (𝑄 ∨ 𝑅)) | ||
Theorem | hlatexch4 33785 | Exchange 2 atoms. (Contributed by NM, 13-May-2013.) |
⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴) ∧ (𝑃 ≠ 𝑅 ∧ 𝑄 ≠ 𝑆 ∧ (𝑃 ∨ 𝑄) = (𝑅 ∨ 𝑆))) → (𝑃 ∨ 𝑅) = (𝑄 ∨ 𝑆)) | ||
Theorem | ps-2b 33786 | Variation of projective geometry axiom ps-2 33782. (Contributed by NM, 3-Jul-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ ∧ = (meet‘𝐾) & ⊢ 0 = (0.‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ 𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴) ∧ (𝑅 ∈ 𝐴 ∧ 𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴) ∧ (¬ 𝑃 ≤ (𝑄 ∨ 𝑅) ∧ 𝑆 ≠ 𝑇 ∧ (𝑆 ≤ (𝑃 ∨ 𝑄) ∧ 𝑇 ≤ (𝑄 ∨ 𝑅)))) → ((𝑃 ∨ 𝑅) ∧ (𝑆 ∨ 𝑇)) ≠ 0 ) | ||
Theorem | 3atlem1 33787 | Lemma for 3at 33794. (Contributed by NM, 22-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ ¬ 𝑃 ≤ (𝑇 ∨ 𝑈) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | ||
Theorem | 3atlem2 33788 | Lemma for 3at 33794. (Contributed by NM, 22-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ (𝑃 ≠ 𝑈 ∧ 𝑃 ≤ (𝑇 ∨ 𝑈)) ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | ||
Theorem | 3atlem3 33789 | Lemma for 3at 33794. (Contributed by NM, 23-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑈 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | ||
Theorem | 3atlem4 33790 | Lemma for 3at 33794. (Contributed by NM, 23-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑅)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑅)) | ||
Theorem | 3atlem5 33791 | Lemma for 3at 33794. (Contributed by NM, 23-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄 ∧ ¬ 𝑄 ≤ (𝑃 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | ||
Theorem | 3atlem6 33792 | Lemma for 3at 33794. (Contributed by NM, 23-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄 ∧ 𝑄 ≤ (𝑃 ∨ 𝑈)) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | ||
Theorem | 3atlem7 33793 | Lemma for 3at 33794. (Contributed by NM, 23-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄) ∧ ((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈)) → ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈)) | ||
Theorem | 3at 33794 | Any three non-colinear atoms in a (lattice) plane determine the plane uniquely. This is the 2-dimensional analogue of ps-1 33781 for lines and 4at 33917 for volumes. I could not find this proof in the literature on projective geometry (where it is either given as an axiom or stated as an unproved fact), but it is similar to Theorem 15 of Veblen, "The Foundations of Geometry" (1911), p. 18, which uses different axioms. This proof was written before I became aware of Veblen's, and it is possible that a shorter proof could be obtained by using Veblen's proof for hints. (Contributed by NM, 23-Jun-2012.) |
⊢ ≤ = (le‘𝐾) & ⊢ ∨ = (join‘𝐾) & ⊢ 𝐴 = (Atoms‘𝐾) ⇒ ⊢ (((𝐾 ∈ HL ∧ (𝑃 ∈ 𝐴 ∧ 𝑄 ∈ 𝐴 ∧ 𝑅 ∈ 𝐴) ∧ (𝑆 ∈ 𝐴 ∧ 𝑇 ∈ 𝐴 ∧ 𝑈 ∈ 𝐴)) ∧ (¬ 𝑅 ≤ (𝑃 ∨ 𝑄) ∧ 𝑃 ≠ 𝑄)) → (((𝑃 ∨ 𝑄) ∨ 𝑅) ≤ ((𝑆 ∨ 𝑇) ∨ 𝑈) ↔ ((𝑃 ∨ 𝑄) ∨ 𝑅) = ((𝑆 ∨ 𝑇) ∨ 𝑈))) | ||
Syntax | clln 33795 | Extend class notation with set of all "lattice lines" (lattice elements which cover an atom) in a Hilbert lattice. |
class LLines | ||
Syntax | clpl 33796 | Extend class notation with set of all "lattice planes" (lattice elements which cover a line) in a Hilbert lattice. |
class LPlanes | ||
Syntax | clvol 33797 | Extend class notation with set of all 3-dimensional "lattice volumes" (lattice elements which cover a plane) in a Hilbert lattice. |
class LVols | ||
Syntax | clines 33798 | Extend class notation with set of all projective lines for a Hilbert lattice. |
class Lines | ||
Syntax | cpointsN 33799 | Extend class notation with set of all projective points. |
class Points | ||
Syntax | cpsubsp 33800 | Extend class notation with set of all projective subspaces. |
class PSubSp |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |