Home | Metamath
Proof Explorer Theorem List (p. 393 of 470) | < Previous Next > |
Bad symbols? Try the
GIF version. |
||
Mirrors > Metamath Home Page > MPE Home Page > Theorem List Contents > Recent Proofs This page: Page List |
Color key: | Metamath Proof Explorer
(1-29646) |
Hilbert Space Explorer
(29647-31169) |
Users' Mathboxes
(31170-46948) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemk13 39201* | Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) = ((π β¨ (π βπ·)) β§ ((πβπ) β¨ (π β(π· β β‘πΉ))))) | ||
Theorem | cdlemkole 39202* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ (π β¨ (π βπ·))) | ||
Theorem | cdlemk14 39203* | Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ ((πβπ) β¨ (π β(πΉ β β‘π·)))) | ||
Theorem | cdlemk15 39204* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·))))) | ||
Theorem | cdlemk16a 39205* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β π΄ β§ Β¬ ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β€ π)) | ||
Theorem | cdlemk16 39206* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·)))) β π΄ β§ Β¬ ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·)))) β€ π)) | ||
Theorem | cdlemk17 39207* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. π, π· are k1, f1. (Contributed by NM, 1-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) = ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘π·))))) | ||
Theorem | cdlemk1u 39208* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (π β¨ (πβπ)) β€ ((π·βπ) β¨ (π βπ·))) | ||
Theorem | cdlemk5auN 39209* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π· β π β§ πΊ β π β§ π β π) β§ ((π βπΊ) β (π βπ·) β§ (π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((π·βπ) β¨ (π βπ·)) β§ ((π·βπ) β¨ (π β(πΊ β β‘π·)))) β€ ((πβπ) β¨ (π β(π β β‘π·)))) | ||
Theorem | cdlemk5u 39210* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((π β¨ (πβπ)) β§ ((πΊβπ) β¨ (π β(πΊ β β‘π·)))) β€ ((πβπ) β¨ (π β(π β β‘π·)))) | ||
Theorem | cdlemk6u 39211* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 38235. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π β(π β β‘π·)) β¨ (πβπ))))) | ||
Theorem | cdlemkj 39212* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β π β π) | ||
Theorem | cdlemkuvN 39213* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma1 (p) function π. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ (πΊ β π β (πβπΊ) = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))))) | ||
Theorem | cdlemkuel 39214* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 39212? (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπΊ) β π) | ||
Theorem | cdlemkuat 39215* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) β π΄) | ||
Theorem | cdlemkuv2 39216* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 1, where sigma1 (p) is π, f1 is π·, and k1 is π. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·))))) | ||
Theorem | cdlemk18 39217* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, π· are k, sigma1 (p), k1, f1. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) = ((πβπΉ)βπ)) | ||
Theorem | cdlemk19 39218* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, π· are k, sigma1 (p), k1, f1. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπΉ) = π) | ||
Theorem | cdlemk7u 39219* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma1 case. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ π)) | ||
Theorem | cdlemk11u 39220* | Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma1 (π) case. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ π β ( I βΎ π΅) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π β(π β β‘πΊ)))) | ||
Theorem | cdlemk12u 39221* | Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma1 (π) case. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β ( I βΎ π΅) β§ (π βπΊ) β (π βπ)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘πΊ))))) | ||
Theorem | cdlemk21N 39222* | Part of proof of Lemma K of [Crawley] p. 118. Lines 26-27, p. 119 for i=0 and j=1. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπΊ) β (π βπΉ)))) β ((πβπΊ)βπ) = ((πβπΊ)βπ)) | ||
Theorem | cdlemk20 39223* | 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.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) & β’ π = (πβπΆ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΆ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΆ) β (π βπΉ) β§ (π βπΆ) β (π βπ·)))) β ((πβπΆ)βπ) = (πβπ)) | ||
Theorem | cdlemkoatnle-2N 39224* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) | ||
Theorem | cdlemk13-2N 39225* | Part of proof of Lemma K of [Crawley] p. 118. Line 13 on p. 119. π, πΆ are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) = ((π β¨ (π βπΆ)) β§ ((πβπ) β¨ (π β(πΆ β β‘πΉ))))) | ||
Theorem | cdlemkole-2N 39226* | Utility lemma. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) β€ (π β¨ (π βπΆ))) | ||
Theorem | cdlemk14-2N 39227* | Part of proof of Lemma K of [Crawley] p. 118. Line 19 on p. 119. π, πΆ are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) β€ ((πβπ) β¨ (π β(πΉ β β‘πΆ)))) | ||
Theorem | cdlemk15-2N 39228* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. π, πΆ are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) β€ ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘πΆ))))) | ||
Theorem | cdlemk16-2N 39229* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘πΆ)))) β π΄ β§ Β¬ ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘πΆ)))) β€ π)) | ||
Theorem | cdlemk17-2N 39230* | Part of proof of Lemma K of [Crawley] p. 118. Line 21 on p. 119. π, πΆ are k2, f2. (Contributed by NM, 1-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) = ((π β¨ (π βπΉ)) β§ ((πβπ) β¨ (π β(πΉ β β‘πΆ))))) | ||
Theorem | cdlemkj-2N 39231* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΆ))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΆ) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β π β π) | ||
Theorem | cdlemkuv-2N 39232* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma2 (p) function, given π. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ (πΊ β π β (πβπΊ) = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΆ)))))) | ||
Theorem | cdlemkuel-2N 39233* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 39212? (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΆ) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπΊ) β π) | ||
Theorem | cdlemkuv2-2 39234* | Part of proof of Lemma K of [Crawley] p. 118. Line 16 on p. 119 for i = 2, where sigma2 (p) is π, f2 is πΆ, and k2 is π. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΆ) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΆ))))) | ||
Theorem | cdlemk18-2N 39235* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, πΆ are k, sigma2 (p), k2, f2. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπ) = ((πβπΉ)βπ)) | ||
Theorem | cdlemk19-2N 39236* | Part of proof of Lemma K of [Crawley] p. 118. Line 22 on p. 119. π, π, π, πΆ are k, sigma2 (p), k2, f2. (Contributed by NM, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ ((π βπΆ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπΉ) = π) | ||
Theorem | cdlemk7u-2N 39237* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119 for the sigma2 case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΆ)) β¨ (π β(π β β‘πΆ)))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΆ β π β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π β§ π β ( I βΎ π΅))) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΊ) β (π βπΆ) β§ (π βπ) β (π βπΆ)) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ π)) | ||
Theorem | cdlemk11u-2N 39238* | Part of proof of Lemma K of [Crawley] p. 118. Line 17, p. 119, showing Eq. 3 (line 8, p. 119) for the sigma2 (π) case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΆ)) β¨ (π β(π β β‘πΆ)))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΆ β π β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π β§ π β ( I βΎ π΅))) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΊ) β (π βπΆ) β§ (π βπ) β (π βπΆ)) β§ (πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π β(π β β‘πΊ)))) | ||
Theorem | cdlemk12u-2N 39239* | Part of proof of Lemma K of [Crawley] p. 118. Line 18, p. 119, showing Eq. 4 (line 10, p. 119) for the sigma2 (π) case. (Contributed by NM, 5-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ (((πΎ β HL β§ π β π» β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΆ β π β§ π β π) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ (π β π β§ π β ( I βΎ π΅))) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΊ) β (π βπΆ) β§ (π βπ) β (π βπΆ)) β§ ((π βπΊ) β (π βπ) β§ πΉ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘πΊ))))) | ||
Theorem | cdlemk21-2N 39240* | 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 39241* | 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 39242* | 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 39243* | 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 39244* | 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 39245* | 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 39246* | 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 39247* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma2 (p) function to be a translation. TODO: combine cdlemkj 39212? (Contributed by NM, 11-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (π·ππΊ) β π) | ||
Theorem | cdlemkuv2-3N 39248* | 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 39249* | 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 39250* | 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 39251* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the (π βπΆ) β (π βπ·) requirement from cdlemk22-3 39250. (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π β§ π₯ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅) β§ π₯ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ ((π βπΊ) β (π βπ·) β§ (π βπ₯) β (π βπΆ)) β§ ((π βπ₯) β (π βπ·) β§ (π βπ₯) β (π βπΉ) β§ (π βπΊ) β (π βπ₯)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk24-3 39252* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the (π βπ₯) β (π βπΆ) requirement from cdlemk23-3 39251 using (π βπΆ) = (π βπ·). (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π β§ π₯ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅) β§ π₯ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ ((π βπΊ) β (π βπ·) β§ (π βπΆ) = (π βπ·)) β§ ((π βπ₯) β (π βπ·) β§ (π βπ₯) β (π βπΉ) β§ (π βπΊ) β (π βπ₯)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk25-3 39253* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the (π βπΆ) = (π βπ·) requirement from cdlemk24-3 39252. (Contributed by NM, 7-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π β§ π₯ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅) β§ π₯ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ (π βπΊ) β (π βπ·) β§ ((π βπ₯) β (π βπ·) β§ (π βπ₯) β (π βπΉ) β§ (π βπΊ) β (π βπ₯)))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk26b-3 39254* | 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 39255* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the π₯ requirements from cdlemk25-3 39253. (Contributed by NM, 10-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ (π βπΊ) β (π βπ·))) β ((π·ππΊ)βπ) = ((πΆππΊ)βπ)) | ||
Theorem | cdlemk27-3 39256* | Part of proof of Lemma K of [Crawley] p. 118. Eliminate the π from the conclusion of cdlemk25-3 39253. (Contributed by NM, 10-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ π· β π β§ π β π) β§ (πΊ β π β§ πΆ β π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ ((π βπΉ) = (π βπ) β§ πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅))) β§ (((π βπΊ) β (π βπΆ) β§ (π βπΆ) β (π βπΉ) β§ (π βπ·) β (π βπΉ)) β§ (π βπΊ) β (π βπ·))) β (π·ππΊ) = (πΆππΊ)) | ||
Theorem | cdlemk28-3 39257* | 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 39258* | 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 39259. (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 39259* | 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 39260* | 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 39261* | Part of proof of Lemma K of [Crawley] p. 118. cdlemk29-3 39260 with shorter hypotheses. (Contributed by NM, 18-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β π β π) | ||
Theorem | cdlemk36 39262* | 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 39263* | 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 39264* | Part of proof of Lemma K of [Crawley] p. 118. Line 31, p. 119. TODO: derive more directly with r19.23 3238? (Contributed by NM, 19-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (πβπ) β€ (π β¨ (π βπΊ))) | ||
Theorem | cdlemk39 39265* | 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 39266* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
β’ π = (β©π§ β π π) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ (πΊ β π β (πβπΊ) = if(πΉ = π, πΊ, β¦πΊ / πβ¦π)) | ||
Theorem | cdlemk40t 39267* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
β’ π = (β©π§ β π π) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((πΉ = π β§ πΊ β π) β (πβπΊ) = πΊ) | ||
Theorem | cdlemk40f 39268* | TODO: fix comment. (Contributed by NM, 31-Jul-2013.) |
β’ π = (β©π§ β π π) & β’ π = (π β π β¦ if(πΉ = π, π, π)) β β’ ((πΉ β π β§ πΊ β π) β (πβπΊ) = β¦πΊ / πβ¦π) | ||
Theorem | cdlemk41 39269* | Part of proof of Lemma K of [Crawley] p. 118. TODO: fix comment. (Contributed by NM, 19-Jul-2013.) |
β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ (πΊ β π β β¦πΊ / πβ¦π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘π))))) | ||
Theorem | cdlemkfid1N 39270 | Lemma for cdlemkfid3N 39274. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ πΊ β π) β§ ((π βπΊ) β (π βπΉ) β§ (π β π΄ β§ Β¬ π β€ π))) β ((π β¨ (π βπΊ)) β§ ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) = (πΊβπ)) | ||
Theorem | cdlemkid1 39271 | Lemma for cdlemkid 39285. (Contributed by NM, 24-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π β§ π β ( I βΎ π΅)))) β (π β¨ (π βπ)) = (π β¨ (π βπ))) | ||
Theorem | cdlemkfid2N 39272 | Lemma for cdlemkfid3N 39274. (Contributed by NM, 29-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ = π) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ ((π βπ) β (π βπΉ) β§ (π β π΄ β§ Β¬ π β€ π))) β π = (πβπ)) | ||
Theorem | cdlemkid2 39273* | Lemma for cdlemkid 39285. (Contributed by NM, 24-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅) β§ (π β π β§ π β ( I βΎ π΅)))) β β¦πΊ / πβ¦π = π) | ||
Theorem | cdlemkfid3N 39274* | 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 39275* | Part of proof of Lemma K of [Crawley] p. 118. TODO: clean up (πππΊ) stuff. π represents π in cdlemk31 39245. (Contributed by NM, 21-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (π β π, π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)))) β β¦πΊ / πβ¦π = ((πππΊ)βπ)) | ||
Theorem | cdlemkyu 39276* | Convert between function and explicit forms. πΆ represents π in cdlemkuu 39244. 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 39277* | cdlemkyu 39276 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 39278* | 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 39279* | Lemma for cdlemk19y 39281. (Contributed by NM, 30-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ πΆ = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘π)))))) β β’ ((((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β β¦πΉ / πβ¦π = (πβπ)) | ||
Theorem | cdlemk11tb 39280* | Part of proof of Lemma K of [Crawley] p. 118. Lemma for Eq. 5, p. 119. πΊ, πΌ stand for g, h. cdlemk11ta 39278 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 39281* | cdlemk19 39218 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 39282* | Lemma for cdlemkid 39285. (Contributed by NM, 25-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β (π§βπ) = π))) | ||
Theorem | cdlemkid4 39283* | Lemma for cdlemkid 39285. (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπΊ)) β π§ = ( I βΎ π΅)))) | ||
Theorem | cdlemkid5 39284* | Lemma for cdlemkid 39285. (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π β§ (π βπΉ) = (π βπ)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΊ = ( I βΎ π΅))) β β¦πΊ / πβ¦π β π) | ||
Theorem | cdlemkid 39285* | 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 39286* | Substitution version of cdlemk35 39261. (Contributed by NM, 22-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
Theorem | cdlemk35s-id 39287* | Substitution version of cdlemk35 39261. (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β β¦πΊ / πβ¦π β π) | ||
Theorem | cdlemk39s 39288* | Substitution version of cdlemk39 39265. TODO: Can any commonality with cdlemk35s 39286 be exploited? (Contributed by NM, 23-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ (πΊ β π β§ πΊ β ( I βΎ π΅)) β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
Theorem | cdlemk39s-id 39289* | Substitution version of cdlemk39 39265 with non-identity requirement on πΊ removed. TODO: Can any commonality with cdlemk35s 39286 be exploited? (Contributed by NM, 26-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ (((πΎ β HL β§ π β π») β§ ((πΉ β π β§ πΉ β ( I βΎ π΅)) β§ πΊ β π β§ π β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ))) β (π ββ¦πΊ / πβ¦π) β€ (π βπΊ)) | ||
Theorem | cdlemk42 39290* | 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 39291* | Lemma for cdlemk19x 39292. (Contributed by NM, 30-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))) & β’ π = ((π β¨ (π βπ)) β§ (π β¨ (π β(π β β‘π)))) & β’ π = (β©π§ β π βπ β π ((π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ) β§ (π βπ) β (π βπ)) β (π§βπ) = π)) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ)) β§ ((πΉ β π β§ πΉ β ( I βΎ π΅) β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β ( I βΎ π΅) β§ (π βπ) β (π βπΉ)))) β (β¦πΉ / πβ¦πβπ) = (πβπ)) | ||
Theorem | cdlemk19x 39292* | cdlemk19 39218 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 39293* | 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 39294* | 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 39295* | 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 39296* | 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 39297* | 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 39298* | 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 39299* | 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 39300* | 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 βΎ π΅))) β ((β¦πΊ / πβ¦π β β¦πΌ / πβ¦π)βπ) β€ ((β¦πΊ / πβ¦πβπ) β¨ (π ββ¦πΌ / πβ¦π))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |