Mathbox for Norm Megill |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > Mathboxes > cdlemefs45ee | Structured version Visualization version GIF version |
Description: Explicit expansion of cdlemefs45 38482. TODO: use to shorten cdlemefs45 38482 uses? Should ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) be assigned to a hypothesis letter? TODO: FIX COMMENT. (Contributed by NM, 10-Apr-2013.) |
Ref | Expression |
---|---|
cdlemef45.b | β’ π΅ = (BaseβπΎ) |
cdlemef45.l | β’ β€ = (leβπΎ) |
cdlemef45.j | β’ β¨ = (joinβπΎ) |
cdlemef45.m | β’ β§ = (meetβπΎ) |
cdlemef45.a | β’ π΄ = (AtomsβπΎ) |
cdlemef45.h | β’ π» = (LHypβπΎ) |
cdlemef45.u | β’ π = ((π β¨ π) β§ π) |
cdlemef45.d | β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) |
cdlemef45.f | β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) |
cdlemefs45.e | β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) |
Ref | Expression |
---|---|
cdlemefs45ee | β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π)))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | cdlemef45.b | . . 3 β’ π΅ = (BaseβπΎ) | |
2 | cdlemef45.l | . . 3 β’ β€ = (leβπΎ) | |
3 | cdlemef45.j | . . 3 β’ β¨ = (joinβπΎ) | |
4 | cdlemef45.m | . . 3 β’ β§ = (meetβπΎ) | |
5 | cdlemef45.a | . . 3 β’ π΄ = (AtomsβπΎ) | |
6 | cdlemef45.h | . . 3 β’ π» = (LHypβπΎ) | |
7 | cdlemef45.u | . . 3 β’ π = ((π β¨ π) β§ π) | |
8 | cdlemef45.d | . . 3 β’ π· = ((π‘ β¨ π) β§ (π β¨ ((π β¨ π‘) β§ π))) | |
9 | cdlemef45.f | . . 3 β’ πΉ = (π₯ β π΅ β¦ if((π β π β§ Β¬ π₯ β€ π), (β©π§ β π΅ βπ β π΄ ((Β¬ π β€ π β§ (π β¨ (π₯ β§ π)) = π₯) β π§ = (if(π β€ (π β¨ π), (β©π¦ β π΅ βπ‘ β π΄ ((Β¬ π‘ β€ π β§ Β¬ π‘ β€ (π β¨ π)) β π¦ = πΈ)), β¦π / π‘β¦π·) β¨ (π₯ β§ π)))), π₯)) | |
10 | cdlemefs45.e | . . 3 β’ πΈ = ((π β¨ π) β§ (π· β¨ ((π β¨ π‘) β§ π))) | |
11 | 1, 2, 3, 4, 5, 6, 7, 8, 9, 10 | cdlemefs45 38482 | . 2 β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = β¦π / π β¦β¦π / π‘β¦πΈ) |
12 | simp22l 1292 | . . 3 β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) | |
13 | simp23l 1294 | . . 3 β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) | |
14 | eqid 2736 | . . . 4 β’ ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) | |
15 | eqid 2736 | . . . 4 β’ ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π))) = ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π))) | |
16 | 8, 10, 14, 15 | cdleme31sde 38438 | . . 3 β’ ((π β π΄ β§ π β π΄) β β¦π / π β¦β¦π / π‘β¦πΈ = ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π)))) |
17 | 12, 13, 16 | syl2anc 585 | . 2 β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β β¦π / π β¦β¦π / π‘β¦πΈ = ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π)))) |
18 | 11, 17 | eqtrd 2776 | 1 β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉβπ ) = ((π β¨ π) β§ (((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) β¨ ((π β¨ π) β§ π)))) |
Colors of variables: wff setvar class |
Syntax hints: Β¬ wn 3 β wi 4 β§ wa 397 β§ w3a 1087 = wceq 1539 β wcel 2104 β wne 2941 βwral 3062 β¦csb 3837 ifcif 4465 class class class wbr 5081 β¦ cmpt 5164 βcfv 6454 β©crio 7259 (class class class)co 7303 Basecbs 16953 lecple 17010 joincjn 18070 meetcmee 18071 Atomscatm 37316 HLchlt 37403 LHypclh 38037 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1795 ax-4 1809 ax-5 1911 ax-6 1969 ax-7 2009 ax-8 2106 ax-9 2114 ax-10 2135 ax-11 2152 ax-12 2169 ax-ext 2707 ax-rep 5218 ax-sep 5232 ax-nul 5239 ax-pow 5297 ax-pr 5361 ax-un 7616 ax-riotaBAD 37006 |
This theorem depends on definitions: df-bi 206 df-an 398 df-or 846 df-3or 1088 df-3an 1089 df-tru 1542 df-fal 1552 df-ex 1780 df-nf 1784 df-sb 2066 df-mo 2538 df-eu 2567 df-clab 2714 df-cleq 2728 df-clel 2814 df-nfc 2887 df-ne 2942 df-ral 3063 df-rex 3072 df-rmo 3285 df-reu 3286 df-rab 3287 df-v 3439 df-sbc 3722 df-csb 3838 df-dif 3895 df-un 3897 df-in 3899 df-ss 3909 df-nul 4263 df-if 4466 df-pw 4541 df-sn 4566 df-pr 4568 df-op 4572 df-uni 4845 df-iun 4933 df-iin 4934 df-br 5082 df-opab 5144 df-mpt 5165 df-id 5496 df-xp 5602 df-rel 5603 df-cnv 5604 df-co 5605 df-dm 5606 df-rn 5607 df-res 5608 df-ima 5609 df-iota 6406 df-fun 6456 df-fn 6457 df-f 6458 df-f1 6459 df-fo 6460 df-f1o 6461 df-fv 6462 df-riota 7260 df-ov 7306 df-oprab 7307 df-mpo 7308 df-1st 7859 df-2nd 7860 df-undef 8116 df-proset 18054 df-poset 18072 df-plt 18089 df-lub 18105 df-glb 18106 df-join 18107 df-meet 18108 df-p0 18184 df-p1 18185 df-lat 18191 df-clat 18258 df-oposet 37229 df-ol 37231 df-oml 37232 df-covers 37319 df-ats 37320 df-atl 37351 df-cvlat 37375 df-hlat 37404 df-llines 37551 df-lplanes 37552 df-lvols 37553 df-lines 37554 df-psubsp 37556 df-pmap 37557 df-padd 37849 df-lhyp 38041 |
This theorem is referenced by: cdlemefs45eN 38484 cdleme50trn2a 38603 |
Copyright terms: Public domain | W3C validator |