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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | diael 39401 | 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 39402 | Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ πΉ β (πΌβπ)) β (π βπΉ) β€ π) | ||
Theorem | diaelrnN 39403 | 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 39404 | 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 39405 | 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 39406 | 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 39407 | 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 39408 | 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 39409 | Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β dom πΌ) | ||
Theorem | dia0 39410 | 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 39411 | 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 39412 | 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 39413* | Partial isomorphism A of a lattice glb. (Contributed by NM, 3-Dec-2013.) (New usage is discouraged.) |
β’ πΊ = (glbβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β dom πΌ β§ π β β )) β (πΌβ(πΊβπ)) = β© π₯ β π (πΌβπ₯)) | ||
Theorem | diameetN 39414 | 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 39415 | 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 39416 | 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 39417 | 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 39418 | 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 39419* | 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 39420 | 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 39421 | A vector (translation) belongs to the 1-dim subspace it generates. (Contributed by NM, 8-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β πΉ β (πΌβ(π βπΉ))) | ||
Theorem | dia2dimlem1 39422 | Lemma for dia2dim 39435. 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 39423 | Lemma for dia2dim 39435. 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 39424 | Lemma for dia2dim 39435. 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 39425 | Lemma for dia2dim 39435. 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 39426 | Lemma for dia2dim 39435. 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 39427 | Lemma for dia2dim 39435. 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 39428 | Lemma for dia2dim 39435. Eliminate (πΉβπ) β π condition. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ Β¬ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) & β’ (π β (π βπΉ) β π) & β’ (π β (π βπΉ) β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem8 39429 | Lemma for dia2dim 39435. 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 39430 | Lemma for dia2dim 39435. Eliminate (π βπΉ) β π, π conditions. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β πΉ β π) & β’ (π β (π βπΉ) β€ (π β¨ π)) & β’ (π β π β π) β β’ (π β πΉ β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem10 39431 | Lemma for dia2dim 39435. 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 39432 | Lemma for dia2dim 39435. 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 39433 | Lemma for dia2dim 39435. Obtain subset relation. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β π β π) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dimlem13 39434 | Lemma for dia2dim 39435. Eliminate π β π condition. (Contributed by NM, 8-Sep-2014.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) & β’ π = (LSpanβπ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ (π β (πΎ β HL β§ π β π»)) & β’ (π β (π β π΄ β§ π β€ π)) & β’ (π β (π β π΄ β§ π β€ π)) β β’ (π β (πΌβ(π β¨ π)) β ((πΌβπ) β (πΌβπ))) | ||
Theorem | dia2dim 39435 | 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 39436 | Extend class notation with constructed full vector space H. |
class DVecH | ||
Definition | df-dvech 39437* | 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 39438* | 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 39439* | 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 39440 | The ring of scalars of the constructed full vector space H. (Contributed by NM, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) β β’ ((πΎ β π β§ π β π») β πΉ = π·) | ||
Theorem | dvhbase 39441 | 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 39442* | 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 39443* | 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 39444 | 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 39445 | 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 39446 | Vector membership in the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ π β πΈ)) β β¨πΉ, πβ© β π) | ||
Theorem | dvhvaddcbv 39447* | Change bound variables to isolate them later. (Contributed by NM, 3-Nov-2013.) |
β’ + = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ) ⨣ (2nd βπ))β©) β β’ + = (β β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st ββ) β (1st βπ)), ((2nd ββ) ⨣ (2nd βπ))β©) | ||
Theorem | dvhvaddval 39448* | 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 39449* | 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 39450 | 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 39451 | 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 39452* | The vector sum operation for the constructed full vector space H. TODO: check if this will shorten proofs that use dvhopvadd 39451 and/or dvhfplusr 39442. (Contributed by NM, 26-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = ((DVecHβπΎ)βπ) & β’ β = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ© β β¨πΊ, π β©) = β¨(πΉ β πΊ), (π + π )β©) | ||
Theorem | dvhvaddcl 39453 | 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 39454 | 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 39455 | Associativity of vector sum. (Contributed by NM, 31-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π· = (Scalarβπ) & ⒠⨣ = (+gβπ·) & β’ + = (+gβπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β (π Γ πΈ) β§ πΊ β (π Γ πΈ) β§ πΌ β (π Γ πΈ))) β ((πΉ + πΊ) + πΌ) = (πΉ + (πΊ + πΌ))) | ||
Theorem | dvhvscacbv 39456* | Change bound variables to isolate them later. (Contributed by NM, 20-Nov-2013.) |
β’ Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ Β· = (π‘ β πΈ, π β (π Γ πΈ) β¦ β¨(π‘β(1st βπ)), (π‘ β (2nd βπ))β©) | ||
Theorem | dvhvscaval 39457* | The scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Nov-2013.) |
β’ Β· = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ ((π β πΈ β§ πΉ β (π Γ πΈ)) β (π Β· πΉ) = β¨(πβ(1st βπΉ)), (π β (2nd βπΉ))β©) | ||
Theorem | dvhfvsca 39458* | 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 39459 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 2-Nov-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β (π Γ πΈ))) β (π Β· πΉ) = β¨(π β(1st βπΉ)), (π β (2nd βπΉ))β©) | ||
Theorem | dvhopvsca 39460 | Scalar product operation for the constructed full vector space H. (Contributed by NM, 20-Feb-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ π β πΈ)) β (π Β· β¨πΉ, πβ©) = β¨(π βπΉ), (π β π)β©) | ||
Theorem | dvhvscacl 39461 | 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 39462* | 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 39341. (Contributed by NM, 10-Apr-2014.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (β β π β¦ ( I βΎ π΅)) & β’ π = ((DVecHβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ π = (invrβπΉ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ π β π) β ((πβπ) β πΈ β§ (πβπ) β π)) | ||
Theorem | tendolinv 39463* | 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 39464* | 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 39465 | 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 39466 | Lemma for dvhlvec 39467. 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 39467 | 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 39468 | 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 39469* | 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 39470 | 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 39474 and dihpN 39694. (Contributed by NM, 27-Mar-2015.) |
β’ π» = (LHypβπΎ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecHβπΎ)βπ) & β’ π = (Baseβπ) & β’ 0 = (0gβπ) & β’ πΈ = β¨( I βΎ π΅), ( I βΎ π)β© & β’ (π β (πΎ β HL β§ π β π»)) β β’ (π β πΈ β (π β { 0 })) | ||
Theorem | dvhopclN 39471 | Closure of a DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ ((πΉ β π β§ π β πΈ) β β¨πΉ, πβ© β (π Γ πΈ)) | ||
Theorem | dvhopaddN 39472* | Sum of DVecH vectors expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ π΄ = (π β (π Γ πΈ), π β (π Γ πΈ) β¦ β¨((1st βπ) β (1st βπ)), ((2nd βπ)π(2nd βπ))β©) β β’ (((πΉ β π β§ π β πΈ) β§ (πΊ β π β§ π β πΈ)) β (β¨πΉ, πβ©π΄β¨πΊ, πβ©) = β¨(πΉ β πΊ), (πππ)β©) | ||
Theorem | dvhopspN 39473* | Scalar product of DVecH vector expressed as ordered pair. (Contributed by NM, 20-Nov-2013.) (New usage is discouraged.) |
β’ π = (π β πΈ, π β (π Γ πΈ) β¦ β¨(π β(1st βπ)), (π β (2nd βπ))β©) β β’ ((π β πΈ β§ (πΉ β π β§ π β πΈ)) β (π πβ¨πΉ, πβ©) = β¨(π βπΉ), (π β π)β©) | ||
Theorem | dvhopN 39474* | 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 39475* | Ordered pair membership in a subspace sum. (Contributed by NM, 12-Mar-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecHβπΎ)βπ) & β’ + = (+gβπ) & β’ π = (LSubSpβπ) & β’ β = (LSSumβπ) β β’ (((πΎ β HL β§ π β π») β§ π β π β§ π β π) β (β¨πΉ, πβ© β (π β π) β βπ₯βπ¦βπ§βπ€((β¨π₯, π¦β© β π β§ β¨π§, π€β© β π) β§ β¨πΉ, πβ© = (β¨π₯, π¦β© + β¨π§, π€β©)))) | ||
Theorem | cdlemm10N 39476* | 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 39477 | Extend class notation with subspace orthocomplement for DVecA partial vector space. |
class ocA | ||
Definition | df-docaN 39478* | 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 39479* | 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 39480* | 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 39481* | 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 39482 | 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 39483 | 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 39484 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β dom πΌ) β ( β₯ β( β₯ β(πΌβπ))) = (πΌβπ)) | ||
Theorem | doca3N 39485 | Double orthocomplement of partial isomorphism A. (Contributed by NM, 17-Jan-2014.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) & β’ β₯ = ((ocAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β ( β₯ β( β₯ βπ)) = π) | ||
Theorem | dvadiaN 39486 | 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 39487* | 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 39488* | 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 39393 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 39489 | Extend class notation with subspace join for DVecA partial vector space. |
class vA | ||
Definition | df-djaN 39490* | 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 39491* | 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 39492* | 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 39493 | 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 39494 | 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 39495 | 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 39496 | Extend class notation with isomorphism B. |
class DIsoB | ||
Definition | df-dib 39497* | 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 39498* | The partial isomorphism B for a lattice πΎ. (Contributed by NM, 8-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoBβπΎ) = (π€ β π» β¦ (π₯ β dom ((DIsoAβπΎ)βπ€) β¦ ((((DIsoAβπΎ)βπ€)βπ₯) Γ {(π β ((LTrnβπΎ)βπ€) β¦ ( I βΎ π΅))})))) | ||
Theorem | dibfval 39499* | The partial isomorphism B for a lattice πΎ. (Contributed by NM, 8-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β dom π½ β¦ ((π½βπ₯) Γ { 0 }))) | ||
Theorem | dibval 39500* | The partial isomorphism B for a lattice πΎ. (Contributed by NM, 8-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ π½ = ((DIsoAβπΎ)βπ) & β’ πΌ = ((DIsoBβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β dom π½) β (πΌβπ) = ((π½βπ) Γ { 0 })) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |