![]() |
Metamath
Proof Explorer Theorem List (p. 398 of 480) | < 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-30435) |
![]() (30436-31958) |
![]() (31959-47941) |
Type | Label | Description |
---|---|---|
Statement | ||
Theorem | cdlemeg46v1v2 39701* | TODO FIX COMMENT v1 = v2 p. 116 3rd line. (Contributed by NM, 2-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) & β’ π = (((πΉβπ ) β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π = π) | ||
Theorem | cdlemeg46vrg 39702* | TODO FIX COMMENT v1 β€ r β¨ g(s) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) & β’ π = (((πΉβπ ) β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β€ (π β¨ (πΊβπ))) | ||
Theorem | cdlemeg46rgv 39703* | TODO FIX COMMENT r β€ g(s) β¨ v1 p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) & β’ π = (((πΉβπ ) β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β€ ((πΊβπ) β¨ π)) | ||
Theorem | cdlemeg46req 39704* | TODO FIX COMMENT r = (v1 β¨ g(s)) p. 116 3rd line. (Contributed by NM, 3-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) & β’ π = (((πΉβπ ) β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π = ((π β¨ π) β§ ((πΊβπ) β¨ π))) | ||
Theorem | cdlemeg46gfv 39705* | TODO FIX COMMENT p. 115 penultimate line: g(f(r)) = (p v q) ^ (g(s) v v1). (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) & β’ π = ((π β¨ (πΊβπ)) β§ π) & β’ π = (((πΉβπ ) β¨ π) β§ π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβ(πΉβπ )) = ((π β¨ π) β§ ((πΊβπ) β¨ π))) | ||
Theorem | cdlemeg46gfr 39706* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΊβ(πΉβπ )) = π ) | ||
Theorem | cdlemeg46gfre 39707* | TODO FIX COMMENT p. 116 penultimate line: g(f(r)) = r. (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β (πΊβ(πΉβπ )) = π ) | ||
Theorem | cdlemeg46gf 39708* | TODO FIX COMMENT Eliminate antecedent π β€ (π β¨ π). (Contributed by NM, 4-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β (πΊβ(πΉβπ )) = π ) | ||
Theorem | cdlemeg46fgN 39709* | TODO FIX COMMENT p. 116 penultimate line: f(g(r)) = r. (Contributed by NM, 4-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β (πΉβ(πΊβπ )) = π ) | ||
Theorem | cdleme48d 39710* | TODO: fix comment. (Contributed by NM, 8-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π)) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π)) β (πΊβ(πΉβπ)) = π) | ||
Theorem | cdleme48gfv1 39711* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΅ β§ Β¬ π β€ π))) β (πΊβ(πΉβπ)) = π) | ||
Theorem | cdleme48gfv 39712* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β (πΊβ(πΉβπ)) = π) | ||
Theorem | cdleme48fgv 39713* | TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β (πΉβ(πΊβπ)) = π) | ||
Theorem | cdlemeg49lebilem 39714* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅)) β (π β€ π β (πΉβπ) β€ (πΉβπ))) | ||
Theorem | cdleme50lebi 39715* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅)) β (π β€ π β (πΉβπ) β€ (πΉβπ))) | ||
Theorem | cdleme50eq 39716* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΅ β§ π β π΅)) β ((πΉβπ) = (πΉβπ) β π = π)) | ||
Theorem | cdleme50f 39717* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. TODO: can we use just πΉ Fn π΅ since range is computed in cdleme50rn 39720? (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ:π΅βΆπ΅) | ||
Theorem | cdleme50f1 39718* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ:π΅β1-1βπ΅) | ||
Theorem | cdleme50rnlem 39719* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. TODO: can we get rid of πΊ stuff if we show πΊ = β‘πΉ earlier? (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β ran πΉ = π΅) | ||
Theorem | cdleme50rn 39720* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β ran πΉ = π΅) | ||
Theorem | cdleme50f1o 39721* | Part of proof of Lemma D in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ:π΅β1-1-ontoβπ΅) | ||
Theorem | cdleme50laut 39722* | Part of proof of Lemma D in [Crawley] p. 113. πΉ is a lattice automorphism. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ πΌ = (LAutβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β πΌ) | ||
Theorem | cdleme50ldil 39723* | Part of proof of Lemma D in [Crawley] p. 113. πΉ is a lattice dilation. TODO: fix comment. (Contributed by NM, 9-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ πΆ = ((LDilβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β πΆ) | ||
Theorem | cdleme50trn1 39724* | Part of proof that πΉ is a translation. Β¬ π β€ (π β¨ π) case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ Β¬ π β€ (π β¨ π)) β ((π β¨ (πΉβπ )) β§ π) = π) | ||
Theorem | cdleme50trn2a 39725* | Part of proof that πΉ is a translation. π β€ (π β¨ π) case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ (πΉβπ )) β§ π) = π) | ||
Theorem | cdleme50trn2 39726* | Part of proof that πΉ is a translation. Remove π hypotheses no longer needed from cdleme50trn2a 39725. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β€ (π β¨ π)) β ((π β¨ (πΉβπ )) β§ π) = π) | ||
Theorem | cdleme50trn12 39727* | Part of proof that πΉ is a translation. Combine π β€ (π β¨ π) and Β¬ π β€ (π β¨ π) cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π))) β ((π β¨ (πΉβπ )) β§ π) = π) | ||
Theorem | cdleme50trn3 39728* | Part of proof that πΉ is a translation. π = π case. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π = π β§ (π β π΄ β§ Β¬ π β€ π))) β ((π β¨ (πΉβπ )) β§ π) = π) | ||
Theorem | cdleme50trn123 39729* | Part of proof that πΉ is a translation. Combine all cases. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((π β¨ (πΉβπ )) β§ π) = π) | ||
Theorem | cdleme51finvfvN 39730* | Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β (β‘πΉβπ) = (πΊβπ)) | ||
Theorem | cdleme51finvN 39731* | Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) & β’ π = ((π£ β¨ π) β§ (π β¨ ((π β¨ π£) β§ π))) & β’ π = ((π β¨ π) β§ (π β¨ ((π’ β¨ π£) β§ π))) & β’ πΊ = (π β π΅ β¦ if((π β π β§ Β¬ π β€ π), (β©π β π΅ βπ’ β π΄ ((Β¬ π’ β€ π β§ (π’ β¨ (π β§ π)) = π) β π = (if(π’ β€ (π β¨ π), (β©π β π΅ βπ£ β π΄ ((Β¬ π£ β€ π β§ Β¬ π£ β€ (π β¨ π)) β π = π)), β¦π’ / π£β¦π) β¨ (π β§ π)))), π)) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ = πΊ) | ||
Theorem | cdleme50ltrn 39732* | Part of proof of Lemma E in [Crawley] p. 113. πΉ is a lattice translation. TODO: fix comment. (Contributed by NM, 10-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) | ||
Theorem | cdleme51finvtrN 39733* | Part of proof of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 14-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ β π) | ||
Theorem | cdleme50ex 39734* | Part of Lemma E in [Crawley] p. 113. TODO: fix comment. (Contributed by NM, 11-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π (πβπ) = π) | ||
Theorem | cdleme 39735* | Lemma E in [Crawley] p. 113. If p,q are atoms not under hyperplane w, then there is a unique translation f such that f(p) = q. (Contributed by NM, 11-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β β!π β π (πβπ) = π) | ||
Theorem | cdlemf1 39736* | Part of Lemma F in [Crawley] p. 116. TODO: should this or part of it become a stand-alone theorem? (Contributed by NM, 12-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π β§ π β€ (π β¨ π))) | ||
Theorem | cdlemf2 39737* | Part of Lemma F in [Crawley] p. 116. (Contributed by NM, 12-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π΄ βπ β π΄ ((Β¬ π β€ π β§ Β¬ π β€ π) β§ π = ((π β¨ π) β§ π))) | ||
Theorem | cdlemf 39738* | Lemma F in [Crawley] p. 116. If u is an atom under w, there exists a translation whose trace is u. (Contributed by NM, 12-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π (π βπ) = π) | ||
Theorem | cdlemfnid 39739* | cdlemf 39738 with additional constraint of non-identity. (Contributed by NM, 20-Jun-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ π β€ π)) β βπ β π ((π βπ) = π β§ π β ( I βΎ π΅))) | ||
Theorem | cdlemftr3 39740* | Special case of cdlemf 39738 showing existence of non-identity translation with trace different from any 3 given lattice elements. (Contributed by NM, 24-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β βπ β π (π β ( I βΎ π΅) β§ ((π βπ) β π β§ (π βπ) β π β§ (π βπ) β π))) | ||
Theorem | cdlemftr2 39741* | Special case of cdlemf 39738 showing existence of non-identity translation with trace different from any 2 given lattice elements. (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β βπ β π (π β ( I βΎ π΅) β§ (π βπ) β π β§ (π βπ) β π)) | ||
Theorem | cdlemftr1 39742* | Part of proof of Lemma G of [Crawley] p. 116, sixth line of third paragraph on p. 117: there is "a translation h, different from the identity, such that tr h β tr f." (Contributed by NM, 25-Jul-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β βπ β π (π β ( I βΎ π΅) β§ (π βπ) β π)) | ||
Theorem | cdlemftr0 39743* | Special case of cdlemf 39738 showing existence of a non-identity translation. (Contributed by NM, 1-Aug-2013.) |
β’ π΅ = (BaseβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β βπ β π π β ( I βΎ π΅)) | ||
Theorem | trlord 39744* | The ordering of two Hilbert lattice elements (under the fiducial hyperplane π) is determined by the translations whose traces are under them. (Contributed by NM, 3-Mar-2014.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β€ π) β§ (π β π΅ β§ π β€ π)) β (π β€ π β βπ β π ((π βπ) β€ π β (π βπ) β€ π))) | ||
Theorem | cdlemg1a 39745* | Shorter expression for πΊ. TODO: fix comment. TODO: shorten using cdleme 39735 or vice-versa? Also, if not shortened with cdleme 39735, then it can be moved up to save repeating hypotheses. (Contributed by NM, 15-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΊ = (β©π β π (πβπ) = π)) | ||
Theorem | cdlemg1b2 39746* | This theorem can be used to shorten πΊ = hypothesis. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ = πΊ) | ||
Theorem | cdlemg1idlemN 39747* | Lemma for cdlemg1idN 39752. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β§ π = π) β (πΉβπ) = π) | ||
Theorem | cdlemg1fvawlemN 39748* | Lemma for ltrniotafvawN 39753. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ ) β π΄ β§ Β¬ (πΉβπ ) β€ π)) | ||
Theorem | cdlemg1ltrnlem 39749* | Lemma for ltrniotacl 39754. (Contributed by NM, 18-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) | ||
Theorem | cdlemg1finvtrlemN 39750* | Lemma for ltrniotacnvN 39755. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ β π) | ||
Theorem | cdlemg1bOLDN 39751* | This theorem can be used to shorten πΉ = hypothesis that have the form of the conclusion. TODO: fix comment. (Contributed by NM, 16-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΉ = (β©π β π (πβπ) = π) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯))) | ||
Theorem | cdlemg1idN 39752* | Version of cdleme31id 39569 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ πΉ = (β©π β π (πβπ) = π) & β’ π = ((LTrnβπΎ)βπ) & β’ π΅ = (BaseβπΎ) β β’ (((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π β π΅) β§ π = π) β (πΉβπ) = π) | ||
Theorem | ltrniotafvawN 39753* | Version of cdleme46fvaw 39676 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ ) β π΄ β§ Β¬ (πΉβπ ) β€ π)) | ||
Theorem | ltrniotacl 39754* | Version of cdleme50ltrn 39732 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 17-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ β π) | ||
Theorem | ltrniotacnvN 39755* | Version of cdleme51finvtrN 39733 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β β‘πΉ β π) | ||
Theorem | ltrniotaval 39756* | Value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (πΉβπ) = π) | ||
Theorem | ltrniotacnvval 39757* | Converse value of the unique translation specified by a value. (Contributed by NM, 21-Feb-2014.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β (β‘πΉβπ) = π) | ||
Theorem | ltrniotaidvalN 39758* | Value of the unique translation specified by identity value. (Contributed by NM, 25-Aug-2014.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ πΉ = (β©π β π (πβπ) = π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β πΉ = ( I βΎ π΅)) | ||
Theorem | ltrniotavalbN 39759* | Value of the unique translation specified by a value. (Contributed by NM, 10-Mar-2014.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) = π β πΉ = (β©π β π (πβπ) = π))) | ||
Theorem | cdlemeiota 39760* | A translation is uniquely determined by one of its values. (Contributed by NM, 18-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β πΉ = (β©π β π (πβπ) = (πΉβπ))) | ||
Theorem | cdlemg1ci2 39761* | Any function of the form of the function constructed for cdleme 39735 is a translation. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ = (β©π β π (πβπ) = π)) β πΉ β π) | ||
Theorem | cdlemg1cN 39762* | Any translation belongs to the set of functions constructed for cdleme 39735. TODO: Fix comment. (Contributed by NM, 18-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉ β π β πΉ = (β©π β π (πβπ) = π))) | ||
Theorem | cdlemg1cex 39763* | Any translation is one of our πΉ s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 39738? (Contributed by NM, 17-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ ((πΎ β HL β§ π β π») β (πΉ β π β βπ β π΄ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = (β©π β π (πβπ) = π)))) | ||
Theorem | cdlemg2cN 39764* | Any translation belongs to the set of functions constructed for cdleme 39735. TODO: Fix comment. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉβπ) = π) β (πΉ β π β πΉ = πΊ)) | ||
Theorem | cdlemg2dN 39765* | This theorem can be used to shorten πΊ = hypothesis. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ (πΉβπ) = π)) β πΉ = πΊ) | ||
Theorem | cdlemg2cex 39766* | Any translation is one of our πΉ s. TODO: fix comment, move to its own block maybe? Would this help for cdlemf 39738? (Contributed by NM, 22-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ ((πΎ β HL β§ π β π») β (πΉ β π β βπ β π΄ βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ π β§ πΉ = πΊ))) | ||
Theorem | cdlemg2ce 39767* | Utility theorem to eliminate p,q when converting theorems with explicit f. TODO: fix comment. (Contributed by NM, 22-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ (πΉ = πΊ β (π β π)) & β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ π) β π) β β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ π) β π) | ||
Theorem | cdlemg2jlemOLDN 39768* | Part of proof of Lemma E in [Crawley] p. 113. TODO: FIX COMMENT. f preserves join: f(r β¨ s) = f(r) β¨ s, p. 115 10th line from bottom. TODO: Combine with cdlemg2jOLDN 39773? (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (πΉβ(π β¨ π)) = ((πΉβπ) β¨ (πΉβπ))) | ||
Theorem | cdlemg2fvlem 39769* | Lemma for cdlemg2fv 39774. (Contributed by NM, 23-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΉ β π β§ (π β¨ (π β§ π)) = π)) β (πΉβπ) = ((πΉβπ) β¨ (π β§ π))) | ||
Theorem | cdlemg2klem 39770* | cdleme42keg 39661 with simpler hypotheses. TODO: FIX COMMENT. (Contributed by NM, 22-Apr-2013.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((π β¨ π) β§ π) & β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) & β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) & β’ πΊ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) | ||
Theorem | cdlemg2idN 39771 | Version of cdleme31id 39569 with simpler hypotheses. TODO: Fix comment. (Contributed by NM, 21-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π΅ = (BaseβπΎ) β β’ ((((πΎ β HL β§ π β π» β§ πΉ β π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((πΉβπ) = π β§ π β π΅) β§ π = π) β (πΉβπ) = π) | ||
Theorem | cdlemg3a 39772 | Part of proof of Lemma G in [Crawley] p. 116, line 19. Show p β¨ q = p β¨ u. TODO: reformat cdleme0cp 39389 to match this, then replace with cdleme0cp 39389. (Contributed by NM, 19-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β (π β¨ π) = (π β¨ π)) | ||
Theorem | cdlemg2jOLDN 39773 | TODO: Replace this with ltrnj 39307. (Contributed by NM, 22-Apr-2013.) (New usage is discouraged.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (πΉβ(π β¨ π)) = ((πΉβπ) β¨ (πΉβπ))) | ||
Theorem | cdlemg2fv 39774 | Value of a translation in terms of an associated atom. cdleme48fvg 39675 with simpler hypotheses. TODO: Use ltrnj 39307 to vastly simplify. (Contributed by NM, 23-Apr-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ β§ = (meetβπΎ) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΉ β π β§ (π β¨ (π β§ π)) = π)) β (πΉβπ) = ((πΉβπ) β¨ (π β§ π))) | ||
Theorem | cdlemg2fv2 39775 | Value of a translation in terms of an associated atom. TODO: FIX COMMENT. TODO: Is this useful elsewhere e.g. around cdlemeg46fjv 39698 that use more complex proofs? TODO: Use ltrnj 39307 to vastly simplify. (Contributed by NM, 23-Apr-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (πΉβ(π β¨ π)) = ((πΉβπ ) β¨ π)) | ||
Theorem | cdlemg2k 39776 | cdleme42keg 39661 with simpler hypotheses. TODO: FIX COMMENT. TODO: derive from cdlemg3a 39772, cdlemg2fv2 39775, cdlemg2jOLDN 39773, ltrnel 39314? (Contributed by NM, 22-Apr-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) | ||
Theorem | cdlemg2kq 39777 | cdlemg2k 39776 with π and π swapped. TODO: FIX COMMENT. (Contributed by NM, 15-May-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β ((πΉβπ) β¨ (πΉβπ)) = ((πΉβπ) β¨ π)) | ||
Theorem | cdlemg2l 39778 | TODO: FIX COMMENT. (Contributed by NM, 23-Apr-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ π)) | ||
Theorem | cdlemg2m 39779 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ β§ = (meetβπΎ) & β’ π = ((π β¨ π) β§ π) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΉ β π) β (((πΉβπ) β¨ (πΉβπ)) β§ π) = π) | ||
Theorem | cdlemg5 39780* | TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 39180? TODO: The β¨ hypothesis is unused. FIX COMMENT. (Contributed by NM, 26-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π΄ (π β π β§ Β¬ π β€ π)) | ||
Theorem | cdlemb3 39781* | Given two atoms not under the fiducial co-atom π, there is a third. Lemma B in [Crawley] p. 112. TODO: Is there a simpler more direct proof, that could be placed earlier e.g. near lhpexle 39180? Then replace cdlemb2 39216 with it. This is a more general version of cdlemb2 39216 without π β π condition. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β βπ β π΄ (Β¬ π β€ π β§ Β¬ π β€ (π β¨ π))) | ||
Theorem | cdlemg7fvbwN 39782 | Properties of a translation of an element not under π. TODO: Fix comment. Can this be simplified? Perhaps derived from cdleme48bw 39677? Done with a *ltrn* theorem? (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π΅ = (BaseβπΎ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ Β¬ π β€ π) β§ πΉ β π) β ((πΉβπ) β π΅ β§ Β¬ (πΉβπ) β€ π)) | ||
Theorem | cdlemg4a 39783 | TODO: FIX COMMENT If fg(p) = p, then tr f = tr g. (Contributed by NM, 23-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ πΉ β π β§ πΊ β π) β§ (πΉβ(πΊβπ)) = π) β (π βπΉ) = (π βπΊ)) | ||
Theorem | cdlemg4b1 39784 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ πΊ β π) β (π β¨ π) = (π β¨ (πΊβπ))) | ||
Theorem | cdlemg4b2 39785 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ πΊ β π) β ((πΊβπ) β¨ π) = (π β¨ (πΊβπ))) | ||
Theorem | cdlemg4b12 39786 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ πΊ β π) β ((πΊβπ) β¨ π) = (π β¨ π)) | ||
Theorem | cdlemg4c 39787 | TODO: FIX COMMENT. (Contributed by NM, 24-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΊ β π) β§ Β¬ π β€ (π β¨ π)) β Β¬ (πΊβπ) β€ (π β¨ π)) | ||
Theorem | cdlemg4d 39788 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β Β¬ (πΊβπ) β€ ((πΊβπ) β¨ (πΉβ(πΊβπ)))) | ||
Theorem | cdlemg4e 39789 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = (((πΊβπ) β¨ (π βπΉ)) β§ ((πΉβ(πΊβπ)) β¨ (((πΊβπ) β¨ (πΊβπ)) β§ π)))) | ||
Theorem | cdlemg4f 39790 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π)))) | ||
Theorem | cdlemg4g 39791 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) & β’ β§ = (meetβπΎ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = ((π β¨ π) β§ (π β¨ π))) | ||
Theorem | cdlemg4 39792 | TODO: FIX COMMENT. (Contributed by NM, 25-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = π) | ||
Theorem | cdlemg6a 39793* | TODO: FIX COMMENT. TODO: replace with cdlemg4 39792. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = π) | ||
Theorem | cdlemg6b 39794* | TODO: FIX COMMENT. TODO: replace with cdlemg4 39792. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ Β¬ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = π) | ||
Theorem | cdlemg6c 39795* | TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (((π β π΄ β§ Β¬ π β€ π) β§ Β¬ π β€ (π β¨ π)) β (πΉβ(πΊβπ)) = π)) | ||
Theorem | cdlemg6d 39796* | TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (((π β π΄ β§ Β¬ π β€ π) β§ Β¬ π β€ (π β¨ (πΊβπ))) β (πΉβ(πΊβπ)) = π)) | ||
Theorem | cdlemg6e 39797 | TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) & β’ π = ((trLβπΎ)βπ) & β’ β¨ = (joinβπΎ) & β’ π = (π βπΊ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ πΉ β π) β§ (πΊ β π β§ π β€ (π β¨ π) β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = π) | ||
Theorem | cdlemg6 39798 | TODO: FIX COMMENT. (Contributed by NM, 27-Apr-2013.) |
β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = π) | ||
Theorem | cdlemg7fvN 39799 | Value of a translation composition in terms of an associated atom. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ β¨ = (joinβπΎ) & β’ β§ = (meetβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (π β¨ (π β§ π)) = π)) β (πΉβ(πΊβπ)) = ((πΉβ(πΊβπ)) β¨ (π β§ π))) | ||
Theorem | cdlemg7aN 39800 | TODO: FIX COMMENT. (Contributed by NM, 28-Apr-2013.) (New usage is discouraged.) |
β’ π΅ = (BaseβπΎ) & β’ β€ = (leβπΎ) & β’ π΄ = (AtomsβπΎ) & β’ π» = (LHypβπΎ) & β’ π = ((LTrnβπΎ)βπ) β β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΅ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π β§ (πΉβ(πΊβπ)) = π)) β (πΉβ(πΊβπ)) = π) |
< Previous Next > |
Copyright terms: Public domain | < Previous Next > |