Home | Metamath
Proof Explorer Theorem List (p. 397 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46966) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dihssxp 39601 | 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 39602 | 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 39603* | 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 39604* | 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 39605* | 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 39606 | 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 39607 | 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 39608 | 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 39609 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ π β€ π) β (πΌβπ) β (πΌβπ)) | ||
Theorem | dihord6a 39610 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ (π β π΅ β§ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord5apre 39611 | 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 39612 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 7-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΌβπ) β (πΌβπ)) β π β€ π) | ||
Theorem | dihord 39613 | 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 39614 | 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 39615 | Functionality of the isomorphism H. (Contributed by NM, 6-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β πΌ:π΅βΆπ) | ||
Theorem | dihf11 39616 | 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 39617 | Functionality and domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΌ Fn π΅) | ||
Theorem | dihdm 39618 | Domain of isomorphism H. (Contributed by NM, 9-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β dom πΌ = π΅) | ||
Theorem | dihcl 39619 | Closure of isomorphism H. (Contributed by NM, 8-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβπ) β ran πΌ) | ||
Theorem | dihcnvcl 39620 | Closure of isomorphism H converse. (Contributed by NM, 8-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β π΅) | ||
Theorem | dihcnvid1 39621 | The converse isomorphism of an isomorphism. (Contributed by NM, 5-Aug-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (β‘πΌβ(πΌβπ)) = π) | ||
Theorem | dihcnvid2 39622 | The isomorphism of a converse isomorphism. (Contributed by NM, 5-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (πΌβ(β‘πΌβπ)) = π) | ||
Theorem | dihcnvord 39623 | Ordering property for converse of isomorphism H. (Contributed by NM, 17-Aug-2014.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β ((β‘πΌβπ) β€ (β‘πΌβπ) β π β π)) | ||
Theorem | dihcnv11 39624 | The converse of isomorphism H is one-to-one. (Contributed by NM, 17-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β ((β‘πΌβπ) = (β‘πΌβπ) β π = π)) | ||
Theorem | dihsslss 39625 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β ran πΌ β π) | ||
Theorem | dihrnlss 39626 | The isomorphism H maps to subspaces. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dihrnss 39627 | The isomorphism H maps to a set of vectors. (Contributed by NM, 14-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dihvalrel 39628 | The value of isomorphism H is a relation. (Contributed by NM, 9-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β Rel (πΌβπ)) | ||
Theorem | dih0 39629 | 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 39630 | 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 39631 | 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 39632 | 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 39633 | 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 39634 | 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 39635 | 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 39636 | 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 39637 | 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 39638* | 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 39639* | 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 39640* | 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 39641 | A conjunction property of isomorphism H. (Contributed by NM, 21-Mar-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihglblem2aN 39642* | 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 39643* | 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 39644* | 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 39645* | 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 39646* | Isomorphism H of a lattice glb. (Contributed by NM, 21-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = {π’ β π΅ β£ βπ£ β π π’ = (π£ β§ π)} & β’ π½ = ((DIsoBβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β (πΌβ(πΊβπ)) β β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglblem5 39647* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β β© π₯ β π (πΌβπ₯) β π) | ||
Theorem | dihmeetlem2N 39648 | 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 39649* | 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 39650* | 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 39651 | 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 39652 | 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 39653 | 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 39654 | 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 39655* | 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 39656 | 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 39657 | Part of proof that isomorphism H is order-preserving . (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ π β€ π)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ π)) | ||
Theorem | dihmeetlem6 39658 | Lemma for isomorphism H of a lattice meet. (Contributed by NM, 6-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β Β¬ (π β§ (π β¨ π)) β€ π) | ||
Theorem | dihmeetlem7N 39659 | 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 39660 | 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 39661 | 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 39662 | 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 39663 | 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 39664 | 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 39665 | 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 39666 | 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 39667 | 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 39668* | 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 39669 | 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 39670 | 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 39671 | 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 39672 | 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 39673 | 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 39674 | 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 39675 | 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 39676 | 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 39677* | Lemma for dih1dimat 39679. (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 39678* | Lemma for dih1dimat 39679. (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 39679 | Any 1-dimensional subspace is a value of isomorphism H. (Contributed by NM, 11-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄) β π β ran πΌ) | ||
Theorem | dihlsprn 39680 | 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 39681 | 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 39682 | 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 39683 | The isomorphism H of an atom is a 1-dim subspace. (Contributed by NM, 28-Apr-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ πΏ = (LSAtomsβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΄) β (πΌβπ) β πΏ) | ||
Theorem | dihat 39684 | There exists at least one atom in the subspaces of vector space H. (Contributed by NM, 12-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π΄ = (LSAtomsβπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (πΌβπ) β π΄) | ||
Theorem | dihpN 39685* | The value of isomorphism H at the fiducial atom π is determined by the vector β¨0, πβ© (the zero translation ltrnid 38484 and a nonzero member of the endomorphism ring). In particular, π can be replaced with the ring unity ( I βΎ π). (Contributed by NM, 26-Aug-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSpanβπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β πΈ β§ π β π)) β β’ (π β (πΌβπ) = (πβ{β¨( I βΎ π΅), πβ©})) | ||
Theorem | dihlatat 39686 | The reverse isomorphism H of a 1-dim subspace is an atom. (Contributed by NM, 28-Apr-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ πΏ = (LSAtomsβπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΏ) β (β‘πΌβπ) β π΄) | ||
Theorem | dihatexv 39687* | There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 16-Aug-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β π΅) β β’ (π β (π β π΄ β βπ₯ β (π β { 0 })(πΌβπ) = (πβ{π₯}))) | ||
Theorem | dihatexv2 39688* | There is a nonzero vector that maps to every lattice atom. (Contributed by NM, 17-Aug-2014.) |
β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β (π β π΄ β βπ₯ β (π β { 0 })π = (β‘πΌβ(πβ{π₯})))) | ||
Theorem | dihglblem6 39689* | Isomorphism H of a lattice glb. (Contributed by NM, 9-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π· = (LSAtomsβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglb 39690* | Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β β )) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | dihglb2 39691* | Isomorphism H of a lattice glb. (Contributed by NM, 11-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π) β (πΌβ(πΊβ{π₯ β π΅ β£ π β (πΌβπ₯)})) = β© {π¦ β ran πΌ β£ π β π¦}) | ||
Theorem | dihmeet 39692 | Isomorphism H of a lattice meet. (Contributed by NM, 13-Apr-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | dihintcl 39693 | The intersection of closed subspaces (the range of isomorphism H) is a closed subspace. (Contributed by NM, 14-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β β )) β β© π β ran πΌ) | ||
Theorem | dihmeetcl 39694 | Closure of closed subspace meet for DVecH vector space. (Contributed by NM, 5-Aug-2014.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (π β© π) β ran πΌ) | ||
Theorem | dihmeet2 39695 | Reverse isomorphism H of a closed subspace intersection. (Contributed by NM, 15-Jan-2015.) |
β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β π β ran πΌ) & β’ (π β π β ran πΌ) β β’ (π β (β‘πΌβ(π β© π)) = ((β‘πΌβπ) β§ (β‘πΌβπ))) | ||
Syntax | coch 39696 | Extend class notation with subspace orthocomplement for DVecH vector space. |
class ocH | ||
Definition | df-doch 39697* | Define subspace orthocomplement for DVecH vector space. Temporarily, we are using the range of the isomorphism instead of the set of closed subspaces. Later, when inner product is introduced, we will show that these are the same. (Contributed by NM, 14-Mar-2014.) |
β’ ocH = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π« (Baseβ((DVecHβπ)βπ€)) β¦ (((DIsoHβπ)βπ€)β((ocβπ)β((glbβπ)β{π¦ β (Baseβπ) β£ π₯ β (((DIsoHβπ)βπ€)βπ¦)})))))) | ||
Theorem | dochffval 39698* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (ocHβπΎ) = (π€ β π» β¦ (π₯ β π« (Baseβ((DVecHβπΎ)βπ€)) β¦ (((DIsoHβπΎ)βπ€)β( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (((DIsoHβπΎ)βπ€)βπ¦)})))))) | ||
Theorem | dochfval 39699* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = ((ocHβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = (π₯ β π« π β¦ (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π₯ β (πΌβπ¦)}))))) | ||
Theorem | dochval 39700* | Subspace orthocomplement for DVecH vector space. (Contributed by NM, 14-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ πΊ = (glbβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoHβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ π = ((ocHβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β π) β (πβπ) = (πΌβ( β₯ β(πΊβ{π¦ β π΅ β£ π β (πΌβπ¦)})))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |