![]() |
Metamath
Proof Explorer Theorem List (p. 396 of 484) | < 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-30767) |
![]() (30768-32290) |
![]() (32291-48346) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | pexmidlem7N 39501 | Lemma for pexmidN 39494. Contradict pexmidlem6N 39500. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) & β’ π = (π + {π}) β β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (( β₯ β( β₯ βπ)) = π β§ π β β β§ Β¬ π β (π + ( β₯ βπ)))) β π β π) | ||
Theorem | pexmidlem8N 39502 | Lemma for pexmidN 39494. The contradiction of pexmidlem6N 39500 and pexmidlem7N 39501 shows that there can be no atom π that is not in π + ( β₯ βπ), which is therefore the whole atom space. (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ (((πΎ β HL β§ π β π΄) β§ (( β₯ β( β₯ βπ)) = π β§ π β β )) β (π + ( β₯ βπ)) = π΄) | ||
Theorem | pexmidALTN 39503 | Excluded middle law for closed projective subspaces, which is equivalent to (and derived from) the orthomodular law poml4N 39478. Lemma 3.3(2) in [Holland95] p. 215. In our proof, we use the variables π, π, π, π, π in place of Hollands' l, m, P, Q, L respectively. TODO: should we make this obsolete? (Contributed by NM, 3-Feb-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ + = (+πβπΎ) & β’ β₯ = (β₯πβπΎ) β β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯ βπ)) = π) β (π + ( β₯ βπ)) = π΄) | ||
Theorem | pl42lem1N 39504 | Lemma for pl42N 39508. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ)) β (πΉβ((((π β¨ π) β§ π) β¨ π) β§ π)) = (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ)))) | ||
Theorem | pl42lem2N 39505 | Lemma for pl42N 39508. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((πΉβπ) + (πΉβπ)) + (((πΉβπ) + (πΉβπ)) β© ((πΉβπ) + (πΉβπ)))) β (πΉβ((π β¨ π) β¨ ((π β¨ π) β§ (π β¨ π))))) | ||
Theorem | pl42lem3N 39506 | Lemma for pl42N 39508. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β (((((πΉβπ) + (πΉβπ)) β© (πΉβπ)) + (πΉβπ)) β© (πΉβπ)) β ((((πΉβπ) + (πΉβπ)) + (πΉβπ)) β© (((πΉβπ) + (πΉβπ)) + (πΉβπ)))) | ||
Theorem | pl42lem4N 39507 | Lemma for pl42N 39508. (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ πΉ = (pmapβπΎ) & β’ + = (+πβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ)) β (πΉβ((((π β¨ π) β§ π) β¨ π) β§ π)) β (πΉβ((π β¨ π) β¨ ((π β¨ π) β§ (π β¨ π)))))) | ||
Theorem | pl42N 39508 | Law holding in a Hilbert lattice that fails in orthomodular lattice L42 (Figure 7 in [MegPav2000] p. 2366). (Contributed by NM, 8-Apr-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ ( β₯ βπ) β§ π β€ ( β₯ βπ)) β ((((π β¨ π) β§ π) β¨ π) β§ π) β€ ((π β¨ π) β¨ ((π β¨ π) β§ (π β¨ π))))) | ||
Syntax | clh 39509 | Extend class notation with set of all co-atoms (lattice hyperplanes). |
class LHyp | ||
Syntax | claut 39510 | Extend class notation with set of all lattice automorphisms. |
class LAut | ||
Syntax | cwpointsN 39511 | Extend class notation with W points. |
class WAtoms | ||
Syntax | cpautN 39512 | Extend class notation with set of all projective automorphisms. |
class PAut | ||
Definition | df-lhyp 39513* | Define the set of lattice hyperplanes, which are all lattice elements covered by 1 (i.e., all co-atoms). We call them "hyperplanes" instead of "co-atoms" in analogy with projective geometry hyperplanes. (Contributed by NM, 11-May-2012.) |
β’ LHyp = (π β V β¦ {π₯ β (Baseβπ) β£ π₯( β βπ)(1.βπ)}) | ||
Definition | df-laut 39514* | Define set of lattice autoisomorphisms. (Contributed by NM, 11-May-2012.) |
β’ LAut = (π β V β¦ {π β£ (π:(Baseβπ)β1-1-ontoβ(Baseβπ) β§ βπ₯ β (Baseβπ)βπ¦ β (Baseβπ)(π₯(leβπ)π¦ β (πβπ₯)(leβπ)(πβπ¦)))}) | ||
Definition | df-watsN 39515* | Define W-atoms corresponding to an arbitrary "fiducial (i.e. reference) atom" π. These are all atoms not in the polarity of {π}), which is the hyperplane determined by π. Definition of set W in [Crawley] p. 111. (Contributed by NM, 26-Jan-2012.) |
β’ WAtoms = (π β V β¦ (π β (Atomsβπ) β¦ ((Atomsβπ) β ((β₯πβπ)β{π})))) | ||
Definition | df-pautN 39516* | Define set of all projective automorphisms. This is the intended definition of automorphism in [Crawley] p. 112. (Contributed by NM, 26-Jan-2012.) |
β’ PAut = (π β V β¦ {π β£ (π:(PSubSpβπ)β1-1-ontoβ(PSubSpβπ) β§ βπ₯ β (PSubSpβπ)βπ¦ β (PSubSpβπ)(π₯ β π¦ β (πβπ₯) β (πβπ¦)))}) | ||
Theorem | watfvalN 39517* | The W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) β β’ (πΎ β π΅ β π = (π β π΄ β¦ (π΄ β ((β₯πβπΎ)β{π})))) | ||
Theorem | watvalN 39518 | Value of the W atoms function. (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (πβπ·) = (π΄ β ((β₯πβπΎ)β{π·}))) | ||
Theorem | iswatN 39519 | The predicate "is a W atom" (corresponding to fiducial atom π·). (Contributed by NM, 26-Jan-2012.) (New usage is discouraged.) |
β’ π΄ = (AtomsβπΎ) & β’ π = (β₯πβπΎ) & β’ π = (WAtomsβπΎ) β β’ ((πΎ β π΅ β§ π· β π΄) β (π β (πβπ·) β (π β π΄ β§ Β¬ π β ((β₯πβπΎ)β{π·})))) | ||
Theorem | lhpset 39520* | The set of co-atoms (lattice hyperplanes). (Contributed by NM, 11-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π΄ β π» = {π€ β π΅ β£ π€πΆ 1 }) | ||
Theorem | islhp 39521 | The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 11-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π΄ β (π β π» β (π β π΅ β§ ππΆ 1 ))) | ||
Theorem | islhp2 39522 | The predicate "is a co-atom (lattice hyperplane)". (Contributed by NM, 18-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β π΄ β§ π β π΅) β (π β π» β ππΆ 1 )) | ||
Theorem | lhpbase 39523 | A co-atom is a member of the lattice base set (i.e., a lattice element). (Contributed by NM, 18-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) β β’ (π β π» β π β π΅) | ||
Theorem | lhp1cvr 39524 | The lattice unity covers a co-atom (lattice hyperplane). (Contributed by NM, 18-May-2012.) |
β’ 1 = (1.βπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β π΄ β§ π β π») β ππΆ 1 ) | ||
Theorem | lhplt 39525 | An atom under a co-atom is strictly less than it. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β π < π) | ||
Theorem | lhp2lt 39526 | The join of two atoms under a co-atom is strictly less than it. (Contributed by NM, 8-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β (π β¨ π) < π) | ||
Theorem | lhpexlt 39527* | There exists an atom less than a co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
β’ < = (ltβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ π < π) | ||
Theorem | lhp0lt 39528 | A co-atom is greater than zero. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) |
β’ < = (ltβπΎ) & β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β 0 < π) | ||
Theorem | lhpn0 39529 | A co-atom is nonzero. TODO: is this needed? (Contributed by NM, 26-Apr-2013.) |
β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β π β 0 ) | ||
Theorem | lhpexle 39530* | There exists an atom under a co-atom. (Contributed by NM, 26-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ π β€ π) | ||
Theorem | lhpexnle 39531* | There exists an atom not under a co-atom. (Contributed by NM, 12-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ Β¬ π β€ π) | ||
Theorem | lhpexle1lem 39532* | Lemma for lhpexle1 39533 and others that eliminates restrictions on π. (Contributed by NM, 24-Jul-2013.) |
β’ (π β βπ β π΄ (π β€ π β§ π)) & β’ ((π β§ (π β π΄ β§ π β€ π)) β βπ β π΄ (π β€ π β§ π β§ π β π)) β β’ (π β βπ β π΄ (π β€ π β§ π β§ π β π)) | ||
Theorem | lhpexle1 39533* | There exists an atom under a co-atom different from any given element. (Contributed by NM, 24-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ π β π)) | ||
Theorem | lhpexle2lem 39534* | Lemma for lhpexle2 39535. (Contributed by NM, 19-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β βπ β π΄ (π β€ π β§ π β π β§ π β π)) | ||
Theorem | lhpexle2 39535* | There exists atom under a co-atom different from any two other elements. (Contributed by NM, 24-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ π β π β§ π β π)) | ||
Theorem | lhpexle3lem 39536* | There exists atom under a co-atom different from any three other atoms. TODO: study if adant*, simp* usage can be improved. (Contributed by NM, 9-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β π΄ β§ π β π΄) β§ (π β€ π β§ π β€ π β§ π β€ π)) β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) | ||
Theorem | lhpexle3 39537* | There exists atom under a co-atom different from any three other elements. (Contributed by NM, 24-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ (π β€ π β§ (π β π β§ π β π β§ π β π))) | ||
Theorem | lhpex2leN 39538* | There exist at least two different atoms under a co-atom. This allows to create a line under the co-atom. TODO: is this needed? (Contributed by NM, 1-Jun-2012.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β βπ β π΄ βπ β π΄ (π β€ π β§ π β€ π β§ π β π)) | ||
Theorem | lhpoc 39539 | The orthocomplement of a co-atom (lattice hyperplane) is an atom. (Contributed by NM, 18-May-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π» β ( β₯ βπ) β π΄)) | ||
Theorem | lhpoc2N 39540 | The orthocomplement of an atom is a co-atom (lattice hyperplane). (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π΅) β (π β π΄ β ( β₯ βπ) β π»)) | ||
Theorem | lhpocnle 39541 | The orthocomplement of a co-atom is not under it. (Contributed by NM, 22-May-2012.) |
β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β Β¬ ( β₯ βπ) β€ π) | ||
Theorem | lhpocat 39542 | The orthocomplement of a co-atom is an atom. (Contributed by NM, 9-Feb-2013.) |
β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β ( β₯ βπ) β π΄) | ||
Theorem | lhpocnel 39543 | The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 25-May-2012.) |
β’ β€ = (leβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((πΎ β HL β§ π β π») β (( β₯ βπ) β π΄ β§ Β¬ ( β₯ βπ) β€ π)) | ||
Theorem | lhpocnel2 39544 | The orthocomplement of a co-atom is an atom not under it. Provides a convenient construction when we need the existence of any object with this property. (Contributed by NM, 20-Feb-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (π β π΄ β§ Β¬ π β€ π)) | ||
Theorem | lhpjat1 39545 | The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 18-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) | ||
Theorem | lhpjat2 39546 | The join of a co-atom (hyperplane) and an atom not under it is the lattice unity. (Contributed by NM, 4-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 1 = (1.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) | ||
Theorem | lhpj1 39547 | The join of a co-atom (hyperplane) and an element not under it is the lattice unity. (Contributed by NM, 7-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 1 = (1.βπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β (π β¨ π) = 1 ) | ||
Theorem | lhpmcvr 39548 | The meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 7-Dec-2012.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β (π β§ π)πΆπ) | ||
Theorem | lhpmcvr2 39549* | Alternate way to express that the meet of a lattice hyperplane with an element not under it is covered by the element. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β βπ β π΄ (Β¬ π β€ π β§ (π β¨ (π β§ π)) = π)) | ||
Theorem | lhpmcvr3 39550 | Specialization of lhpmcvr2 39549. TODO: Use this to simplify many uses of (π β¨ (π β§ π)) = π to become π β€ π. (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β€ π β (π β¨ (π β§ π)) = π)) | ||
Theorem | lhpmcvr4N 39551 | Specialization of lhpmcvr2 39549. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΅ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β§ π) β€ π β§ π β€ π)) β Β¬ π β€ π) | ||
Theorem | lhpmcvr5N 39552* | Specialization of lhpmcvr2 39549. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ (π β§ π) β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ (π β¨ (π β§ π)) = π)) | ||
Theorem | lhpmcvr6N 39553* | Specialization of lhpmcvr2 39549. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ (π β§ π) β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ π β€ π)) | ||
Theorem | lhpm0atN 39554 | If the meet of a lattice hyperplane with a nonzero element is zero, the element is an atom. (Contributed by NM, 28-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β 0 β§ (π β§ π) = 0 )) β π β π΄) | ||
Theorem | lhpmat 39555 | An element covered by the lattice unity, when conjoined with an atom not under it, equals the lattice zero. (Contributed by NM, 6-Jun-2012.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (π β§ π) = 0 ) | ||
Theorem | lhpmatb 39556 | An element covered by the lattice unity, when conjoined with an atom, equals zero iff the atom is not under it. (Contributed by NM, 15-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄) β (Β¬ π β€ π β (π β§ π) = 0 )) | ||
Theorem | lhp2at0 39557 | Join and meet with different atoms under co-atom π. (Contributed by NM, 15-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β¨ π) β§ π) = 0 ) | ||
Theorem | lhp2atnle 39558 | Inequality for 2 different atoms under co-atom π. (Contributed by NM, 17-Jun-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β Β¬ π β€ (π β¨ π)) | ||
Theorem | lhp2atne 39559 | Inequality for joins with 2 different atoms under co-atom π. (Contributed by NM, 22-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β π΄ β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ π β π) β (π β¨ π) β (π β¨ π)) | ||
Theorem | lhp2at0nle 39560 | Inequality for 2 different atoms (or an atom and zero) under co-atom π. (Contributed by NM, 28-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π) β§ ((π β π΄ β¨ π = 0 ) β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β Β¬ π β€ (π β¨ π)) | ||
Theorem | lhp2at0ne 39561 | Inequality for joins with 2 different atoms (or an atom and zero) under co-atom π. (Contributed by NM, 28-Jul-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ 0 = (0.βπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (((π β π΄ β¨ π = 0 ) β§ π β€ π) β§ (π β π΄ β§ π β€ π)) β§ π β π) β (π β¨ π) β (π β¨ π)) | ||
Theorem | lhpelim 39562 | Eliminate an atom not under a lattice hyperplane. TODO: Look at proofs using lhpmat 39555 to see if this can be used to shorten them. (Contributed by NM, 27-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΅) β ((π β¨ (π β§ π)) β§ π) = (π β§ π)) | ||
Theorem | lhpmod2i2 39563 | Modular law for hyperplanes analogous to atmod2i2 39387 for atoms. (Contributed by NM, 9-Feb-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β ((π β§ π) β¨ π) = (π β§ (π β¨ π))) | ||
Theorem | lhpmod6i1 39564 | Modular law for hyperplanes analogous to complement of atmod2i1 39386 for atoms. (Contributed by NM, 1-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β€ π) β (π β¨ (π β§ π)) = ((π β¨ π) β§ π)) | ||
Theorem | lhprelat3N 39565* | The Hilbert lattice is relatively atomic with respect to co-atoms (lattice hyperplanes). Dual version of hlrelat3 38937. (Contributed by NM, 20-Jun-2012.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ < = (ltβπΎ) & β’ β§ = (meetβπΎ) & β’ πΆ = ( β βπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ π < π) β βπ€ β π» (π β€ (π β§ π€) β§ (π β§ π€)πΆπ)) | ||
Theorem | cdlemb2 39566* | Given two atoms not under the fiducial (reference) co-atom π, there is a third. Lemma B in [Crawley] p. 112. (Contributed by NM, 30-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) | ||
Theorem | lhple 39567 | Property of a lattice element under a co-atom. (Contributed by NM, 28-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((π β¨ π) β§ π) = π) | ||
Theorem | lhpat 39568 | Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 23-May-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β ((π β¨ π) β§ π) β π΄) | ||
Theorem | lhpat4N 39569 | Property of an atom under a co-atom. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β ((π β¨ π) β§ π) = π) | ||
Theorem | lhpat2 39570 | Create an atom under a co-atom. Part of proof of Lemma B in [Crawley] p. 112. (Contributed by NM, 21-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) | ||
Theorem | lhpat3 39571 | There is only one atom under both π β¨ π and co-atom π. (Contributed by NM, 21-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ π β π΄) β§ (π β π β§ π β€ (π β¨ π))) β (Β¬ π β€ π β π β π )) | ||
Theorem | 4atexlemk 39572 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β πΎ β HL) | ||
Theorem | 4atexlemw 39573 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β π β π») | ||
Theorem | 4atexlempw 39574 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β (π β π΄ β§ Β¬ π β€ π)) | ||
Theorem | 4atexlemp 39575 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β π β π΄) | ||
Theorem | 4atexlemq 39576 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β π β π΄) | ||
Theorem | 4atexlems 39577 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β π β π΄) | ||
Theorem | 4atexlemt 39578 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β π β π΄) | ||
Theorem | 4atexlemutvt 39579 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β (π β¨ π) = (π β¨ π)) | ||
Theorem | 4atexlempnq 39580 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β π β π) | ||
Theorem | 4atexlemnslpq 39581 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β Β¬ π β€ (π β¨ π)) | ||
Theorem | 4atexlemkl 39582 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β πΎ β Lat) | ||
Theorem | 4atexlemkc 39583 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) β β’ (π β πΎ β CvLat) | ||
Theorem | 4atexlemwb 39584 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ π» = (LHypβπΎ) β β’ (π β π β (BaseβπΎ)) | ||
Theorem | 4atexlempsb 39585 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (π β (π β¨ π) β (BaseβπΎ)) | ||
Theorem | 4atexlemqtb 39586 | Lemma for 4atexlem7 39600. (Contributed by NM, 24-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (π β (π β¨ π) β (BaseβπΎ)) | ||
Theorem | 4atexlempns 39587 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (π β π β π) | ||
Theorem | 4atexlemswapqr 39588 | Lemma for 4atexlem7 39600. Swap π and π , so that theorems involving πΆ can be reused for π·. Note that π must be expanded because it involves π. (Contributed by NM, 25-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)) β§ (π β π΄ β§ (((π β¨ π ) β§ π) β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π )))) | ||
Theorem | 4atexlemu 39589 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (π β π β π΄) | ||
Theorem | 4atexlemv 39590 | Lemma for 4atexlem7 39600. (Contributed by NM, 23-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (π β π β π΄) | ||
Theorem | 4atexlemunv 39591 | Lemma for 4atexlem7 39600. (Contributed by NM, 21-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (π β π β π) | ||
Theorem | 4atexlemtlw 39592 | Lemma for 4atexlem7 39600. (Contributed by NM, 24-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (π β π β€ π) | ||
Theorem | 4atexlemntlpq 39593 | Lemma for 4atexlem7 39600. (Contributed by NM, 24-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) β β’ (π β Β¬ π β€ (π β¨ π)) | ||
Theorem | 4atexlemc 39594 | Lemma for 4atexlem7 39600. (Contributed by NM, 24-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ π)) β β’ (π β πΆ β π΄) | ||
Theorem | 4atexlemnclw 39595 | Lemma for 4atexlem7 39600. (Contributed by NM, 24-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ π)) β β’ (π β Β¬ πΆ β€ π) | ||
Theorem | 4atexlemex2 39596* | Lemma for 4atexlem7 39600. Show that when πΆ β π, πΆ satisfies the existence condition of the consequent. (Contributed by NM, 25-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ π)) β β’ ((π β§ πΆ β π) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) | ||
Theorem | 4atexlemcnd 39597 | Lemma for 4atexlem7 39600. (Contributed by NM, 24-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ π)) & β’ π· = ((π β¨ π) β§ (π β¨ π)) β β’ (π β πΆ β π·) | ||
Theorem | 4atexlemex4 39598* | Lemma for 4atexlem7 39600. Show that when πΆ = π, π· satisfies the existence condition of the consequent. (Contributed by NM, 26-Nov-2012.) |
β’ (π β (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ (π β π΄ β§ Β¬ π β€ π β§ (π β¨ π ) = (π β¨ π )) β§ (π β π΄ β§ (π β¨ π) = (π β¨ π))) β§ (π β π β§ Β¬ π β€ (π β¨ π)))) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π β¨ π) β§ π) & β’ πΆ = ((π β¨ π) β§ (π β¨ π)) & β’ π· = ((π β¨ π) β§ (π β¨ π)) β β’ ((π β§ πΆ = π) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) | ||
Theorem | 4atexlemex6 39599* | Lemma for 4atexlem7 39600. (Contributed by NM, 25-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π β¨ π ) = (π β¨ π ) β§ π β π β§ Β¬ π β€ (π β¨ π))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) | ||
Theorem | 4atexlem7 39600* | Whenever there are at least 4 atoms under π β¨ π (specifically, π, π, π, and (π β¨ π) β§ π), there are also at least 4 atoms under π β¨ π. This proves the statement in Lemma E of [Crawley] p. 114, last line, "...p β¨ q/0 and hence p β¨ s/0 contains at least four atoms..." Note that by cvlsupr2 38867, our (π β¨ π) = (π β¨ π) is a shorter way to express π β π β§ π β π β§ π β€ (π β¨ π). With a longer proof, the condition Β¬ π β€ (π β¨ π) could be eliminated (see 4atex 39601), although for some purposes this more restricted lemma may be adequate. (Contributed by NM, 25-Nov-2012.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ (π β π β§ Β¬ π β€ (π β¨ π) β§ βπ β π΄ (Β¬ π β€ π β§ (π β¨ π) = (π β¨ π)))) β βπ§ β π΄ (Β¬ π§ β€ π β§ (π β¨ π§) = (π β¨ π§))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |