Step | Hyp | Ref
| Expression |
1 | | dihmeetlem9.b |
. . . 4
β’ π΅ = (BaseβπΎ) |
2 | | dihmeetlem9.l |
. . . 4
β’ β€ =
(leβπΎ) |
3 | | dihmeetlem9.h |
. . . 4
β’ π» = (LHypβπΎ) |
4 | | dihmeetlem9.j |
. . . 4
β’ β¨ =
(joinβπΎ) |
5 | | dihmeetlem9.m |
. . . 4
β’ β§ =
(meetβπΎ) |
6 | | dihmeetlem9.a |
. . . 4
β’ π΄ = (AtomsβπΎ) |
7 | | dihmeetlem9.u |
. . . 4
β’ π = ((DVecHβπΎ)βπ) |
8 | | dihmeetlem9.s |
. . . 4
β’ β =
(LSSumβπ) |
9 | | dihmeetlem9.i |
. . . 4
β’ πΌ = ((DIsoHβπΎ)βπ) |
10 | 1, 2, 3, 4, 5, 6, 7, 8, 9 | dihmeetlem10N 39825 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (πΌβ((π β§ π) β¨ π)) = ((πΌβπ) β© (πΌβ(π β¨ π)))) |
11 | 10 | ineq1d 4172 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((πΌβ((π β§ π) β¨ π)) β© (πΌβπ)) = (((πΌβπ) β© (πΌβ(π β¨ π))) β© (πΌβπ))) |
12 | | inass 4180 |
. . 3
β’ (((πΌβπ) β© (πΌβ(π β¨ π))) β© (πΌβπ)) = ((πΌβπ) β© ((πΌβ(π β¨ π)) β© (πΌβπ))) |
13 | | simpl1l 1225 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β πΎ β HL) |
14 | 13 | hllatd 37872 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β πΎ β Lat) |
15 | | simpl3 1194 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΅) |
16 | | simprll 778 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΄) |
17 | 1, 6 | atbase 37797 |
. . . . . . . 8
β’ (π β π΄ β π β π΅) |
18 | 16, 17 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΅) |
19 | 1, 2, 4 | latlej1 18342 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β π β€ (π β¨ π)) |
20 | 14, 15, 18, 19 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β€ (π β¨ π)) |
21 | | simpl1 1192 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (πΎ β HL β§ π β π»)) |
22 | 1, 4 | latjcl 18333 |
. . . . . . . 8
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β¨ π) β π΅) |
23 | 14, 15, 18, 22 | syl3anc 1372 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (π β¨ π) β π΅) |
24 | 1, 2, 3, 9 | dihord 39773 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ π β π΅ β§ (π β¨ π) β π΅) β ((πΌβπ) β (πΌβ(π β¨ π)) β π β€ (π β¨ π))) |
25 | 21, 15, 23, 24 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((πΌβπ) β (πΌβ(π β¨ π)) β π β€ (π β¨ π))) |
26 | 20, 25 | mpbird 257 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (πΌβπ) β (πΌβ(π β¨ π))) |
27 | | sseqin2 4176 |
. . . . 5
β’ ((πΌβπ) β (πΌβ(π β¨ π)) β ((πΌβ(π β¨ π)) β© (πΌβπ)) = (πΌβπ)) |
28 | 26, 27 | sylib 217 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((πΌβ(π β¨ π)) β© (πΌβπ)) = (πΌβπ)) |
29 | 28 | ineq2d 4173 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((πΌβπ) β© ((πΌβ(π β¨ π)) β© (πΌβπ))) = ((πΌβπ) β© (πΌβπ))) |
30 | 12, 29 | eqtrid 2785 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (((πΌβπ) β© (πΌβ(π β¨ π))) β© (πΌβπ)) = ((πΌβπ) β© (πΌβπ))) |
31 | 11, 30 | eqtrd 2773 |
1
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((πΌβ((π β§ π) β¨ π)) β© (πΌβπ)) = ((πΌβπ) β© (πΌβπ))) |