Home | Metamath
Proof Explorer Theorem List (p. 395 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-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | dia0 39401 | 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 39402 | 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 39403 | 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 39404* | Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β )) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | diameetN 39405 | 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 39406 | 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 39407 | 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 39408 | 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 39409 | 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 39410* | 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 39411 | 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 39412 | A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ β (πΌβ(π βπΉ))) | ||
Theorem | dia2dimlem1 39413 | Lemma for dia2dim 39426. 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 39414 | Lemma for dia2dim 39426. 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 39415 | Lemma for dia2dim 39426. 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 39416 | Lemma for dia2dim 39426. 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 39417 | Lemma for dia2dim 39426. 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 39418 | Lemma for dia2dim 39426. 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 39419 | Lemma for dia2dim 39426. Eliminate (πΉβπ) β π condition. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem8 39420 | Lemma for dia2dim 39426. 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 39421 | Lemma for dia2dim 39426. Eliminate (π βπΉ) β π, π conditions. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem10 39422 | Lemma for dia2dim 39426. 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 39423 | Lemma for dia2dim 39426. 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 39424 | Lemma for dia2dim 39426. Obtain subset relation. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β π β π) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem13 39425 | Lemma for dia2dim 39426. Eliminate π β π condition. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dim 39426 | 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 39427 | Extend class notation with constructed full vector space H. |
class DVecH | ||
Definition | df-dvech 39428* | 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 39429* | 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 39430* | 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 39431 | The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) β β’ ((πΎ β π β§ π β π») β πΉ = π·) | ||
Theorem | dvhbase 39432 | 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 39433* | 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 39434* | 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 39435 | 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 39436 | 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 39437 | Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨πΉ, πβ© β π) | ||
Theorem | dvhvaddcbv 39438* | Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.) |
β’ + = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ) ⨣ (2nd βπ))β©) β β’ + = (β β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st ββ) β (1st βπ)), ((2nd ββ) ⨣ (2nd βπ))β©) | ||
Theorem | dvhvaddval 39439* | 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 39440* | 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 39441 | 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 39442 | 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 39443* | The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 39442 and/or dvhfplusr 39433. (Contributed by NM, 26-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ© β β¨πΊ, π β©) = β¨(πΉ β πΊ), (π + π )β©) | ||
Theorem | dvhvaddcl 39444 | 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 39445 | 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 39446 | Associativity of vector sum. (Contributed by NM, 31-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((πΉ + πΊ) + πΌ) = (πΉ + (πΊ + πΌ))) | ||
Theorem | dvhvscacbv 39447* | Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.) |
β’ Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ Β· = (π‘ β πΈ, π β (π Γ πΈ) β¦ β¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) | ||
Theorem | dvhvscaval 39448* | The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.) |
β’ Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ ((π β πΈ β§ πΉ β (π Γ πΈ)) β (π Β· πΉ) = β¨(πβ(1st βπΉ)), (π β (2nd βπΉ))β©) | ||
Theorem | dvhfvsca 39449* | 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 39450 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β (π Γ πΈ))) β (π Β· πΉ) = β¨(π β(1st βπΉ)), (π β (2nd βπΉ))β©) | ||
Theorem | dvhopvsca 39451 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ π β πΈ)) β (π Β· β¨πΉ, πβ©) = β¨(π βπΉ), (π β π)β©) | ||
Theorem | dvhvscacl 39452 | 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 39453* | 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 39332. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (invrβπΉ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((πβπ) β πΈ β§ (πβπ) β π)) | ||
Theorem | tendolinv 39454* | 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 39455* | 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 39456 | 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 39457 | Lemma for dvhlvec 39458. 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 39458 | 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 39459 | 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 39460* | 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 39461 | 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 39465 and dihpN 39685. (Contributed by NM, 27-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΈ = β¨( I βΎ π΅), ( I βΎ π)β© & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΈ β (π β { 0 })) | ||
Theorem | dvhopclN 39462 | Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ ((πΉ β π β§ π β πΈ) β β¨πΉ, πβ© β (π Γ πΈ)) | ||
Theorem | dvhopaddN 39463* | Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ π΄ = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ)π(2nd βπ))β©) β β’ (((πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ©π΄β¨πΊ, πβ©) = β¨(πΉ β πΊ), (πππ)β©) | ||
Theorem | dvhopspN 39464* | Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ π = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ ((π β πΈ β§ (πΉ β π β§ π β πΈ)) β (π πβ¨πΉ, πβ©) = β¨(π βπΉ), (π β π)β©) | ||
Theorem | dvhopN 39465* | 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 39466* | Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (β¨πΉ, πβ© β (π β π) β βπ₯βπ¦βπ§βπ€((β¨π₯, π¦β© β π β§ β¨π§, π€β© β π) β§ β¨πΉ, πβ© = (β¨π₯, π¦β© + β¨π§, π€β©)))) | ||
Theorem | cdlemm10N 39467* | 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 39468 | Extend class notation with subspace orthocomplement for DVecA partial vector space. |
class ocA | ||
Definition | df-docaN 39469* | 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 39470* | 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 39471* | 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 39472* | 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 39473 | 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 39474 | 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 39475 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β ( β₯ β( β₯ β(πΌβπ))) = (πΌβπ)) | ||
Theorem | doca3N 39476 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | dvadiaN 39477 | 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 39478* | 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 πΌ = {π₯ β π β£ ( β₯ β( β₯ βπ₯)) = π₯}) | ||
Theorem | diaf1oN 39479* | The partial isomorphism A for a lattice πΎ is a one-to-one, onto function. Part of Lemma M of [Crawley] p. 121 line 12, with closed subspaces rather than subspaces. See diadm 39384 for the domain. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) & β’ π = (LSubSpβπ) β β’ ((πΎ β HL β§ π β π») β πΌ:dom πΌβ1-1-ontoβ{π₯ β π β£ ( β₯ β( β₯ βπ₯)) = π₯}) | ||
Syntax | cdjaN 39480 | Extend class notation with subspace join for DVecA partial vector space. |
class vA | ||
Definition | df-djaN 39481* | Define (closed) subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) |
β’ vA = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β π« ((LTrnβπ)βπ€), π¦ β π« ((LTrnβπ)βπ€) β¦ (((ocAβπ)βπ€)β((((ocAβπ)βπ€)βπ₯) β© (((ocAβπ)βπ€)βπ¦)))))) | ||
Theorem | djaffvalN 39482* | Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (vAβπΎ) = (π€ β π» β¦ (π₯ β π« ((LTrnβπΎ)βπ€), π¦ β π« ((LTrnβπΎ)βπ€) β¦ (((ocAβπΎ)βπ€)β((((ocAβπΎ)βπ€)βπ₯) β© (((ocAβπΎ)βπ€)βπ¦)))))) | ||
Theorem | djafvalN 39483* | Subspace join for DVecA partial vector space. TODO: take out hypothesis .i, no longer used. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) & β’ π½ = ((vAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π½ = (π₯ β π« π, π¦ β π« π β¦ ( β₯ β(( β₯ βπ₯) β© ( β₯ βπ¦))))) | ||
Theorem | djavalN 39484 | Subspace join for DVecA partial vector space. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) & β’ π½ = ((vAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β (ππ½π) = ( β₯ β(( β₯ βπ) β© ( β₯ βπ)))) | ||
Theorem | djaclN 39485 | Closure of subspace join for DVecA partial vector space. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π½ = ((vAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π β§ π β π)) β (ππ½π) β ran πΌ) | ||
Theorem | djajN 39486 | Transfer lattice join to DVecA partial vector space closed subspace join. Part of Lemma M of [Crawley] p. 120 line 29, with closed subspace join rather than subspace sum. (Contributed by NM, 5-Dec-2013.) (New usage is discouraged.) |
β’ β¨ = (joinβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π½ = ((vAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β dom πΌ)) β (πΌβ(π β¨ π)) = ((πΌβπ)π½(πΌβπ))) | ||
Syntax | cdib 39487 | Extend class notation with isomorphism B. |
class DIsoB | ||
Definition | df-dib 39488* | Isomorphism B is isomorphism A extended with an extra dimension set to the zero vector component i.e. the zero endormorphism. Its domain is lattice elements less than or equal to the fiducial co-atom π€. (Contributed by NM, 8-Dec-2013.) |
β’ DIsoB = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β dom ((DIsoAβπ)βπ€) β¦ ((((DIsoAβπ)βπ€)βπ₯) Γ {(π β ((LTrnβπ)βπ€) β¦ ( I βΎ (Baseβπ)))})))) | ||
Theorem | dibffval 39489* | The partial isomorphism B for a lattice πΎ. (Contributed by NM, 8-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoBβπΎ) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))) | ||
Theorem | dibfval 39490* | The partial isomorphism B for a lattice πΎ. (Contributed by NM, 8-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β dom π½ β¦ ((π½βπ₯) Γ { 0 }))) | ||
Theorem | dibval 39491* | The partial isomorphism B for a lattice πΎ. (Contributed by NM, 8-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β dom π½) β (πΌβπ) = ((π½βπ) Γ { 0 })) | ||
Theorem | dibopelvalN 39492* | Member of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) (Revised by Mario Carneiro, 6-May-2015.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β dom π½) β (β¨πΉ, πβ© β (πΌβπ) β (πΉ β (π½βπ) β§ π = 0 ))) | ||
Theorem | dibval2 39493* | Value of the partial isomorphism B. (Contributed by NM, 18-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = ((π½βπ) Γ { 0 })) | ||
Theorem | dibopelval2 39494* | Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) (Revised by Mario Carneiro, 6-May-2015.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (β¨πΉ, πβ© β (πΌβπ) β (πΉ β (π½βπ) β§ π = 0 ))) | ||
Theorem | dibval3N 39495* | Value of the partial isomorphism B for a lattice πΎ. (Contributed by NM, 24-Feb-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) = ({π β π β£ (π βπ) β€ π} Γ { 0 })) | ||
Theorem | dibelval3 39496* | Member of the partial isomorphism B. (Contributed by NM, 26-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (π β (πΌβπ) β βπ β π (π = β¨π, 0 β© β§ (π βπ) β€ π))) | ||
Theorem | dibopelval3 39497* | Member of the partial isomorphism B. (Contributed by NM, 3-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (β¨πΉ, πβ© β (πΌβπ) β ((πΉ β π β§ (π βπΉ) β€ π) β§ π = 0 ))) | ||
Theorem | dibelval1st 39498 | Membership in value of the partial isomorphism B for a lattice πΎ. (Contributed by NM, 13-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β (1st βπ) β (π½βπ)) | ||
Theorem | dibelval1st1 39499 | Membership in value of the partial isomorphism B for a lattice πΎ. (Contributed by NM, 13-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β (1st βπ) β π) | ||
Theorem | dibelval1st2N 39500 | Membership in value of the partial isomorphism B for a lattice πΎ. (Contributed by NM, 13-Feb-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ π β (πΌβπ)) β (π β(1st βπ)) β€ π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |