![]() |
Metamath
Proof Explorer Theorem List (p. 403 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 | tendo0pl 40201* | Property of the additive identity endormorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendo0plr 40202* | Property of the additive identity endormorphism. (Contributed by NM, 21-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πππ) = π) | ||
Theorem | tendoicbv 40203* | Define inverse function for trace-preserving endomorphisms. Change bound variable to isolate it later. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ πΌ = (π’ β πΈ β¦ (π β π β¦ β‘(π’βπ))) | ||
Theorem | tendoi 40204* | Value of inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ (π β πΈ β (πΌβπ) = (π β π β¦ β‘(πβπ))) | ||
Theorem | tendoi2 40205* | Value of additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π = ((LTrnβπΎ)βπ) β β’ ((π β πΈ β§ πΉ β π) β ((πΌβπ)βπΉ) = β‘(πβπΉ)) | ||
Theorem | tendoicl 40206* | Closure of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (πΌβπ) β πΈ) | ||
Theorem | tendoipl 40207* | Property of the additive inverse endomorphism. (Contributed by NM, 12-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β ((πΌβπ)ππ) = π) | ||
Theorem | tendoipl2 40208* | Property of the additive inverse endomorphism. (Contributed by NM, 29-Sep-2014.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ πΌ = (π β πΈ β¦ (π β π β¦ β‘(π βπ))) & β’ π΅ = (BaseβπΎ) & β’ π = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ)))) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (ππ(πΌβπ)) = π) | ||
Theorem | erngfset 40209* | The division rings on trace-preserving endomorphisms for a lattice πΎ. (Contributed by NM, 8-Jun-2013.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (EDRingβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((TEndoβπΎ)βπ€)β©, β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β π‘))β©})) | ||
Theorem | erngset 40210* | The division ring on trace-preserving endomorphisms for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π· = {β¨(Baseβndx), πΈβ©, β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β πΈ, π‘ β πΈ β¦ (π β π‘))β©}) | ||
Theorem | erngbase 40211 | The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom π). TODO: the .t hypothesis isn't used. (Also look at others.) (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ πΆ = (Baseβπ·) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
Theorem | erngfplus 40212* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus 40213* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2 40214 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul 40215* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π β π‘))) | ||
Theorem | erngmul 40216 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | erngfset-rN 40217* | The division rings on trace-preserving endomorphisms for a lattice πΎ. (Contributed by NM, 8-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) β β’ (πΎ β π β (EDRingRβπΎ) = (π€ β π» β¦ {β¨(Baseβndx), ((TEndoβπΎ)βπ€)β©, β¨(+gβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π β ((LTrnβπΎ)βπ€) β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β ((TEndoβπΎ)βπ€), π‘ β ((TEndoβπΎ)βπ€) β¦ (π‘ β π ))β©})) | ||
Theorem | erngset-rN 40218* | The division ring on trace-preserving endomorphisms for a fiducial co-atom π. (Contributed by NM, 5-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) β β’ ((πΎ β π β§ π β π») β π· = {β¨(Baseβndx), πΈβ©, β¨(+gβndx), (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))β©, β¨(.rβndx), (π β πΈ, π‘ β πΈ β¦ (π‘ β π ))β©}) | ||
Theorem | erngbase-rN 40219 | The base set of the division ring on trace-preserving endomorphisms is the set of all trace-preserving endomorphisms (for a fiducial co-atom π). (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ πΆ = (Baseβπ·) β β’ ((πΎ β π β§ π β π») β πΆ = πΈ) | ||
Theorem | erngfplus-rN 40220* | Ring addition operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ ((πΎ β π β§ π β π») β + = (π β πΈ, π‘ β πΈ β¦ (π β π β¦ ((π βπ) β (π‘βπ))))) | ||
Theorem | erngplus-rN 40221* | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π + π) = (π β π β¦ ((πβπ) β (πβπ)))) | ||
Theorem | erngplus2-rN 40222 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ + = (+gβπ·) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ πΉ β π)) β ((π + π)βπΉ) = ((πβπΉ) β (πβπΉ))) | ||
Theorem | erngfmul-rN 40223* | Ring multiplication operation. (Contributed by NM, 9-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ ((πΎ β π β§ π β π») β Β· = (π β πΈ, π‘ β πΈ β¦ (π‘ β π ))) | ||
Theorem | erngmul-rN 40224 | Ring addition operation. (Contributed by NM, 10-Jun-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π· = ((EDRingRβπΎ)βπ) & β’ Β· = (.rβπ·) β β’ (((πΎ β π β§ π β π») β§ (π β πΈ β§ π β πΈ)) β (π Β· π) = (π β π)) | ||
Theorem | cdlemh1 40225 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ π β π΄) β§ (π β€ (π β¨ (π βπΉ)) β§ (π βπΉ) β (π βπΊ))) β (π β¨ (π β(πΊ β β‘πΉ))) = (π β¨ (π β(πΊ β β‘πΉ)))) | ||
Theorem | cdlemh2 40226 | Part of proof of Lemma H of [Crawley] p. 118. (Contributed by NM, 16-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘πΉ)))) & β’ 0 = (0.βπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) β (π βπΊ))) β (π β§ π) = 0 ) | ||
Theorem | cdlemh 40227 | Lemma H of [Crawley] p. 118. (Contributed by NM, 17-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (π β¨ (π β(πΊ β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ π β€ (π β¨ (π βπΉ))) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) β (π βπΊ))) β (π β π΄ β§ Β¬ π β€ π)) | ||
Theorem | cdlemi1 40228 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (π β¨ (π βπΊ))) | ||
Theorem | cdlemi2 40229 | Part of proof of Lemma I of [Crawley] p. 118. (Contributed by NM, 18-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πβπΊ)βπ) β€ (((πβπΉ)βπ) β¨ (π β(πΊ β β‘πΉ)))) | ||
Theorem | cdlemi 40230 | Lemma I of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = ((π β¨ (π βπΊ)) β§ (((πβπΉ)βπ) β¨ (π β(πΊ β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β πΈ β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΉ) β (π βπΊ))) β ((πβπΊ)βπ) = π) | ||
Theorem | cdlemj1 40231 | Part of proof of Lemma J of [Crawley] p. 118. (Contributed by NM, 19-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ (β β ( I βΎ π΅) β§ π β π β§ π β ( I βΎ π΅)) β§ ((π βπΉ) β (π βπ) β§ (π βπ) β (π ββ) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πββ)βπ) = ((πββ)βπ)) | ||
Theorem | cdlemj2 40232 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate π. (Contributed by NM, 20-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ (β β ( I βΎ π΅) β§ π β π β§ π β ( I βΎ π΅)) β§ ((π βπΉ) β (π βπ) β§ (π βπ) β (π ββ))) β (πββ) = (πββ)) | ||
Theorem | cdlemj3 40233 | Part of proof of Lemma J of [Crawley] p. 118. Eliminate π. (Contributed by NM, 20-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅) β§ β β π)) β§ β β ( I βΎ π΅)) β (πββ) = (πββ)) | ||
Theorem | tendocan 40234 | Cancellation law: if the values of two trace-preserving endormorphisms are equal, so are the endormorphisms. Lemma J of [Crawley] p. 118. (Contributed by NM, 21-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β πΈ β§ (πβπΉ) = (πβπΉ)) β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β π = π) | ||
Theorem | tendoid0 40235* | A trace-preserving endomorphism is the additive identity iff at least one of its values (at a non-identity translation) is the identity translation. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ β§ (πΉ β π β§ πΉ β ( I βΎ π΅))) β ((πβπΉ) = ( I βΎ π΅) β π = π)) | ||
Theorem | tendo0mul 40236* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β π) = π) | ||
Theorem | tendo0mulr 40237* | Additive identity multiplied by a trace-preserving endomorphism. (Contributed by NM, 13-Feb-2014.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ π β πΈ) β (π β π) = π) | ||
Theorem | tendo1ne0 40238* | The identity (unity) is not equal to the zero trace-preserving endomorphism. (Contributed by NM, 8-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ ((πΎ β HL β§ π β π») β ( I βΎ π) β π) | ||
Theorem | tendoconid 40239* | The composition (product) of trace-preserving endormorphisms is nonzero when each argument is nonzero. (Contributed by NM, 8-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ (π β πΈ β§ π β π)) β (π β π) β π) | ||
Theorem | tendotr 40240* | The trace of the value of a nonzero trace-preserving endomorphism equals the trace of the argument. (Contributed by NM, 11-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ πΈ = ((TEndoβπΎ)βπ) & β’ π = (π β π β¦ ( I βΎ π΅)) β β’ (((πΎ β HL β§ π β π») β§ (π β πΈ β§ π β π) β§ πΉ β π) β (π β(πβπΉ)) = (π βπΉ)) | ||
Theorem | cdlemk1 40241 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ ((π βπΉ) = (π βπ) β§ (π β π΄ β§ Β¬ π β€ π))) β (π β¨ (πβπ)) = ((πΉβπ) β¨ (π βπΉ))) | ||
Theorem | cdlemk2 40242 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 22-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (π β(πΊ β β‘πΉ))) = ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) | ||
Theorem | cdlemk3 40243 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π) β§ ((π βπΊ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((πΉβπ) β¨ (π βπΉ)) β§ ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) = (πΉβπ)) | ||
Theorem | cdlemk4 40244 | Part of proof of Lemma K of [Crawley] p. 118, last line. We use π for their h, since π» is already used. (Contributed by NM, 24-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) β€ ((πβπ) β¨ (π β(π β β‘πΉ)))) | ||
Theorem | cdlemk5a 40245 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 3-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ π β π) β§ ((π βπΊ) β (π βπΉ) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (((πΉβπ) β¨ (π βπΉ)) β§ ((πΉβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((πβπ) β¨ (π β(π β β‘πΉ)))) | ||
Theorem | cdlemk5 40246 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β ((π β¨ (πβπ)) β§ ((πΊβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((πβπ) β¨ (π β(π β β‘πΉ)))) | ||
Theorem | cdlemk6 40247 | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 39296. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ ((π βπΊ) β (π βπΉ) β§ (π βπ) β (π βπΉ)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β¨ (((πβπ) β¨ π) β§ ((π β(π β β‘πΉ)) β¨ (πβπ))))) | ||
Theorem | cdlemk8 40248 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 26-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β¨ (πβπ)) = ((πΊβπ) β¨ (π β(π β β‘πΊ)))) | ||
Theorem | cdlemk9 40249 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊβπ) β¨ (πβπ)) β§ π) = (π β(π β β‘πΊ))) | ||
Theorem | cdlemk9bN 40250 | Part of proof of Lemma K of [Crawley] p. 118. TODO: is this needed? If so, shorten with cdlemk9 40249 if that one is also needed. (Contributed by NM, 28-Jun-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β (((πΊβπ) β¨ (πβπ)) β§ π) = (π β(πΊ β β‘π))) | ||
Theorem | cdlemki 40251* | Part of proof of Lemma K of [Crawley] p. 118. TODO: Eliminate and put into cdlemksel 40255. (Contributed by NM, 25-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ πΌ = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β πΌ β π) | ||
Theorem | cdlemkvcl 40252 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ π β π) β§ π β π΄) β π β π΅) | ||
Theorem | cdlemk10 40253 | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 29-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β β’ (((πΎ β HL β§ π β π») β§ (πΉ β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π)) β π β€ (π β(π β β‘πΊ))) | ||
Theorem | cdlemksv 40254* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function. (Contributed by NM, 26-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ (πΊ β π β (πβπΊ) = (β©π β π (πβπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ)))))) | ||
Theorem | cdlemksel 40255* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma(p) function to be a translation. TODO: combine cdlemki 40251? (Contributed by NM, 26-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β (πβπΊ) β π) | ||
Theorem | cdlemksat 40256* | Part of proof of Lemma K of [Crawley] p. 118. (Contributed by NM, 27-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β ((πβπΊ)βπ) β π΄) | ||
Theorem | cdlemksv2 40257* | Part of proof of Lemma K of [Crawley] p. 118. Value of the sigma(p) function π at the fixed π parameter. (Contributed by NM, 26-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ (π βπΊ) β (π βπΉ))) β ((πβπΊ)βπ) = ((π β¨ (π βπΊ)) β§ ((πβπ) β¨ (π β(πΊ β β‘πΉ))))) | ||
Theorem | cdlemk7 40258* | Part of proof of Lemma K of [Crawley] p. 118. Line 5, p. 119. (Contributed by NM, 27-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ (π βπΊ) β (π βπΉ) β§ (π βπ) β (π βπΉ))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ π)) | ||
Theorem | cdlemk11 40259* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 3, line 8, p. 119. (Contributed by NM, 29-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘πΉ)) β¨ (π β(π β β‘πΉ)))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ (π βπΊ) β (π βπΉ) β§ (π βπ) β (π βπΉ))) β ((πβπΊ)βπ) β€ (((πβπ)βπ) β¨ (π β(π β β‘πΊ)))) | ||
Theorem | cdlemk12 40260* | Part of proof of Lemma K of [Crawley] p. 118. Eq. 4, line 10, p. 119. (Contributed by NM, 30-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β§ = (meetβπΎ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ πΊ β π) β§ ((π β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π β ( I βΎ π΅)) β§ ((π βπΊ) β (π βπΉ) β§ (π βπ) β (π βπΉ)) β§ (π βπΊ) β (π βπ))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘πΊ))))) | ||
Theorem | cdlemkoatnle 40261* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β ((πβπ) β π΄ β§ Β¬ (πβπ) β€ π)) | ||
Theorem | cdlemk13 40262* | 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 40263* | Utility lemma. (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ (πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ (π βπ·) β (π βπΉ))) β (πβπ) β€ (π β¨ (π βπ·))) | ||
Theorem | cdlemk14 40264* | 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 40265* | 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 40266* | 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 40267* | 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 40268* | 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 40269* | 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 40270* | 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 40271* | 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 40272* | Part of proof of Lemma K of [Crawley] p. 118. Apply dalaw 39296. (Contributed by NM, 4-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) β β’ ((((πΎ β HL β§ π β π») β§ πΉ β π β§ π· β π) β§ ((π β π β§ πΊ β π β§ π β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π βπΉ) = (π βπ)) β§ ((πΉ β ( I βΎ π΅) β§ π· β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅)) β§ ((π βπ·) β (π βπΉ) β§ (π βπΊ) β (π βπ·) β§ (π βπ) β (π βπ·)))) β ((π β¨ (πΊβπ)) β§ ((πβπ) β¨ (π β(πΊ β β‘π·)))) β€ ((((πΊβπ) β¨ (πβπ)) β§ ((π β(πΊ β β‘π·)) β¨ (π β(π β β‘π·)))) β¨ (((πβπ) β¨ π) β§ ((π β(π β β‘π·)) β¨ (πβπ))))) | ||
Theorem | cdlemkj 40273* | 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 40274* | 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 40275* | Part of proof of Lemma K of [Crawley] p. 118. Conditions for the sigma1 (p) function to be a translation. TODO: combine cdlemkj 40273? (Contributed by NM, 2-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπ·) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘π·)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ π· β π β§ π β π) β§ (((π βπ·) β (π βπΉ) β§ (π βπ·) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ π· β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπΊ) β π) | ||
Theorem | cdlemkuat 40276* | 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 40277* | 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 40278* | 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 40279* | 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 40280* | 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 40281* | 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 40282* | 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 40283* | 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 40284* | 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 40285* | 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 40286* | 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 40287* | 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 40288* | 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 40289* | 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 40290* | 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 40291* | 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 40292* | 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 40293* | 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 40294* | 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, 2-Jul-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΉ)))))) & β’ π = (πβπΆ) & β’ π = (π β π β¦ (β©π β π (πβπ) = ((π β¨ (π βπ)) β§ ((πβπ) β¨ (π β(π β β‘πΆ)))))) β β’ ((((πΎ β HL β§ π β π») β§ (π βπΉ) = (π βπ) β§ πΊ β π) β§ (πΉ β π β§ πΆ β π β§ π β π) β§ (((π βπΆ) β (π βπΉ) β§ (π βπΆ) β (π βπΊ)) β§ (πΉ β ( I βΎ π΅) β§ πΊ β ( I βΎ π΅) β§ πΆ β ( I βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β (πβπΊ) β π) | ||
Theorem | cdlemkuv2-2 40295* | 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 40296* | 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 40297* | 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 40298* | 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 40299* | 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 40300* | 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 βΎ π΅)) β§ (π β π΄ β§ Β¬ π β€ π))) β ((πβπΊ)βπ) = ((π β¨ (πΊβπ)) β§ (((πβπ)βπ) β¨ (π β(π β β‘πΊ))))) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |