![]() |
Metamath
Proof Explorer Theorem List (p. 402 of 479) | < 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-30166) |
![]() (30167-31689) |
![]() (31690-47842) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dihvalcqpre 40101 | 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 40102 | Value of isomorphism H for a lattice πΎ when Β¬ π β€ π, given auxiliary atom π. TODO: Use dihvalcq2 40113 (with lhpmcvr3 38891 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 40103 | Value of isomorphism H for a lattice πΎ when π β€ π. (Contributed by NM, 4-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π· = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = (π·βπ)) | ||
Theorem | dihopelvalbN 40104* | 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 40105 | 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 40106* | 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 40107* | 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 40108* | 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 40109 | Extend dia2dim 39943 to partial isomorphism B. (Contributed by NM, 22-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoBβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dih2dimb 40110 | Extend dib2dim 40109 to isomorphism H. (Contributed by NM, 22-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dih2dimbALTN 40111 | Extend dia2dim 39943 to isomorphism H. (This version combines dib2dim 40109 and dih2dimb 40110 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 40112* | 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 40113 | 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 40114* | 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 40115* | 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 40116 | The value of isomorphism H is a subspace. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β π) | ||
Theorem | dihss 40117 | The value of isomorphism H is a set of vectors. (Contributed by NM, 14-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β π) | ||
Theorem | dihssxp 40118 | 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 40119 | 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 40120* | 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 40121* | 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 40122* | 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 40123 | 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 40124 | 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 40125 | 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 40126 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ π β€ π) β (πΌβπ) β (πΌβπ)) | ||
Theorem | dihord6a 40127 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord5apre 40128 | 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 40129 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord 40130 | 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 40131 | 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 40132 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β πΌ:π΅βΆπ) | ||
Theorem | dihf11 40133 | 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 40134 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΌ Fn π΅) | ||
Theorem | dihdm 40135 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β dom πΌ = π΅) | ||
Theorem | dihcl 40136 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β ran πΌ) | ||
Theorem | dihcnvcl 40137 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β π΅) | ||
Theorem | dihcnvid1 40138 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (β‘πΌβ(πΌβπ)) = π) | ||
Theorem | dihcnvid2 40139 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) | ||
Theorem | dihcnvord 40140 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β ((β‘πΌβπ) β€ (β‘πΌβπ) β π β π)) | ||
Theorem | dihcnv11 40141 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β ((β‘πΌβπ) = (β‘πΌβπ) β π = π)) | ||
Theorem | dihsslss 40142 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β ran πΌ β π) | ||
Theorem | dihrnlss 40143 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dihrnss 40144 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dihvalrel 40145 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β Rel (πΌβπ)) | ||
Theorem | dih0 40146 | 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 40147 | 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 40148 | 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 40149 | 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 40150 | 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 40151 | 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 40152 | 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 40153 | 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 40154 | 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 40155* | 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 40156* | 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 40157* | 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 40158 | A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihglblem2aN 40159* | 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 40160* | 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 40161* | 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 40162* | 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 40163* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} & β’ π½ = ((DIsoBβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglblem5 40164* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β β© π₯ β π (πΌβπ₯) β π) | ||
Theorem | dihmeetlem2N 40165 | 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 40166* | 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 40167* | 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 40168 | 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 40169 | 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 40170 | 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 40171 | 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 40172* | 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 40173 | 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 40174 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ π β€ π)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ π)) | ||
Theorem | dihmeetlem6 40175 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β Β¬ (π β§ (π β¨ π)) β€ π) | ||
Theorem | dihmeetlem7N 40176 | 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 40177 | 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 40178 | 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 40179 | 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 40180 | 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 40181 | 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 40182 | 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 40183 | 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 40184 | 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 40185* | 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 40186 | 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 40187 | 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 40188 | 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 40189 | 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 40190 | 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 40191 | 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 | dihmeetlem20N 40192 | 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 | dihmeetALTN 40193 | Isomorphism H of a lattice meet. This version does not depend on the atomisticity of the constructed vector space. TODO: Delete? (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dih1dimatlem0 40194* | Lemma for dih1dimat 40196. (Contributed by NM, 11-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = (AtomsβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ πΉ = (Scalarβπ) & β’ π½ = (invrβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ πΊ = (β©β β π (ββπ) = (((π½βπ )βπ)βπ)) β β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β πΈ) β§ π β π) β ((π = (πβπΊ) β§ π β πΈ) β ((π β π β§ π β πΈ) β§ βπ‘ β πΈ (π = (π‘βπ) β§ π = (π‘ β π ))))) | ||
Theorem | dih1dimatlem 40195* | Lemma for dih1dimat 40196. (Contributed by NM, 10-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ πΆ = (AtomsβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ πΉ = (Scalarβπ) & β’ π½ = (invrβπΉ) & β’ π = (Baseβπ) & β’ Β· = ( Β·π βπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ 0 = (0gβπ) & β’ πΊ = (β©β β π (ββπ) = (((π½βπ )βπ)βπ)) β β’ (((πΎ β HL β§ π β π») β§ π· β π΄) β π· β ran πΌ) | ||
Theorem | dih1dimat 40196 | Any 1-dimensional subspace is a value of isomorphism H. (Contributed by NM, 11-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄) β π β ran πΌ) | ||
Theorem | dihlsprn 40197 | The span of a vector belongs to the range of isomorphism H. (Contributed by NM, 27-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβ{π}) β ran πΌ) | ||
Theorem | dihlspsnssN 40198 | A subspace included in a 1-dim subspace belongs to the range of isomorphism H. (Contributed by NM, 26-Apr-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β (πβ{π})) β (π β π β π β ran πΌ)) | ||
Theorem | dihlspsnat 40199 | The inverse isomorphism H of the span of a singleton is a Hilbert lattice atom. (Contributed by NM, 27-Apr-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β 0 ) β (β‘πΌβ(πβ{π})) β π΄) | ||
Theorem | dihatlat 40200 | The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ πΏ = (LSAtomsβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄) β (πΌβπ) β πΏ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |