![]() |
Metamath
Proof Explorer Theorem List (p. 400 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-30171) |
![]() (30172-31694) |
![]() (31695-47852) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | diaffval 39901* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) | ||
Theorem | diafval 39902* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π βπ) β€ π₯})) | ||
Theorem | diaval 39903* | The partial isomorphism A for a lattice πΎ. Definition of isomorphism map in [Crawley] p. 120 line 24. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = {π β π β£ (π βπ) β€ π}) | ||
Theorem | diaelval 39904 | Member of the partial isomorphism A for a lattice πΎ. (Contributed by NM, 3-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΉ β (πΌβπ) β (πΉ β π β§ (π βπΉ) β€ π))) | ||
Theorem | diafn 39905* | Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ Fn {π₯ β π΅ β£ π₯ β€ π}) | ||
Theorem | diadm 39906* | Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β dom πΌ = {π₯ β π΅ β£ π₯ β€ π}) | ||
Theorem | diaeldm 39907 | Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β (π β dom πΌ β (π β π΅ β§ π β€ π))) | ||
Theorem | diadmclN 39908 | A member of domain of the partial isomorphism A is a lattice element. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β π β π΅) | ||
Theorem | diadmleN 39909 | A member of domain of the partial isomorphism A is under the fiducial hyperplane. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β dom πΌ) β π β€ π) | ||
Theorem | dian0 39910 | The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β β ) | ||
Theorem | dia0eldmN 39911 | The lattice zero belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β 0 β dom πΌ) | ||
Theorem | dia1eldmN 39912 | The fiducial hyperplane (the largest allowed lattice element) belongs to the domain of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π β dom πΌ) | ||
Theorem | diass 39913 | The value of the partial isomorphism A is a set of translations, i.e., a set of vectors. (Contributed by NM, 26-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β π) | ||
Theorem | diael 39914 | A member of the value of the partial isomorphism A is a translation, i.e., a vector. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ πΉ β (πΌβπ)) β πΉ β π) | ||
Theorem | diatrl 39915 | Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ πΉ β (πΌβπ)) β (π βπΉ) β€ π) | ||
Theorem | diaelrnN 39916 | Any value of the partial isomorphism A is a set of translations i.e. a set of vectors. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β ran πΌ) β π β π) | ||
Theorem | dialss 39917 | The value of partial isomorphism A is a subspace of partial vector space A. Part of Lemma M of [Crawley] p. 120 line 26. (Contributed by NM, 17-Jan-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β π) | ||
Theorem | diaord 39918 | The partial isomorphism A for a lattice πΎ is order-preserving in the region under co-atom π. Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 26-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) β (πΌβπ) β π β€ π)) | ||
Theorem | dia11N 39919 | The partial isomorphism A for a lattice πΎ is one-to-one in the region under co-atom π. Part of Lemma M of [Crawley] p. 120 line 28. (Contributed by NM, 25-Nov-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β ((πΌβπ) = (πΌβπ) β π = π)) | ||
Theorem | diaf11N 39920 | The partial isomorphism A for a lattice πΎ is a one-to-one function. Part of Lemma M of [Crawley] p. 120 line 27. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β πΌ:dom πΌβ1-1-ontoβran πΌ) | ||
Theorem | diaclN 39921 | Closure of partial isomorphism A for a lattice πΎ. (Contributed by NM, 4-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβπ) β ran πΌ) | ||
Theorem | diacnvclN 39922 | Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β dom πΌ) | ||
Theorem | dia0 39923 | The value of the partial isomorphism A at the lattice zero is the singleton of the identity translation i.e. the zero subspace. (Contributed by NM, 26-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ 0 = (0.βπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (πΌβ 0 ) = {( I βΎ π΅)}) | ||
Theorem | dia1N 39924 | The value of the partial isomorphism A at the fiducial co-atom is the set of all translations i.e. the entire vector space. (Contributed by NM, 26-Nov-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (πΌβπ) = π) | ||
Theorem | dia1elN 39925 | The largest subspace in the range of partial isomorphism A. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π β ran πΌ) | ||
Theorem | diaglbN 39926* | Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β )) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | diameetN 39927 | Partial isomorphism A of a lattice meet. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(π β§ π)) = ((πΌβπ) β© (πΌβπ))) | ||
Theorem | diainN 39928 | Inverse partial isomorphism A of an intersection. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β ran πΌ)) β (π β© π) = (πΌβ((β‘πΌβπ) β§ (β‘πΌβπ)))) | ||
Theorem | diaintclN 39929 | The intersection of partial isomorphism A closed subspaces is a closed subspace. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β ran πΌ β§ π β β )) β β© π β ran πΌ) | ||
Theorem | diasslssN 39930 | The partial isomorphism A maps to subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β ran πΌ β π) | ||
Theorem | diassdvaN 39931 | The partial isomorphism A maps to a set of vectors in partial vector space A. (Contributed by NM, 1-Jan-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β π) | ||
Theorem | dia1dim 39932* | Two expressions for the 1-dimensional subspaces of partial vector space A (when πΉ is a nonzero vector i.e. non-identity translation). Remark after Lemma L in [Crawley] p. 120 line 21. (Contributed by NM, 15-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΌβ(π βπΉ)) = {π β£ βπ β πΈ π = (π βπΉ)}) | ||
Theorem | dia1dim2 39933 | Two expressions for a 1-dimensional subspace of partial vector space A (when πΉ is a nonzero vector i.e. non-identity translation). (Contributed by NM, 15-Jan-2014.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = (LSpanβπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β (πΌβ(π βπΉ)) = (πβ{πΉ})) | ||
Theorem | dia1dimid 39934 | A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ β (πΌβ(π βπΉ))) | ||
Theorem | dia2dimlem1 39935 | Lemma for dia2dim 39948. Show properties of the auxiliary atom π. Part of proof of Lemma M in [Crawley] p. 121 line 3. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β (πΉ β π β§ (πΉβπ) β π)) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) β β’ (π β (π β π΄ β§ Β¬ π β€ π)) | ||
Theorem | dia2dimlem2 39936 | Lemma for dia2dim 39948. Define a translation πΊ whose trace is atom π. Part of proof of Lemma M in [Crawley] p. 121 line 4. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β (πΉ β π β§ (πΉβπ) β π)) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β (π βπΉ) β π) & β’ (π β πΊ β π) & β’ (π β (πΊβπ) = π) β β’ (π β (π βπΊ) = π) | ||
Theorem | dia2dimlem3 39937 | Lemma for dia2dim 39948. Define a translation π· whose trace is atom π. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β (πΉ β π β§ (πΉβπ) β π)) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) & β’ (π β π· β π) & β’ (π β (π·βπ) = (πΉβπ)) β β’ (π β (π βπ·) = π) | ||
Theorem | dia2dimlem4 39938 | Lemma for dia2dim 39948. Show that the composition (sum) of translations (vectors) πΊ and π· equals πΉ. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β πΉ β π) & β’ (π β πΊ β π) & β’ (π β (πΊβπ) = π) & β’ (π β π· β π) & β’ (π β (π·βπ) = (πΉβπ)) β β’ (π β (π· β πΊ) = πΉ) | ||
Theorem | dia2dimlem5 39939 | Lemma for dia2dim 39948. The sum of vectors πΊ and π· belongs to the sum of the subspaces generated by them. Thus, πΉ = (πΊ β π·) belongs to the subspace sum. Part of proof of Lemma M in [Crawley] p. 121 line 5. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β (πΉ β π β§ (πΉβπ) β π)) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) & β’ (π β πΊ β π) & β’ (π β (πΊβπ) = π) & β’ (π β π· β π) & β’ (π β (π·βπ) = (πΉβπ)) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem6 39940 | Lemma for dia2dim 39948. Eliminate auxiliary translations πΊ and π·. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β (πΉ β π β§ (πΉβπ) β π)) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem7 39941 | Lemma for dia2dim 39948. Eliminate (πΉβπ) β π condition. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem8 39942 | Lemma for dia2dim 39948. Eliminate no-longer used auxiliary atoms π and π. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem9 39943 | Lemma for dia2dim 39948. Eliminate (π βπΉ) β π, π conditions. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem10 39944 | Lemma for dia2dim 39948. Convert membership in closed subspace (πΌβ(π β¨ π)) to a lattice ordering. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β πΉ β π) & β’ (π β πΉ β (πΌβ(π β¨ π))) β β’ (π β (π βπΉ) β€ (π β¨ π)) | ||
Theorem | dia2dimlem11 39945 | Lemma for dia2dim 39948. Convert ordering hypothesis on π βπΉ to subspace membership πΉ β (πΌβ(π β¨ π)). (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β πΉ β π) & β’ (π β π β π) & β’ (π β πΉ β (πΌβ(π β¨ π))) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem12 39946 | Lemma for dia2dim 39948. Obtain subset relation. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β π β π) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem13 39947 | Lemma for dia2dim 39948. Eliminate π β π condition. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dim 39948 | A two-dimensional subspace of partial vector space A is closed, or equivalently, the isomorphism of a join of two atoms is a subset of the subspace sum of the isomorphisms of each atom (and thus they are equal, as shown later for the full vector space H). (Contributed by NM, 9-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ β = (LSSumβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Syntax | cdvh 39949 | Extend class notation with constructed full vector space H. |
class DVecH | ||
Definition | df-dvech 39950* | Define constructed full vector space H. (Contributed by NM, 17-Oct-2013.) |
β’ DVecH = (π β V β¦ (π€ β (LHypβπ) β¦ ({β¨(Baseβndx), (((LTrnβπ)βπ€) Γ ((TEndoβπ)βπ€))β©, β¨(+gβndx), (π β (((LTrnβπ)βπ€) Γ ((TEndoβπ)βπ€)), π β (((LTrnβπ)βπ€) Γ ((TEndoβπ)βπ€)) β¦ β¨((1st βπ) β (1st βπ)), (β β ((LTrnβπ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx), ((EDRingβπ)βπ€)β©} βͺ {β¨( Β·π βndx), (π β ((TEndoβπ)βπ€), π β (((LTrnβπ)βπ€) Γ ((TEndoβπ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) | ||
Theorem | dvhfset 39951* | The constructed full vector space H for a lattice πΎ. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DVecHβπΎ) = (π€ β π» β¦ ({β¨(Baseβndx), (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€))β©, β¨(+gβndx), (π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨((1st βπ) β (1st βπ)), (β β ((LTrnβπΎ)βπ€) β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx), ((EDRingβπΎ)βπ€)β©} βͺ {β¨( Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β (((LTrnβπΎ)βπ€) Γ ((TEndoβπΎ)βπ€)) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©}))) | ||
Theorem | dvhset 39952* | The constructed full vector space H for a lattice πΎ. (Contributed by NM, 17-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = ({β¨(Baseβndx), (π Γ πΈ)β©, β¨(+gβndx), (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), (β β π β¦ (((2nd βπ)ββ) β ((2nd βπ)ββ)))β©)β©, β¨(Scalarβndx), π·β©} βͺ {β¨( Β·π βndx), (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)β©})) | ||
Theorem | dvhsca 39953 | The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) β β’ ((πΎ β π β§ π β π») β πΉ = π·) | ||
Theorem | dvhbase 39954 | The ring base set of the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ πΆ = (BaseβπΉ) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
Theorem | dvhfplusr 39955* | Ring addition operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ β = (+gβπΉ) β β’ ((πΎ β π β§ π β π») β β = + ) | ||
Theorem | dvhfmulr 39956* | Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
Theorem | dvhmulr 39957 | Ring multiplication operation for the constructed full vector space H. (Contributed by NM, 29-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | dvhvbase 39958 | The vectors (vector base set) of the constructed full vector space H are all translations (for a fiducial co-atom π). (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ ((πΎ β π β§ π β π») β π = (π Γ πΈ)) | ||
Theorem | dvhelvbasei 39959 | Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨πΉ, πβ© β π) | ||
Theorem | dvhvaddcbv 39960* | Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.) |
β’ + = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ) ⨣ (2nd βπ))β©) β β’ + = (β β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st ββ) β (1st βπ)), ((2nd ββ) ⨣ (2nd βπ))β©) | ||
Theorem | dvhvaddval 39961* | The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) |
β’ + = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ) ⨣ (2nd βπ))β©) β β’ ((πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ)) β (πΉ + πΊ) = β¨((1st βπΉ) β (1st βπΊ)), ((2nd βπΉ) ⨣ (2nd βπΊ))β©) | ||
Theorem | dvhfvadd 39962* | The vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ β = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ) ⨣ (2nd βπ))β©) & β’ + = (+gβπ) β β’ ((πΎ β HL β§ π β π») β + = β ) | ||
Theorem | dvhvadd 39963 | The vector sum operation for the constructed full vector space H. (Contributed by NM, 11-Feb-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) = β¨((1st βπΉ) β (1st βπΊ)), ((2nd βπΉ) ⨣ (2nd βπΊ))β©) | ||
Theorem | dvhopvadd 39964 | The vector sum operation for the constructed full vector space H. (Contributed by NM, 21-Feb-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & β’ + = (+gβπ) & ⒠⨣ = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ© + β¨πΊ, π β©) = β¨(πΉ β πΊ), (π ⨣ π )β©) | ||
Theorem | dvhopvadd2 39965* | The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 39964 and/or dvhfplusr 39955. (Contributed by NM, 26-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ© β β¨πΊ, π β©) = β¨(πΉ β πΊ), (π + π )β©) | ||
Theorem | dvhvaddcl 39966 | Closure of the vector sum operation for the constructed full vector space H. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) β (π Γ πΈ)) | ||
Theorem | dvhvaddcomN 39967 | Commutativity of vector sum. (Contributed by NM, 26-Oct-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ))) β (πΉ + πΊ) = (πΊ + πΉ)) | ||
Theorem | dvhvaddass 39968 | Associativity of vector sum. (Contributed by NM, 31-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((πΉ + πΊ) + πΌ) = (πΉ + (πΊ + πΌ))) | ||
Theorem | dvhvscacbv 39969* | Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.) |
β’ Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ Β· = (π‘ β πΈ, π β (π Γ πΈ) β¦ β¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) | ||
Theorem | dvhvscaval 39970* | The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.) |
β’ Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ ((π β πΈ β§ πΉ β (π Γ πΈ)) β (π Β· πΉ) = β¨(πβ(1st βπΉ)), (π β (2nd βπΉ))β©) | ||
Theorem | dvhfvsca 39971* | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©)) | ||
Theorem | dvhvsca 39972 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β (π Γ πΈ))) β (π Β· πΉ) = β¨(π β(1st βπΉ)), (π β (2nd βπΉ))β©) | ||
Theorem | dvhopvsca 39973 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ π β πΈ)) β (π Β· β¨πΉ, πβ©) = β¨(π βπΉ), (π β π)β©) | ||
Theorem | dvhvscacl 39974 | Closure of the scalar product operation for the constructed full vector space H. (Contributed by NM, 12-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β (π Γ πΈ))) β (π Β· πΉ) β (π Γ πΈ)) | ||
Theorem | tendoinvcl 39975* | Closure of multiplicative inverse for endomorphism. We use the scalar inverse of the vector space since it is much simpler than the direct inverse of cdleml8 39854. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (invrβπΉ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((πβπ) β πΈ β§ (πβπ) β π)) | ||
Theorem | tendolinv 39976* | Left multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (invrβπΉ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((πβπ) β π) = ( I βΎ π)) | ||
Theorem | tendorinv 39977* | Right multiplicative inverse for endomorphism. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (invrβπΉ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β (π β (πβπ)) = ( I βΎ π)) | ||
Theorem | dvhgrp 39978 | The full vector space π constructed from a Hilbert lattice πΎ (given a fiducial hyperplane π) is a group. (Contributed by NM, 19-Oct-2013.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) & β’ 0 = (0gβπ·) & β’ πΌ = (invgβπ·) β β’ ((πΎ β HL β§ π β π») β π β Grp) | ||
Theorem | dvhlveclem 39979 | Lemma for dvhlvec 39980. TODO: proof substituting inner part first shorter/longer than substituting outer part first? TODO: break up into smaller lemmas? TODO: does π β method shorten proof? (Contributed by NM, 22-Oct-2013.) (Proof shortened by Mario Carneiro, 24-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) & β’ 0 = (0gβπ·) & β’ πΌ = (invgβπ·) & β’ Γ = (.rβπ·) & β’ Β· = ( Β·π βπ) β β’ ((πΎ β HL β§ π β π») β π β LVec) | ||
Theorem | dvhlvec 39980 | The full vector space π constructed from a Hilbert lattice πΎ (given a fiducial hyperplane π) is a left module. (Contributed by NM, 23-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π β LVec) | ||
Theorem | dvhlmod 39981 | The full vector space π constructed from a Hilbert lattice πΎ (given a fiducial hyperplane π) is a left module. (Contributed by NM, 23-May-2015.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β π β LMod) | ||
Theorem | dvh0g 39982* | The zero vector of vector space H has the zero translation as its first member and the zero trace-preserving endomorphism as the second. (Contributed by NM, 9-Mar-2014.) (Revised by Mario Carneiro, 24-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ 0 = (0gβπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ ((πΎ β HL β§ π β π») β 0 = β¨( I βΎ π΅), πβ©) | ||
Theorem | dvheveccl 39983 | Properties of a unit vector that we will use later as a convenient reference vector. This vector is called "e" in the remark after Lemma M of [Crawley] p. 121. line 17. See also dvhopN 39987 and dihpN 40207. (Contributed by NM, 27-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΈ = β¨( I βΎ π΅), ( I βΎ π)β© & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΈ β (π β { 0 })) | ||
Theorem | dvhopclN 39984 | Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ ((πΉ β π β§ π β πΈ) β β¨πΉ, πβ© β (π Γ πΈ)) | ||
Theorem | dvhopaddN 39985* | Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ π΄ = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ)π(2nd βπ))β©) β β’ (((πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ©π΄β¨πΊ, πβ©) = β¨(πΉ β πΊ), (πππ)β©) | ||
Theorem | dvhopspN 39986* | Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ π = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ ((π β πΈ β§ (πΉ β π β§ π β πΈ)) β (π πβ¨πΉ, πβ©) = β¨(π βπΉ), (π β π)β©) | ||
Theorem | dvhopN 39987* | Decompose a DVecH vector expressed as an ordered pair into the sum of two components, the first from the translation group vector base of DVecA and the other from the one-dimensional vector subspace πΈ. Part of Lemma M of [Crawley] p. 121, line 18. We represent their e, sigma, f by β¨( I βΎ π΅), ( I βΎ π)β©, π, β¨πΉ, πβ©. We swapped the order of vector sum (their juxtaposition i.e. composition) to show β¨πΉ, πβ© first. Note that π and ( I βΎ π) are the zero and one of the division ring πΈ, and ( I βΎ π΅) is the zero of the translation group. π is the scalar product. (Contributed by NM, 21-Nov-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π΄ = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ)π(2nd βπ))β©) & β’ π = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨πΉ, πβ© = (β¨πΉ, πβ©π΄(ππβ¨( I βΎ π΅), ( I βΎ π)β©))) | ||
Theorem | dvhopellsm 39988* | Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (β¨πΉ, πβ© β (π β π) β βπ₯βπ¦βπ§βπ€((β¨π₯, π¦β© β π β§ β¨π§, π€β© β π) β§ β¨πΉ, πβ© = (β¨π₯, π¦β© + β¨π§, π€β©)))) | ||
Theorem | cdlemm10N 39989* | The image of the map πΊ is the entire one-dimensional subspace (πΌβπ). Remark after Lemma M of [Crawley] p. 121 line 23. (Contributed by NM, 24-Nov-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ πΆ = {π β π΄ β£ (π β€ (π β¨ π) β§ Β¬ π β€ π)} & β’ πΉ = (β©π β π (πβπ) = π ) & β’ πΊ = (π β πΆ β¦ (β©π β π (πβπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β€ π)) β ran πΊ = (πΌβπ)) | ||
Syntax | cocaN 39990 | Extend class notation with subspace orthocomplement for DVecA partial vector space. |
class ocA | ||
Definition | df-docaN 39991* | Define subspace orthocomplement for DVecA partial 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, 6-Dec-2013.) |
β’ ocA = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€) β¦ (((DIsoAβπ)βπ€)β((((ocβπ)β(β‘((DIsoAβπ)βπ€)ββ© {π§ β ran ((DIsoAβπ)βπ€) β£ π₯ β π§}))(joinβπ)((ocβπ)βπ€))(meetβπ)π€))))) | ||
Theorem | docaffvalN 39992* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (ocAβπΎ) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€) β¦ (((DIsoAβπΎ)βπ€)β((( β₯ β(β‘((DIsoAβπΎ)βπ€)ββ© {π§ β ran ((DIsoAβπΎ)βπ€) β£ π₯ β π§})) β¨ ( β₯ βπ€)) β§ π€))))) | ||
Theorem | docafvalN 39993* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((ocAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = (π₯ β π« π β¦ (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π₯ β π§})) β¨ ( β₯ βπ)) β§ π)))) | ||
Theorem | docavalN 39994* | Subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π) β (πβπ) = (πΌβ((( β₯ β(β‘πΌββ© {π§ β ran πΌ β£ π β π§})) β¨ ( β₯ βπ)) β§ π))) | ||
Theorem | docaclN 39995 | Closure of subspace orthocomplement for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β π) β ( β₯ βπ) β ran πΌ) | ||
Theorem | diaocN 39996 | Value of partial isomorphism A at lattice orthocomplement (using a Sasaki projection to get orthocomplement relative to the fiducial co-atom π). (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β (πΌβ((( β₯ βπ) β¨ ( β₯ βπ)) β§ π)) = (πβ(πΌβπ))) | ||
Theorem | doca2N 39997 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β ( β₯ β( β₯ β(πΌβπ))) = (πΌβπ)) | ||
Theorem | doca3N 39998 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | dvadiaN 39999 | Any closed subspace is a member of the range of partial isomorphism A, showing the isomorphism maps onto the set of closed subspaces of partial vector space A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π β§ ( β₯ β( β₯ βπ)) = π)) β π β ran πΌ) | ||
Theorem | diarnN 40000* | Partial isomorphism A maps onto the set of all closed subspaces of partial vector space A. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β ran πΌ = {π₯ β π β£ ( β₯ β( β₯ βπ₯)) = π₯}) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |