![]() |
Metamath
Proof Explorer Theorem List (p. 405 of 480) | < 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-30439) |
![]() (30440-31962) |
![]() (31963-47940) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dihord2pre2 40401* | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. (Contributed by NM, 4-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoBβπΎ)βπ) & β’ π½ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((ocβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ + = (+gβπ) & β’ πΊ = (β©β β π (ββπ) = π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ) β (πΌβ(π β§ π))))) β (π β¨ (π β§ π)) β€ (π β¨ (π β§ π))) | ||
Theorem | dihord2 40402 | Part of proof after Lemma N of [Crawley] p. 122. Reverse ordering property. TODO: do we need Β¬ π β€ π and Β¬ π β€ π? (Contributed by NM, 4-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoBβπΎ)βπ) & β’ π½ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅) β§ ((π β¨ (π β§ π)) = π β§ (π β¨ (π β§ π)) = π β§ ((π½βπ) β (πΌβ(π β§ π))) β ((π½βπ) β (πΌβ(π β§ π))))) β π β€ π) | ||
Syntax | cdih 40403 | Extend class notation with isomorphism H. |
class DIsoH | ||
Definition | df-dih 40404* | Define isomorphism H. (Contributed by NM, 28-Jan-2014.) |
β’ DIsoH = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β (Baseβπ) β¦ if(π₯(leβπ)π€, (((DIsoBβπ)βπ€)βπ₯), (β©π’ β (LSubSpβ((DVecHβπ)βπ€))βπ β (Atomsβπ)((Β¬ π(leβπ)π€ β§ (π(joinβπ)(π₯(meetβπ)π€)) = π₯) β π’ = ((((DIsoCβπ)βπ€)βπ)(LSSumβ((DVecHβπ)βπ€))(((DIsoBβπ)βπ€)β(π₯(meetβπ)π€))))))))) | ||
Theorem | dihffval 40405* | The isomorphism H for a lattice πΎ. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoHβπΎ) = (π€ β π» β¦ (π₯ β π΅ β¦ if(π₯ β€ π€, (((DIsoBβπΎ)βπ€)βπ₯), (β©π’ β (LSubSpβ((DVecHβπΎ)βπ€))βπ β π΄ ((Β¬ π β€ π€ β§ (π β¨ (π₯ β§ π€)) = π₯) β π’ = ((((DIsoCβπΎ)βπ€)βπ)(LSSumβ((DVecHβπΎ)βπ€))(((DIsoBβπΎ)βπ€)β(π₯ β§ π€))))))))) | ||
Theorem | dihfval 40406* | Isomorphism H for a lattice πΎ. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 28-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β π΅ β¦ if(π₯ β€ π, (π·βπ₯), (β©π’ β π βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π’ = ((πΆβπ) β (π·β(π₯ β§ π)))))))) | ||
Theorem | dihval 40407* | Value of isomorphism H for a lattice πΎ. Definition of isomorphism map in [Crawley] p. 122 line 3. (Contributed by NM, 3-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β π β§ π β π») β§ π β π΅) β (πΌβπ) = if(π β€ π, (π·βπ), (β©π’ β π βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π’ = ((πΆβπ) β (π·β(π β§ π))))))) | ||
Theorem | dihvalc 40408* | Value of isomorphism H for a lattice πΎ when Β¬ π β€ π. (Contributed by NM, 4-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β (πΌβπ) = (β©π’ β π βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π β§ π)) = π) β π’ = ((πΆβπ) β (π·β(π β§ π)))))) | ||
Theorem | dihlsscpre 40409 | Closure of isomorphism H for a lattice πΎ when Β¬ π β€ π. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β (πΌβπ) β π) | ||
Theorem | dihvalcqpre 40410 | Value of isomorphism H for a lattice πΎ when Β¬ π β€ π, given auxiliary atom π. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΌβπ) = ((πΆβπ) β (π·β(π β§ π)))) | ||
Theorem | dihvalcq 40411 | Value of isomorphism H for a lattice πΎ when Β¬ π β€ π, given auxiliary atom π. TODO: Use dihvalcq2 40422 (with lhpmcvr3 39200 for (π β¨ (π β§ π)) = π simplification) that changes πΆ and π· to πΌ and make this obsolete. Do to other theorems as well. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΌβπ) = ((πΆβπ) β (π·β(π β§ π)))) | ||
Theorem | dihvalb 40412 | Value of isomorphism H for a lattice πΎ when π β€ π. (Contributed by NM, 4-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = (π·βπ)) | ||
Theorem | dihopelvalbN 40413* | Ordered pair member of the partial isomorphism H for argument under π. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (β¨πΉ, πβ© β (πΌβπ) β ((πΉ β π β§ (π βπΉ) β€ π) β§ π = π))) | ||
Theorem | dihvalcqat 40414 | Value of isomorphism H for a lattice πΎ at an atom not under π. (Contributed by NM, 27-Mar-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π½ = ((DIsoCβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (πΌβπ) = (π½βπ)) | ||
Theorem | dih1dimb 40415* | Two expressions for a 1-dimensional subspace of vector space H (when πΉ is a nonzero vector i.e. non-identity translation). (Contributed by NM, 27-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSpanβπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΌβ(π βπΉ)) = (πβ{β¨πΉ, πβ©})) | ||
Theorem | dih1dimb2 40416* | Isomorphism H at an atom under π. (Contributed by NM, 27-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSpanβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π (π β ( I βΎ π΅) β§ (πΌβπ) = (πβ{β¨π, πβ©}))) | ||
Theorem | dih1dimc 40417* | Isomorphism H at an atom not under π. (Contributed by NM, 27-Apr-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSpanβπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (πΌβπ) = (πβ{β¨πΉ, ( I βΎ π)β©})) | ||
Theorem | dib2dim 40418 | Extend dia2dim 40252 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoBβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dih2dimb 40419 | Extend dib2dim 40418 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dih2dimbALTN 40420 | Extend dia2dim 40252 to isomorphism H. (This version combines dib2dim 40418 and dih2dimb 40419 for shorter overall proof, but may be less easy to understand. TODO: decide which to use.) (Contributed by NM, 22-Sep-2014.) (Proof modification is discouraged.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dihopelvalcqat 40421* | Ordered pair member of the partial isomorphism H for atom argument not under π. TODO: remove .t hypothesis. (Contributed by NM, 30-Mar-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ πΊ = (β©π β π (πβπ) = π) & β’ πΉ β V & β’ π β V β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β (β¨πΉ, πβ© β (πΌβπ) β (πΉ = (πβπΊ) β§ π β πΈ))) | ||
Theorem | dihvalcq2 40422 | Value of isomorphism H for a lattice πΎ when Β¬ π β€ π, given auxiliary atom π. (Contributed by NM, 26-Sep-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (πΌβπ) = ((πΌβπ) β (πΌβ(π β§ π)))) | ||
Theorem | dihopelvalcpre 40423* | Member of value of isomorphism H for a lattice πΎ when Β¬ π β€ π, given auxiliary atom π. TODO: refactor to be shorter and more understandable; add lemmas? (Contributed by NM, 13-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ πΊ = (β©π β π (πβπ) = π) & β’ πΉ β V & β’ π β V & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DIsoBβπΎ)βπ) & β’ πΆ = ((DIsoCβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (π β πΈ, π β πΈ β¦ (β β π β¦ ((πββ) β (πββ)))) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (β¨πΉ, πβ© β (πΌβπ) β ((πΉ β π β§ π β πΈ) β§ (π β(πΉ β β‘(πβπΊ))) β€ π))) | ||
Theorem | dihopelvalc 40424* | Member of value of isomorphism H for a lattice πΎ when Β¬ π β€ π, given auxiliary atom π. (Contributed by NM, 13-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ πΊ = (β©π β π (πβπ) = π) & β’ πΉ β V & β’ π β V β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (β¨πΉ, πβ© β (πΌβπ) β ((πΉ β π β§ π β πΈ) β§ (π β(πΉ β β‘(πβπΊ))) β€ π))) | ||
Theorem | dihlss 40425 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β π) | ||
Theorem | dihss 40426 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β π) | ||
Theorem | dihssxp 40427 | An isomorphism H value is included in the vector space (expressed as π Γ πΈ). (Contributed by NM, 26-Sep-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (πΌβπ) β (π Γ πΈ)) | ||
Theorem | dihopcl 40428 | Closure of an ordered pair (vector) member of a value of isomorphism H. (Contributed by NM, 26-Sep-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β β¨πΉ, πβ© β (πΌβπ)) β β’ (π β (πΉ β π β§ π β πΈ)) | ||
Theorem | xihopellsmN 40429* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π΄ = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((DVecHβπΎ)βπ) & β’ πΏ = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (πΉ = (π β β) β§ π = (π‘π΄π’))))) | ||
Theorem | dihopellsm 40430* | Ordered pair membership in a subspace sum of isomorphism H values. (Contributed by NM, 26-Sep-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π΄ = (π£ β πΈ, π€ β πΈ β¦ (π β π β¦ ((π£βπ) β (π€βπ)))) & β’ π = ((DVecHβπΎ)βπ) & β’ πΏ = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) & β’ (π β π β π΅) β β’ (π β (β¨πΉ, πβ© β ((πΌβπ) β (πΌβπ)) β βπβπ‘βββπ’((β¨π, π‘β© β (πΌβπ) β§ β¨β, π’β© β (πΌβπ)) β§ (πΉ = (π β β) β§ π = (π‘π΄π’))))) | ||
Theorem | dihord6apre 40431* | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΊ = (β©β β π (ββπ) = π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord3 40432 | The isomorphism H for a lattice πΎ is order-preserving in the region under co-atom π. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) | ||
Theorem | dihord4 40433 | The isomorphism H for a lattice πΎ is order-preserving in the region not under co-atom π. TODO: reformat (π β π΄ β§ Β¬ π β€ π) to eliminate adant*. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) | ||
Theorem | dihord5b 40434 | Part of proof that isomorphism H is order-preserving. TODO: eliminate 3ad2ant1; combine with other way to have one lhpmcvr2 . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ π β€ π) β (πΌβπ) β (πΌβπ)) | ||
Theorem | dihord6b 40435 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ π β€ π) β (πΌβπ) β (πΌβπ)) | ||
Theorem | dihord6a 40436 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord5apre 40437 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord5a 40438 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord 40439 | The isomorphism H is order-preserving. Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β ((πΌβπ) β (πΌβπ) β π β€ π)) | ||
Theorem | dih11 40440 | The isomorphism H is one-to-one. Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β ((πΌβπ) = (πΌβπ) β π = π)) | ||
Theorem | dihf11lem 40441 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β πΌ:π΅βΆπ) | ||
Theorem | dihf11 40442 | The isomorphism H for a lattice πΎ is a one-to-one function. Part of proof after Lemma N of [Crawley] p. 122 line 6. (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β πΌ:π΅β1-1βπ) | ||
Theorem | dihfn 40443 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΌ Fn π΅) | ||
Theorem | dihdm 40444 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β dom πΌ = π΅) | ||
Theorem | dihcl 40445 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β ran πΌ) | ||
Theorem | dihcnvcl 40446 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β π΅) | ||
Theorem | dihcnvid1 40447 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (β‘πΌβ(πΌβπ)) = π) | ||
Theorem | dihcnvid2 40448 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) | ||
Theorem | dihcnvord 40449 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β ((β‘πΌβπ) β€ (β‘πΌβπ) β π β π)) | ||
Theorem | dihcnv11 40450 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β ((β‘πΌβπ) = (β‘πΌβπ) β π = π)) | ||
Theorem | dihsslss 40451 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β ran πΌ β π) | ||
Theorem | dihrnlss 40452 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dihrnss 40453 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dihvalrel 40454 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β Rel (πΌβπ)) | ||
Theorem | dih0 40455 | The value of isomorphism H at the lattice zero is the singleton of the zero vector i.e. the zero subspace. (Contributed by NM, 9-Mar-2014.) |
β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (0gβπ) β β’ ((πΎ β HL β§ π β π») β (πΌβ 0 ) = {π}) | ||
Theorem | dih0bN 40456 | A lattice element is zero iff its isomorphism is the zero subspace. (Contributed by NM, 16-Aug-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ 0 = (0.βπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (0gβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (π = 0 β (πΌβπ) = {π})) | ||
Theorem | dih0vbN 40457 | A vector is zero iff its span is the isomorphism of lattice zero. (Contributed by NM, 16-Aug-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ 0 = (0.βπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π) β β’ (π β (π = π β (πβ{π}) = (πΌβ 0 ))) | ||
Theorem | dih0cnv 40458 | The isomorphism H converse value of the zero subspace is the lattice zero. (Contributed by NM, 19-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ 0 = (0.βπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (0gβπ) β β’ ((πΎ β HL β§ π β π») β (β‘πΌβ{π}) = 0 ) | ||
Theorem | dih0rn 40459 | The zero subspace belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ 0 = (0gβπ) β β’ ((πΎ β HL β§ π β π») β { 0 } β ran πΌ) | ||
Theorem | dih0sb 40460 | A subspace is zero iff the converse of its isomorphism is lattice zero. (Contributed by NM, 17-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ 0 = (0.βπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (0gβπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) β β’ (π β (π = {π} β (β‘πΌβπ) = 0 )) | ||
Theorem | dih1 40461 | The value of isomorphism H at the lattice unity is the set of all vectors. (Contributed by NM, 13-Mar-2014.) |
β’ 1 = (1.βπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ ((πΎ β HL β§ π β π») β (πΌβ 1 ) = π) | ||
Theorem | dih1rn 40462 | The full vector space belongs to the range of isomorphism H. (Contributed by NM, 19-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ ((πΎ β HL β§ π β π») β π β ran πΌ) | ||
Theorem | dih1cnv 40463 | The isomorphism H converse value of the full vector space is the lattice one. (Contributed by NM, 19-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ 1 = (1.βπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ ((πΎ β HL β§ π β π») β (β‘πΌβπ) = 1 ) | ||
Theorem | dihwN 40464* | Value of isomorphism H at the fiducial hyperplane π. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πΌβπ) = (π Γ { 0 })) | ||
Theorem | dihmeetlem1N 40465* | Isomorphism H of a conjunction. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΊ = (β©β β π (ββπ) = π) & β’ 0 = (β β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihglblem5apreN 40466* | A conjunction property of isomorphism H. TODO: reduce antecedent size; general review for shorter proof. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΊ = (β©β β π (ββπ) = π) & β’ 0 = (β β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihglblem5aN 40467 | A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihglblem2aN 40468* | Lemma for isomorphism H of a GLB. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β π β β ) | ||
Theorem | dihglblem2N 40469* | The GLB of a set of lattice elements π is the same as that of the set π with elements of π cut down to be under π. (Contributed by NM, 19-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (πΊβπ) β€ π) β (πΊβπ) = (πΊβπ)) | ||
Theorem | dihglblem3N 40470* | Isomorphism H of a lattice glb. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} & β’ π½ = ((DIsoBβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β ) β§ (πΊβπ) β€ π) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglblem3aN 40471* | Isomorphism H of a lattice glb. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} & β’ π½ = ((DIsoBβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β ) β§ (πΊβπ) β€ π) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglblem4 40472* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} & β’ π½ = ((DIsoBβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglblem5 40473* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β β© π₯ β π (πΌβπ₯) β π) | ||
Theorem | dihmeetlem2N 40474 | Isomorphism H of a conjunction. (Contributed by NM, 22-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΊ = (β©β β π (ββπ) = π) & β’ 0 = (β β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihglbcpreN 40475* | Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane π. (Contributed by NM, 20-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β ) β§ Β¬ (πΊβπ) β€ π) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglbcN 40476* | Isomorphism H of a lattice glb when the glb is not under the fiducial hyperplane π. (Contributed by NM, 26-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ β€ = (leβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β ) β§ Β¬ (πΊβπ) β€ π) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihmeetcN 40477 | Isomorphism H of a lattice meet when the meet is not under the fiducial hyperplane π. (Contributed by NM, 26-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ Β¬ (π β§ π) β€ π) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihmeetbN 40478 | Isomorphism H of a lattice meet when one element is under the fiducial hyperplane π. (Contributed by NM, 26-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΅ β§ π β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihmeetbclemN 40479 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β (πΌβ(π β§ π)) = (((πΌβπ) β© (πΌβπ)) β© (πΌβπ))) | ||
Theorem | dihmeetlem3N 40480 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β π β π ) | ||
Theorem | dihmeetlem4preN 40481* | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ 0 = (0gβπ) & β’ πΊ = (β©π β π (πβπ) = π) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΌβπ) β© (πΌβ(π β§ π))) = { 0 }) | ||
Theorem | dihmeetlem4N 40482 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 30-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ 0 = (0gβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΌβπ) β© (πΌβ(π β§ π))) = { 0 }) | ||
Theorem | dihmeetlem5 40483 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ π β€ π)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ π)) | ||
Theorem | dihmeetlem6 40484 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β Β¬ (π β§ (π β¨ π)) β€ π) | ||
Theorem | dihmeetlem7N 40485 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ Β¬ π β€ π)) β (((π β§ π) β¨ π) β§ π) = (π β§ π)) | ||
Theorem | dihjatc1 40486 | Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we change β¨ order of (π β§ π) β¨ π here and down? (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ (π β§ π) β€ π)) β (πΌβ((π β§ π) β¨ π)) = ((πΌβπ) β (πΌβ(π β§ π)))) | ||
Theorem | dihjatc2N 40487 | Isomorphism H of join with an atom. (Contributed by NM, 26-Aug-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ (π β§ π) β€ π)) β (πΌβ(π β¨ (π β§ π))) = ((πΌβπ) β (πΌβ(π β§ π)))) | ||
Theorem | dihjatc3 40488 | Isomorphism H of join with an atom. (Contributed by NM, 26-Aug-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ (π β§ π) β€ π)) β (πΌβ((π β§ π) β¨ π)) = ((πΌβ(π β§ π)) β (πΌβπ))) | ||
Theorem | dihmeetlem8N 40489 | Lemma for isomorphism H of a lattice meet. TODO: shorter proof if we change β¨ order of (π β§ π) β¨ π here and down? (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ (π β§ π) β€ π)) β (πΌβ((π β§ π) β¨ π)) = ((πΌβπ) β (πΌβ(π β§ π)))) | ||
Theorem | dihmeetlem9N 40490 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ π β π΄) β (((πΌβπ) β (πΌβ(π β§ π))) β© (πΌβπ)) = ((πΌβ(π β§ π)) β ((πΌβπ) β© (πΌβπ)))) | ||
Theorem | dihmeetlem10N 40491 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (πΌβ((π β§ π) β¨ π)) = ((πΌβπ) β© (πΌβ(π β¨ π)))) | ||
Theorem | dihmeetlem11N 40492 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((πΌβ((π β§ π) β¨ π)) β© (πΌβπ)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihmeetlem12N 40493 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π β§ (π β§ π) β€ π)) β ((πΌβ(π β§ π)) β ((πΌβπ) β© (πΌβπ))) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihmeetlem13N 40494* | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ 0 = (0gβπ) & β’ πΉ = (β©β β π (ββπ) = π) & β’ πΊ = (β©β β π (ββπ) = π ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π ) β ((πΌβπ) β© (πΌβπ )) = { 0 }) | ||
Theorem | dihmeetlem14N 40495 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π β§ (π β§ π) β€ π)) β ((πΌβ(π β§ π)) β ((πΌβπ) β© (πΌβπ))) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihmeetlem15N 40496 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ 0 = (0gβπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π β§ (π β§ π) β€ π)) β ((πΌβπ) β© (πΌβπ)) = { 0 }) | ||
Theorem | dihmeetlem16N 40497 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π β§ (π β§ π) β€ π)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihmeetlem17N 40498 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ 0 = (0.βπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ (π β§ π) β€ π β§ π β€ π)) β (π β§ π) = 0 ) | ||
Theorem | dihmeetlem18N 40499 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ 0 = (0gβπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ π β€ π β§ (π β§ π) β€ π))) β ((πΌβπ) β© (πΌβπ)) = { 0 }) | ||
Theorem | dihmeetlem19N 40500 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β€ π β§ π β€ π β§ (π β§ π) β€ π))) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |