![]() |
Metamath
Proof Explorer Theorem List (p. 404 of 482) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | ![]() (1-30715) |
![]() (30716-32238) |
![]() (32239-48161) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemk21-2N 40301* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=2. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΆ β π β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΊ) β (π βπΆ)) β§ ((π βπΊ) β (π βπΉ) β§ πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((πβπΊ)βπ)) | ||
Theorem | cdlemk20-2N 40302* | Part of proof of Lemma K of [Crawley] p. 118. Line 22, p. 119 for the i=2, j=1 case. Note typo on line 22: f should be fi. Our π·, πΆ, π, π, π, π represent their f1, f2, k1, k2, sigma1, sigma2. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) & β’ π = (πβπ·) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΆ β π β§ π β π) β§ (π· β π β§ π· β ( I βΎ π΅)) β§ (πΆ β π β§ πΆ β ( I βΎ π΅))) β§ (((π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΆ)) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ·)βπ) = (πβπ)) | ||
Theorem | cdlemk22 40303* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 5-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ πΆ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (πΆ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπΆ) β (π βπ·)))) β ((πβπΊ)βπ) = ((πβπΊ)βπ)) | ||
Theorem | cdlemk30 40304* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π β§ π β π) β§ ((π βπ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ)βπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ))))) | ||
Theorem | cdlemkuu 40305* | Convert between function and operation forms of π. TODO: Use operation form everywhere. (Contributed by NM, 6-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((π· β π β§ πΊ β π) β (π·ππΊ) = (πβπΊ)) | ||
Theorem | cdlemk31 40306* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ π β π β§ π β π) β§ πΊ β π) β§ (((π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πππΊ)βπ) = ((π β¨ (π βπΊ)) β§ (((πβπ)βπ) β¨ (π β(πΊ β β‘π))))) | ||
Theorem | cdlemk32 40307* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 17-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ π β π β§ π β π) β§ πΊ β π) β§ (((π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ π β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πππΊ)βπ) = ((π β¨ (π βπΊ)) β§ (((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) β¨ (π β(πΊ β β‘π))))) | ||
Theorem | cdlemkuel-3 40308* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 40273? (Contributed by NM, 11-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (π·ππΊ) β π) | ||
Theorem | cdlemkuv2-3N 40309* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma2 (p) is π, f1 is π·, and k1 is π. (Contributed by NM, 6-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((π·ππΊ)βπ) = ((π β¨ (π βπΊ)) β§ (((πβπ·)βπ) β¨ (π β(πΊ β β‘π·))))) | ||
Theorem | cdlemk18-3N 40310* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, π· are k, sigma2 (p), k1, f1. (Contributed by NM, 7-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π· β π β§ π β π) β§ ((π βπ·) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((π·ππΉ)βπ) = (πβπ)) | ||
Theorem | cdlemk22-3 40311* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=1 and j=2. (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ πΆ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (πΆ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπΆ) β (π βπ·)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk23-3 40312* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the (π βπΆ) β (π βπ·) requirement from cdlemk22-3 40311. (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π β§ π₯ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅) β§ π₯ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ ((π βπΊ) β (π βπ·) β§ (π βπ₯) β (π βπΆ)) β§ ((π βπ₯) β (π βπ·) β§ (π βπ₯) β (π βπΉ) β§ (π βπΊ) β (π βπ₯)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk24-3 40313* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the (π βπ₯) β (π βπΆ) requirement from cdlemk23-3 40312 using (π βπΆ) = (π βπ·). (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π β§ π₯ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅) β§ π₯ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ ((π βπΊ) β (π βπ·) β§ (π βπΆ) = (π βπ·)) β§ ((π βπ₯) β (π βπ·) β§ (π βπ₯) β (π βπΉ) β§ (π βπΊ) β (π βπ₯)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk25-3 40314* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the (π βπΆ) = (π βπ·) requirement from cdlemk24-3 40313. (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π β§ π₯ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅) β§ π₯ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ (π βπΊ) β (π βπ·) β§ ((π βπ₯) β (π βπ·) β§ (π βπ₯) β (π βπΉ) β§ (π βπΊ) β (π βπ₯)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk26b-3 40315* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) = (π βπ))) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ₯ β π ((π₯ β ( I βΎ π΅) β§ (π βπ₯) β (π βπΉ) β§ (π βπ₯) β (π βπΊ)) β§ (π₯ππΊ) β π)) | ||
Theorem | cdlemk26-3 40316* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the π₯ requirements from cdlemk25-3 40314. (Contributed by NM, 10-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ (π βπΊ) β (π βπ·))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk27-3 40317* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the π from the conclusion of cdlemk25-3 40314. (Contributed by NM, 10-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ (π βπΊ) β (π βπ·))) β (π·ππΊ) = (πΆππΊ)) | ||
Theorem | cdlemk28-3 40318* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 14-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β βπ§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = (πππΊ))) | ||
Theorem | cdlemk33N 40319* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. TODO: not needed, is embodied in cdlemk34 40320. (Contributed by NM, 18-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = (πππΊ))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = ((πππΊ)βπ)))) | ||
Theorem | cdlemk34 40320* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. Part of attempt to simplify hypotheses. (Contributed by NM, 18-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = (πππΊ))) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = ((π β¨ (π βπΊ)) β§ (((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) β¨ (π β(πΊ β β‘π))))))) | ||
Theorem | cdlemk29-3 40321* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 14-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = (πππΊ))) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β π β π) | ||
Theorem | cdlemk35 40322* | Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 40321 with shorter hypotheses. (Contributed by NM, 18-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β π β π) | ||
Theorem | cdlemk36 40323* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (πβπ) = π) | ||
Theorem | cdlemk37 40324* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 18-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (πβπ) β€ (π β¨ (π βπΊ))) | ||
Theorem | cdlemk38 40325* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 3248? (Contributed by NM, 19-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (πβπ) β€ (π β¨ (π βπΊ))) | ||
Theorem | cdlemk39 40326* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. Trace-preserving property of tau, represented by π. (Contributed by NM, 19-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π βπ) β€ (π βπΊ)) | ||
Theorem | cdlemk40 40327* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
β’ π = (β©π§ β π π) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (πΊ β π β (πβπΊ) = if(πΉ = π, πΊ, β¦πΊ / πβ¦π)) | ||
Theorem | cdlemk40t 40328* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
β’ π = (β©π§ β π π) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((πΉ = π β§ πΊ β π) β (πβπΊ) = πΊ) | ||
Theorem | cdlemk40f 40329* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
β’ π = (β©π§ β π π) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((πΉ β π β§ πΊ β π) β (πβπΊ) = β¦πΊ / πβ¦π) | ||
Theorem | cdlemk41 40330* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.) |
β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ (πΊ β π β β¦πΊ / πβ¦π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π))))) | ||
Theorem | cdlemkfid1N 40331 | Lemma for cdlemkfid3N 40335. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ πΊ β π) β§ ((π βπΊ) β (π βπΉ) β§ (π β π΄ β§ Β¬ π β€ π))) β ((π β¨ (π βπΊ)) β§ ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) = (πΊβπ)) | ||
Theorem | cdlemkid1 40332 | Lemma for cdlemkid 40346. (Contributed by NM, 24-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β¨ (π βπ)) = (π β¨ (π βπ))) | ||
Theorem | cdlemkfid2N 40333 | Lemma for cdlemkfid3N 40335. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ = π) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ ((π βπ) β (π βπΉ) β§ (π β π΄ β§ Β¬ π β€ π))) β π = (πβπ)) | ||
Theorem | cdlemkid2 40334* | Lemma for cdlemkid 40346. (Contributed by NM, 24-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅) β§ (π β π β§ π β ( I βΎ π΅)))) β β¦πΊ / πβ¦π = π) | ||
Theorem | cdlemkfid3N 40335* | TODO: is this useful or should it be deleted? (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ = π) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ (π β π β§ π β ( I βΎ π΅))) β§ ((π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ) β§ (π β π΄ β§ Β¬ π β€ π))) β β¦πΊ / πβ¦π = (πΊβπ)) | ||
Theorem | cdlemky 40336* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up (πππΊ) stuff. π represents π in cdlemk31 40306. (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πππΊ)βπ)) | ||
Theorem | cdlemkyu 40337* | Convert between function and explicit forms. πΆ represents π in cdlemkuu 40305. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) & β’ π = (πβπ) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πΆβπΊ)βπ)) | ||
Theorem | cdlemkyuu 40338* | cdlemkyu 40337 with some hypotheses eliminated. TODO: Clean all this up. (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πΆβπΊ)βπ)) | ||
Theorem | cdlemk11ta 40339* | 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βπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπ) β (π βπΌ)))) β β¦πΊ / πβ¦π β€ (β¦πΌ / πβ¦π β¨ (π β(πΌ β β‘πΊ)))) | ||
Theorem | cdlemk19ylem 40340* | Lemma for cdlemk19y 40342. (Contributed by NM, 30-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β β¦πΉ / πβ¦π = (πβπ)) | ||
Theorem | cdlemk11tb 40341* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. πΊ, πΌ stand for g, h. cdlemk11ta 40339 with hypotheses removed. TODO: Can this be proved directly with no quantification? (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπ) β (π βπΌ)))) β β¦πΊ / πβ¦π β€ (β¦πΌ / πβ¦π β¨ (π β(πΌ β β‘πΊ)))) | ||
Theorem | cdlemk19y 40342* | cdlemk19 40279 with simpler hypotheses. TODO: Clean all this up. (Contributed by NM, 30-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β β¦πΉ / πβ¦π = (πβπ)) | ||
Theorem | cdlemkid3N 40343* | Lemma for cdlemkid 40346. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π))) | ||
Theorem | cdlemkid4 40344* | Lemma for cdlemkid 40346. (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = ( I βΎ π΅)))) | ||
Theorem | cdlemkid5 40345* | Lemma for cdlemkid 40346. (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π β π) | ||
Theorem | cdlemkid 40346* | The value of the tau function (in Lemma K of [Crawley] p. 118) on the identity relation. (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = ( I βΎ π΅)) | ||
Theorem | cdlemk35s 40347* | Substitution version of cdlemk35 40322. (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
Theorem | cdlemk35s-id 40348* | Substitution version of cdlemk35 40322. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
Theorem | cdlemk39s 40349* | Substitution version of cdlemk39 40326. TODO: Can any commonality with cdlemk35s 40347 be exploited? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
Theorem | cdlemk39s-id 40350* | Substitution version of cdlemk39 40326 with non-identity requirement on πΊ removed. TODO: Can any commonality with cdlemk35s 40347 be exploited? (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
Theorem | cdlemk42 40351* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 20-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β (β¦πΊ / πβ¦πβπ) = β¦πΊ / πβ¦π) | ||
Theorem | cdlemk19xlem 40352* | Lemma for cdlemk19x 40353. (Contributed by NM, 30-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β (β¦πΉ / πβ¦πβπ) = (πβπ)) | ||
Theorem | cdlemk19x 40353* | cdlemk19 40279 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 40354* | 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 40355* | 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 40356* | 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 40357* | 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 40358* | 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 40359* | 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 40360* | 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 40361* | 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 40362* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 40364? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π)))) | ||
Theorem | cdlemk51 40363* | Part of proof of Lemma K of [Crawley] p. 118. Line 6, p. 120. πΊ, πΌ stand for g, h. π represents tau. TODO: Combine into cdlemk52 40364? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅))) β (((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π ββ¦πΊ / πβ¦π))) β€ (((β¦πΊ / πβ¦πβπ) β¨ (π βπΌ)) β§ ((β¦πΌ / πβ¦πβπ) β¨ (π βπΊ)))) | ||
Theorem | cdlemk52 40364* | 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 40365* | Lemma for cdlemk53 40367. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk53b 40366* | Lemma for cdlemk53 40367. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ πΌ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk53 40367* | 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 40368* | 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 40369* | Lemma for cdlemk55 40371. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΌ β π β§ (π βπΊ) = (π βπΌ)) β§ π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΊ) β§ (π βπ) β (π β(πΊ β πΌ))))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk55b 40370* | Lemma for cdlemk55 40371. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΌ β π β§ (π βπΊ) = (π βπΌ))) β β¦(πΊ β πΌ) / πβ¦π = (β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)) | ||
Theorem | cdlemk55 40371* | 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 40372* | 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 40373* | 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 40374* | Substitution version of cdlemk35 40322. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβπΊ) β π) | ||
Theorem | cdlemk55u1 40375* | Lemma for cdlemk55u 40376. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ (((π βπΉ) = (π βπ) β§ πΉ β π) β§ πΊ β π β§ πΌ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πβ(πΊ β πΌ)) = ((πβπΊ) β (πβπΌ))) | ||
Theorem | cdlemk55u 40376* | 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 40377* | Lemma for cdlemk39u 40378. (Contributed by NM, 31-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (π β(πβπΊ)) β€ (π βπΊ)) | ||
Theorem | cdlemk39u 40378* | 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 40379* | cdlemk19 40279 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 40380* | 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 40381* | 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 40382* | Use a fixed element to eliminate π in cdlemk19u 40380. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (πβπΉ) = π) | ||
Theorem | cdlemk56w 40383* | Use a fixed element to eliminate π in cdlemk56 40381. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ β₯ = (ocβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ( β₯ βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) & β’ π = (π β π β¦ if(πΉ = π, π, π)) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπΉ) = (π βπ)) β (π β πΈ β§ (πβπΉ) = π)) | ||
Theorem | cdlemk 40384* | 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 40385* | Generalization of Lemma K of [Crawley] p. 118, cdlemk 40384. TODO: can this be used to shorten uses of cdlemk 40384? (Contributed by NM, 15-Oct-2013.) |
β’ β€ = (leβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π βπ) β€ (π βπΉ)) β βπ’ β πΈ (π’βπΉ) = π) | ||
Theorem | cdleml1N 40386 | 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 40387* | 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 40388* | 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 40389* | 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 40390* | 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 40391* | 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 40392* | 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 40393* | 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 40394* | 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 40395* | 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 39973. πΈ is the division ring base by erngdv 40403, and π βπΉ is the scalar product by dvavsca 40427. πΉ 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 40396* | Two expressions for the 1-dimensional subspaces of vector space π», in the isomorphism B case where the second 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 40397 | Value of the endomorphism division ring unity. (Contributed by NM, 12-Oct-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ ((πΎ β HL β§ π β π») β π· β Ring) β β’ ((πΎ β HL β§ π β π») β (1rβπ·) = ( I βΎ π)) | ||
Theorem | erngdvlem1 40398* | Lemma for eringring 40402. (Contributed by NM, 4-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Grp) | ||
Theorem | erngdvlem2N 40399* | Lemma for eringring 40402. (Contributed by NM, 6-Aug-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) β β’ ((πΎ β HL β§ π β π») β π· β Abel) | ||
Theorem | erngdvlem3 40400* | Lemma for eringring 40402. (Contributed by NM, 6-Aug-2013.) |
β’ π» = (LHypβπΎ) & β’ π· = ((EDRingβπΎ)βπ) & β’ π΅ = (BaseβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β πΈ, π β πΈ β¦ (π β π β¦ ((πβπ) β (πβπ)))) & β’ 0 = (π β π β¦ ( I βΎ π΅)) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(πβπ))) & β’ + = (π β πΈ, π β πΈ β¦ (π β π)) β β’ ((πΎ β HL β§ π β π») β π· β Ring) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |