Step | Hyp | Ref
| Expression |
1 | | cdlemg2inv.h |
. . . . 5
β’ π» = (LHypβπΎ) |
2 | | cdlemg2inv.t |
. . . . 5
β’ π = ((LTrnβπΎ)βπ) |
3 | | cdlemg2j.l |
. . . . 5
β’ β€ =
(leβπΎ) |
4 | | cdlemg2j.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
5 | | cdlemg2j.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
6 | | cdlemg2j.m |
. . . . 5
β’ β§ =
(meetβπΎ) |
7 | | cdlemg2j.u |
. . . . 5
β’ π = ((π β¨ π) β§ π) |
8 | 1, 2, 3, 4, 5, 6, 7 | cdlemg2k 39775 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ πΊ β π) β ((πΊβπ) β¨ (πΊβπ)) = ((πΊβπ) β¨ π)) |
9 | 8 | 3adant3l 1180 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((πΊβπ) β¨ (πΊβπ)) = ((πΊβπ) β¨ π)) |
10 | 9 | fveq2d 6895 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΉβ((πΊβπ) β¨ (πΊβπ))) = (πΉβ((πΊβπ) β¨ π))) |
11 | | simp1 1136 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΎ β HL β§ π β π»)) |
12 | | simp3l 1201 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β πΉ β π) |
13 | | simp3r 1202 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β πΊ β π) |
14 | | simp2l 1199 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (π β π΄ β§ Β¬ π β€ π)) |
15 | 3, 5, 1, 2 | ltrnel 39313 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
16 | 11, 13, 14, 15 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
17 | 16 | simpld 495 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ) β π΄) |
18 | | eqid 2732 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
19 | 18, 5 | atbase 38462 |
. . . 4
β’ ((πΊβπ) β π΄ β (πΊβπ) β (BaseβπΎ)) |
20 | 17, 19 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ) β (BaseβπΎ)) |
21 | | simp2r 1200 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (π β π΄ β§ Β¬ π β€ π)) |
22 | 3, 5, 1, 2 | ltrnel 39313 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
23 | 11, 13, 21, 22 | syl3anc 1371 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) |
24 | 23 | simpld 495 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ) β π΄) |
25 | 18, 5 | atbase 38462 |
. . . 4
β’ ((πΊβπ) β π΄ β (πΊβπ) β (BaseβπΎ)) |
26 | 24, 25 | syl 17 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΊβπ) β (BaseβπΎ)) |
27 | 18, 4, 1, 2 | ltrnj 39306 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ ((πΊβπ) β (BaseβπΎ) β§ (πΊβπ) β (BaseβπΎ))) β (πΉβ((πΊβπ) β¨ (πΊβπ))) = ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
28 | 11, 12, 20, 26, 27 | syl112anc 1374 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΉβ((πΊβπ) β¨ (πΊβπ))) = ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ)))) |
29 | 1, 2, 3, 4, 5, 6, 7 | cdlemg2fv2 39774 |
. . 3
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ ((πΊβπ) β π΄ β§ Β¬ (πΊβπ) β€ π)) β§ πΉ β π) β (πΉβ((πΊβπ) β¨ π)) = ((πΉβ(πΊβπ)) β¨ π)) |
30 | 11, 14, 21, 16, 12, 29 | syl131anc 1383 |
. 2
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β (πΉβ((πΊβπ) β¨ π)) = ((πΉβ(πΊβπ)) β¨ π)) |
31 | 10, 28, 30 | 3eqtr3d 2780 |
1
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (πΉ β π β§ πΊ β π)) β ((πΉβ(πΊβπ)) β¨ (πΉβ(πΊβπ))) = ((πΉβ(πΊβπ)) β¨ π)) |