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-29658) |
Hilbert Space Explorer
(29659-31181) |
Users' Mathboxes
(31182-46997) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemk19x 39301* | cdlemk19 39227 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β¦πΉ / πβ¦πβπ) = (πβπ)) | ||
Theorem | cdlemk42yN 39302* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (β¦πΊ / πβ¦πβπ) = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π))))) | ||
Theorem | cdlemk11tc 39303* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. πΊ, πΌ stand for g, h. TODO: fix comment. (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπ) β (π βπΌ)))) β (β¦πΊ / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π β(πΌ β β‘πΊ)))) | ||
Theorem | cdlemk11t 39304* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 5, line 36, p. 119. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (β¦πΊ / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π β(πΌ β β‘πΊ)))) | ||
Theorem | cdlemk45 39305* | Part of proof of Lemma K of [Crawley] p. 118. Line 37, p. 119. πΊ, πΌ stand for g, h. π represents tau. They do not explicitly mention the requirement (πΊ β πΌ) β ( I βΎ π΅). (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ))) | ||
Theorem | cdlemk46 39306* | Part of proof of Lemma K of [Crawley] p. 118. Line 38 (last line), p. 119. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (πΊ β πΌ) β ( I βΎ π΅))) β (β¦(πΊ β πΌ) / πβ¦πβπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ))) | ||
Theorem | cdlemk47 39307* | Part of proof of Lemma K of [Crawley] p. 118. Line 2, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β (β¦(πΊ β πΌ) / πβ¦πβπ) = (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
Theorem | cdlemk48 39308* | Part of proof of Lemma K of [Crawley] p. 118. Line 4, p. 120. πΊ, πΌ stand for g, h. π represents tau. (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) | ||
Theorem | cdlemk49 39309* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, 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 | cdlemk50 39310* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 39312? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π)))) | ||
Theorem | cdlemk51 39311* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 39312? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
Theorem | cdlemk52 39312* | 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 39313* | Lemma for cdlemk53 39315. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk53b 39314* | Lemma for cdlemk53 39315. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk53 39315* | 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 39316* | 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 39317* | Lemma for cdlemk55 39319. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk55b 39318* | Lemma for cdlemk55 39319. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) = (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk55 39319* | 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 39320* | 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 39321* | 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 39322* | Substitution version of cdlemk35 39270. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΊ) β π) | ||
Theorem | cdlemk55u1 39323* | Lemma for cdlemk55u 39324. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (((π βπΉ) = (π βπ) β§ πΉ β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
Theorem | cdlemk55u 39324* | 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 39325* | Lemma for cdlemk39u 39326. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
Theorem | cdlemk39u 39326* | 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 39327* | cdlemk19 39227 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 39328* | 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 39329* | 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 39330* | Use a fixed element to eliminate π in cdlemk19u 39328. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (πβπΉ) = π) | ||
Theorem | cdlemk56w 39331* | Use a fixed element to eliminate π in cdlemk56 39329. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (π β πΈ β§ (πβπΉ) = π)) | ||
Theorem | cdlemk 39332* | 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 39333* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 39332. TODO: can this be used to shorten uses of cdlemk 39332? (Contributed by NM, 15-Oct-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπ) β€ (π βπΉ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
Theorem | cdleml1N 39334 | 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 39335* | 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 39336* | 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 39337* | 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 39338* | 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 39339* | 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 39340* | 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 39341* | 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 39342* | 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 39343* | 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 38921. πΈ is the division ring base by erngdv 39351, and π βπΉ is the scalar product by dvavsca 39375. πΉ 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 39344* | 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 39345 | Value of the endomorphism division ring unity. (Contributed by NM, 12-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ ((πΎ β HL β§ π β π») β π· β Ring) β β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) | ||
Theorem | erngdvlem1 39346* | Lemma for eringring 39350. (Contributed by NM, 4-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
Theorem | erngdvlem2N 39347* | Lemma for eringring 39350. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
Theorem | erngdvlem3 39348* | Lemma for eringring 39350. (Contributed by NM, 6-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdvlem4 39349* | Lemma for erngdv 39351. (Contributed by NM, 11-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((ocβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((ββπ) β¨ (π β(π β β‘(π ββ))))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π β(π ββ)) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if((π ββ) = β, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (β β π β§ β β ( I βΎ π΅))) β π· β DivRing) | ||
Theorem | eringring 39350 | An endomorphism ring is a ring. TODO: fix comment. (Contributed by NM, 4-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdv 39351 | An endomorphism ring is a division ring. TODO: fix comment. (Contributed by NM, 11-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β π· β DivRing) | ||
Theorem | erng0g 39352* | 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 39353 | 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 39354* | Lemma for eringring 39350. (Contributed by NM, 4-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
Theorem | erngdvlem2-rN 39355* | Lemma for eringring 39350. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
Theorem | erngdvlem3-rN 39356* | Lemma for eringring 39350. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ π = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) | ||
Theorem | erngdvlem4-rN 39357* | Lemma for erngdv 39351. (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 39358 | 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 39359 | 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 39360 | Extend class notation with constructed vector space A. |
class DVecA | ||
Definition | df-dveca 39361* | 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 39362* | 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 39363* | 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 39364 | 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 39365 | 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 39366* | 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 39367* | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((π βπ) β (πβπ)))) | ||
Theorem | dvaplusgv 39368 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ + = (+gβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΊ β π)) β ((π + π)βπΊ) = ((π βπΊ) β (πβπΊ))) | ||
Theorem | dvafmulr 39369* | 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 39370 | Ring multiplication operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ πΉ = (Scalarβπ) & β’ Β· = (.rβπΉ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | dvavbase 39371 | 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 39372* | 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 39373 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ + = (+gβπ) β β’ (((πΎ β π β§ π β π») β§ (πΉ β π β§ πΊ β π)) β (πΉ + πΊ) = (πΉ β πΊ)) | ||
Theorem | dvafvsca 39374* | 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 39375 | Ring addition operation for the constructed partial vector space A. (Contributed by NM, 11-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((DVecAβπΎ)βπ) & β’ Β· = ( Β·π βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π)) β (π Β· πΉ) = (π βπΉ)) | ||
Theorem | tendospcl 39376 | Closure of endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ π β πΈ β§ πΉ β π) β (πβπΉ) β π) | ||
Theorem | tendospass 39377 | Associative law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π β π)βπΉ) = (πβ(πβπΉ))) | ||
Theorem | tendospdi1 39378 | Forward distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π)) β (πβ(πΉ β πΊ)) = ((πβπΉ) β (πβπΊ))) | ||
Theorem | tendocnv 39379 | Converse of a trace-preserving endomorphism value. (Contributed by NM, 7-Apr-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ πΉ β π) β β‘(πβπΉ) = (πββ‘πΉ)) | ||
Theorem | tendospdi2 39380* | Reverse distributive law for endomorphism scalar product operation. (Contributed by NM, 10-Oct-2013.) |
β’ π = ((LTrnβπΎ)βπ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ ((π β πΈ β§ π β πΈ β§ πΉ β π) β ((πππ)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | tendospcanN 39381* | 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 39382 | 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 39383 | Lemma for dvalvec 39384. (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 39384 | 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 39385 | 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 39386 | Extend class notation with partial isomorphism A. |
class DIsoA | ||
Definition | df-disoa 39387* | Define partial isomorphism A. (Contributed by NM, 15-Oct-2013.) |
β’ DIsoA = (π β V β¦ (π€ β (LHypβπ) β¦ (π₯ β {π¦ β (Baseβπ) β£ π¦(leβπ)π€} β¦ {π β ((LTrnβπ)βπ€) β£ (((trLβπ)βπ€)βπ)(leβπ)π₯}))) | ||
Theorem | diaffval 39388* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) β β’ (πΎ β π β (DIsoAβπΎ) = (π€ β π» β¦ (π₯ β {π¦ β π΅ β£ π¦ β€ π€} β¦ {π β ((LTrnβπΎ)βπ€) β£ (((trLβπΎ)βπ€)βπ) β€ π₯}))) | ||
Theorem | diafval 39389* | The partial isomorphism A for a lattice πΎ. (Contributed by NM, 15-Oct-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ = (π₯ β {π¦ β π΅ β£ π¦ β€ π} β¦ {π β π β£ (π βπ) β€ π₯})) | ||
Theorem | diaval 39390* | 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 39391 | Member of the partial isomorphism A for a lattice πΎ. (Contributed by NM, 3-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΉ β (πΌβπ) β (πΉ β π β§ (π βπΉ) β€ π))) | ||
Theorem | diafn 39392* | Functionality and domain of the partial isomorphism A. (Contributed by NM, 26-Nov-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β πΌ Fn {π₯ β π΅ β£ π₯ β€ π}) | ||
Theorem | diadm 39393* | Domain of the partial isomorphism A. (Contributed by NM, 3-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β dom πΌ = {π₯ β π΅ β£ π₯ β€ π}) | ||
Theorem | diaeldm 39394 | Member of domain of the partial isomorphism A. (Contributed by NM, 4-Dec-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β (π β dom πΌ β (π β π΅ β§ π β€ π))) | ||
Theorem | diadmclN 39395 | 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 39396 | 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 39397 | The value of the partial isomorphism A is not empty. (Contributed by NM, 17-Jan-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ πΌ = ((DIsoAβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β β ) | ||
Theorem | dia0eldmN 39398 | 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 39399 | 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 39400 | 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βπΎ)βπ) β β’ (((πΎ β π β§ π β π») β§ (π β π΅ β§ π β€ π)) β (πΌβπ) β π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |