Home | Metamath
Proof Explorer Theorem List (p. 394 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 | cdlemk50 39301* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 39303? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π)))) | ||
Theorem | cdlemk51 39302* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 39303? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
Theorem | cdlemk52 39303* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) = (β¦(πΊ β πΌ) / πβ¦πβπ)) | ||
Theorem | cdlemk53a 39304* | Lemma for cdlemk53 39306. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk53b 39305* | Lemma for cdlemk53 39306. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk53 39306* | Part of proof of Lemma K of [Crawley] p. 118. Line 7, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk54 39307* | Part of proof of Lemma K of [Crawley] p. 118. Line 10, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β (β¦(πΊ β πΌ) / πβ¦π β β¦π / πβ¦π) = ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π) β β¦π / πβ¦π)) | ||
Theorem | cdlemk55a 39308* | Lemma for cdlemk55 39310. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk55b 39309* | Lemma for cdlemk55 39310. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) = (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk55 39310* | Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemkyyN 39311* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up (πππΊ) stuff. (Contributed by NM, 21-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (β¦πΊ / πβ¦πβπ) = ((πππΊ)βπ)) | ||
Theorem | cdlemk43N 39312* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 31-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ π β π β§ πΉ β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β ((πβπΊ)βπ) = β¦πΊ / πβ¦π) | ||
Theorem | cdlemk35u 39313* | Substitution version of cdlemk35 39261. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΊ) β π) | ||
Theorem | cdlemk55u1 39314* | Lemma for cdlemk55u 39315. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (((π βπΉ) = (π βπ) β§ πΉ β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
Theorem | cdlemk55u 39315* | Part of proof of Lemma K of [Crawley] p. 118. Line 11, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
Theorem | cdlemk39u1 39316* | Lemma for cdlemk39u 39317. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
Theorem | cdlemk39u 39317* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of the value of tau, represented by (πβπΊ). (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
Theorem | cdlemk19u1 39318* | cdlemk19 39218 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΉ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΉ)βπ) = (πβπ)) | ||
Theorem | cdlemk19u 39319* | Part of Lemma K of [Crawley] p. 118. Line 12, p. 120, "f (exponent) tau = k". We represent f, k, tau with πΉ, π, π. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΉ) = π) | ||
Theorem | cdlemk56 39320* | Part of Lemma K of [Crawley] p. 118. Line 11, p. 120, "tau is in Delta" i.e. π is a trace-preserving endormorphism. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ) β§ (π β π΄ β§ Β¬ π β€ π)) β π β πΈ) | ||
Theorem | cdlemk19w 39321* | Use a fixed element to eliminate π in cdlemk19u 39319. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (πβπΉ) = π) | ||
Theorem | cdlemk56w 39322* | Use a fixed element to eliminate π in cdlemk56 39320. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (π β πΈ β§ (πβπΉ) = π)) | ||
Theorem | cdlemk 39323* | Lemma K of [Crawley] p. 118. Final result, lines 11 and 12 on p. 120: given two translations f and k with the same trace, there exists a trace-preserving endomorphism tau whose value at f is k. We use πΉ, π, and π’ to represent f, k, and tau. (Contributed by NM, 1-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
Theorem | tendoex 39324* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 39323. TODO: can this be used to shorten uses of cdlemk 39323? (Contributed by NM, 15-Oct-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπ) β€ (π βπΉ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
Theorem | cdleml1N 39325 | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β (π β(πβπ)) = (π β(πβπ))) | ||
Theorem | cdleml2N 39326* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅) β§ (πβπ) β ( I βΎ π΅))) β βπ β πΈ (π β(πβπ)) = (πβπ)) | ||
Theorem | cdleml3N 39327* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ π β π) β§ (π β ( I βΎ π΅) β§ π β 0 β§ π β 0 )) β βπ β πΈ (π β π) = π) | ||
Theorem | cdleml4N 39328* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ (π β 0 β§ π β 0 )) β βπ β πΈ (π β π) = π) | ||
Theorem | cdleml5N 39329* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 1-Aug-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ) β§ π β 0 ) β βπ β πΈ (π β π) = π) | ||
Theorem | cdleml6 39330* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β (π β πΈ β§ (πβ(π ββ)) = β)) | ||
Theorem | cdleml7 39331* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ β β π β§ (π β πΈ β§ π β 0 )) β ((π β π )ββ) = (( I βΎ π)ββ)) | ||
Theorem | cdleml8 39332* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β (π β π ) = ( I βΎ π)) | ||
Theorem | cdleml9 39333* | Part of proof of Lemma L of [Crawley] p. 120. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅)) β§ (π β πΈ β§ π β 0 )) β π β 0 ) | ||
Theorem | dva1dim 39334* | Two expressions for the 1-dimensional subspaces of partial vector space A. Remark in [Crawley] p. 120 line 21, but using a non-identity translation (nonzero vector) πΉ whose trace is π rather than π itself; πΉ exists by cdlemf 38912. πΈ is the division ring base by erngdv 39342, and π βπΉ is the scalar product by dvavsca 39366. πΉ must be a non-identity translation for the expression to be a 1-dimensional subspace, although the theorem doesn't require it. (Contributed by NM, 14-Oct-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β£ βπ β πΈ π = (π βπΉ)} = {π β π β£ (π βπ) β€ (π βπΉ)}) | ||
Theorem | dvhb1dimN 39335* | Two expressions for the 1-dimensional subspaces of vector space H, in the isomorphism B case where the 2nd vector component is zero. (Contributed by NM, 23-Feb-2014.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ 0 = (β β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π) β {π β (π Γ πΈ) β£ βπ β πΈ π = β¨(π βπΉ), 0 β©} = {π β (π Γ πΈ) β£ ((π β(1st βπ)) β€ (π βπΉ) β§ (2nd βπ) = 0 )}) | ||
Theorem | erng1lem 39336 | Value of the endomorphism division ring unity. (Contributed by NM, 12-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ ((πΎ β HL β§ π β π») β π· β Ring) β β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) | ||
Theorem | erngdvlem1 39337* | Lemma for eringring 39341. (Contributed by NM, 4-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
Theorem | erngdvlem2N 39338* | Lemma for eringring 39341. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
Theorem | erngdvlem3 39339* | Lemma for eringring 39341. (Contributed by NM, 6-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdvlem4 39340* | Lemma for erngdv 39342. (Contributed by NM, 11-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) | ||
Theorem | eringring 39341 | An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdv 39342 | An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β DivRing) | ||
Theorem | erng0g 39343* | The division ring zero of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ 0 = (0gβπ·) β β’ ((πΎ β HL β§ π β π») β 0 = π) | ||
Theorem | erng1r 39344 | The division ring unity of an endomorphism ring. (Contributed by NM, 5-Nov-2013.) (Revised by Mario Carneiro, 23-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ 1 = (1rβπ·) β β’ ((πΎ β HL β§ π β π») β 1 = ( I βΎ π)) | ||
Theorem | erngdvlem1-rN 39345* | Lemma for eringring 39341. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
Theorem | erngdvlem2-rN 39346* | Lemma for eringring 39341. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
Theorem | erngdvlem3-rN 39347* | Lemma for eringring 39341. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ π = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdvlem4-rN 39348* | Lemma for erngdv 39342. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ π = (π β πΈ, π β πΈ β¦ (π β π)) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) | ||
Theorem | erngring-rN 39349 | An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdv-rN 39350 | An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β DivRing) | ||
Syntax | cdveca 39351 | Extend class notation with constructed vector space A. |
class DVecA | ||
Definition | df-dveca 39352* | Define constructed partial vector space A. (Contributed by NM, 8-Oct-2013.) |
β’ DVecA = (π β V β¦ (π€ β (LHypβπ) β¦ ({β¨(Baseβndx), ((LTrnβπ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx), ((EDRingβπ)βπ€)β©} βͺ {β¨( Β·π βndx), (π β ((TEndoβπ)βπ€), π β ((LTrnβπ)βπ€) β¦ (π βπ))β©}))) | ||
Theorem | dvafset 39353* | The constructed partial vector space A for a lattice πΎ. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DVecAβπΎ) = (π€ β π» β¦ ({β¨(Baseβndx), ((LTrnβπΎ)βπ€)β©, β¨(+gβndx), (π β ((LTrnβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π β π))β©, β¨(Scalarβndx), ((EDRingβπΎ)βπ€)β©} βͺ {β¨( Β·π βndx), (π β ((TEndoβπΎ)βπ€), π β ((LTrnβπΎ)βπ€) β¦ (π βπ))β©}))) | ||
Theorem | dvaset 39354* | The constructed partial vector space A for a lattice πΎ. (Contributed by NM, 8-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π = ({β¨(Baseβndx), πβ©, β¨(+gβndx), (π β π, π β π β¦ (π β π))β©, β¨(Scalarβndx), π·β©} βͺ {β¨( Β·π βndx), (π β πΈ, π β π β¦ (π βπ))β©})) | ||
Theorem | dvasca 39355 | The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom π). (Contributed by NM, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) β β’ ((πΎ β π β§ π β π») β πΉ = π·) | ||
Theorem | dvabase 39356 | The ring base set of the constructed partial vector space A are all translation group endomorphisms (for a fiducial co-atom π). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ πΆ = (BaseβπΉ) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
Theorem | dvafplusg 39357* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | dvaplusg 39358* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((π βπ) β (πβπ)))) | ||
Theorem | dvaplusgv 39359 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΊ β π)) β ((π + π)βπΊ) = ((π βπΊ) β (πβπΊ))) | ||
Theorem | dvafmulr 39360* | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
Theorem | dvamulr 39361 | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | dvavbase 39362 | The vectors (vector base set) of the constructed partial vector space A are all translations (for a fiducial co-atom π). (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = (Baseβπ) β β’ ((πΎ β π β§ π β π») β π = π) | ||
Theorem | dvafvadd 39363* | The vector sum operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ + = (+gβπ) β β’ ((πΎ β π β§ π β π») β + = (π β π, π β π β¦ (π β π))) | ||
Theorem | dvavadd 39364 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ + = (+gβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ πΊ β π)) β (πΉ + πΊ) = (πΉ β πΊ)) | ||
Theorem | dvafvsca 39365* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 9-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π β π β¦ (π βπ))) | ||
Theorem | dvavsca 39366 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π)) β (π Β· πΉ) = (π βπΉ)) | ||
Theorem | tendospcl 39367 | Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) | ||
Theorem | tendospass 39368 | Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π β π)βπΉ) = (πβ(πβπΉ))) | ||
Theorem | tendospdi1 39369 | Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendocnv 39370 | Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ) = (πββ‘πΉ)) | ||
Theorem | tendospdi2 39371* | Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π = ((LTrnβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | tendospcanN 39372* | Cancellation law for trace-preserving endomorphism values (used as scalar product). (Contributed by NM, 7-Apr-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (πΉ β π β§ πΊ β π)) β ((πβπΉ) = (πβπΊ) β πΉ = πΊ)) | ||
Theorem | dvaabl 39373 | The constructed partial vector space A for a lattice πΎ is an abelian group. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π β Abel) | ||
Theorem | dvalveclem 39374 | Lemma for dvalvec 39375. (Contributed by NM, 11-Oct-2013.) (Proof shortened by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) & β’ π = ((LTrnβπΎ)βπ) & β’ + = (+gβπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = (Scalarβπ) & β’ π΅ = (BaseβπΎ) & ⒠⨣ = (+gβπ·) & β’ Γ = (.rβπ·) & β’ Β· = ( Β·π βπ) β β’ ((πΎ β HL β§ π β π») β π β LVec) | ||
Theorem | dvalvec 39375 | The constructed partial vector space A for a lattice πΎ is a left vector space. (Contributed by NM, 11-Oct-2013.) (Revised by Mario Carneiro, 22-Jun-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((DVecAβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π β LVec) | ||
Theorem | dva0g 39376 | The zero vector of partial vector space A. (Contributed by NM, 9-Sep-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ 0 = (0gβπ) β β’ ((πΎ β HL β§ π β π») β 0 = ( I βΎ π΅)) | ||
Syntax | cdia 39377 | Extend class notation with partial isomorphism A. |
class DIsoA | ||
Definition | df-disoa 39378* | Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.) |
β’ DIsoA = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} β¦ {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯}))) | ||
Theorem | diaffval 39379* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) | ||
Theorem | diafval 39380* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π βπ) β€ π₯})) | ||
Theorem | diaval 39381* | 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 39382 | Member of the partial isomorphism A for a lattice πΎ. (Contributed by NM, 3-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΉ β (πΌβπ) β (πΉ β π β§ (π βπΉ) β€ π))) | ||
Theorem | diafn 39383* | Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ Fn {π₯ β π΅ β£ π₯ β€ π}) | ||
Theorem | diadm 39384* | Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β dom πΌ = {π₯ β π΅ β£ π₯ β€ π}) | ||
Theorem | diaeldm 39385 | Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β (π β dom πΌ β (π β π΅ β§ π β€ π))) | ||
Theorem | diadmclN 39386 | 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 39387 | 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 39388 | The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β β ) | ||
Theorem | dia0eldmN 39389 | 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 39390 | 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 39391 | 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 39392 | 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 39393 | Trace of a member of the partial isomorphism A. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π) β§ πΉ β (πΌβπ)) β (π βπΉ) β€ π) | ||
Theorem | diaelrnN 39394 | 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 39395 | 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 39396 | 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 39397 | 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 39398 | 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 39399 | 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 39400 | Closure of partial isomorphism A converse. (Contributed by NM, 6-Dec-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β ran πΌ) β (β‘πΌβπ) β dom πΌ) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |