Step | Hyp | Ref
| Expression |
1 | | simprlr 779 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β Β¬ π β€ π) |
2 | | simpl1l 1225 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β πΎ β HL) |
3 | 2 | hllatd 37876 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β πΎ β Lat) |
4 | | simpl2 1193 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΅) |
5 | | simpl3 1194 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΅) |
6 | | dihmeetlem6.b |
. . . . . . 7
β’ π΅ = (BaseβπΎ) |
7 | | dihmeetlem6.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
8 | 6, 7 | latmcl 18337 |
. . . . . 6
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
9 | 3, 4, 5, 8 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (π β§ π) β π΅) |
10 | | simprll 778 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΄) |
11 | | dihmeetlem6.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
12 | 6, 11 | atbase 37801 |
. . . . . 6
β’ (π β π΄ β π β π΅) |
13 | 10, 12 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΅) |
14 | | simpl1r 1226 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π») |
15 | | dihmeetlem6.h |
. . . . . . 7
β’ π» = (LHypβπΎ) |
16 | 6, 15 | lhpbase 38511 |
. . . . . 6
β’ (π β π» β π β π΅) |
17 | 14, 16 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β π΅) |
18 | | dihmeetlem6.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
19 | | dihmeetlem6.j |
. . . . . 6
β’ β¨ =
(joinβπΎ) |
20 | 6, 18, 19 | latjle12 18347 |
. . . . 5
β’ ((πΎ β Lat β§ ((π β§ π) β π΅ β§ π β π΅ β§ π β π΅)) β (((π β§ π) β€ π β§ π β€ π) β ((π β§ π) β¨ π) β€ π)) |
21 | 3, 9, 13, 17, 20 | syl13anc 1373 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (((π β§ π) β€ π β§ π β€ π) β ((π β§ π) β¨ π) β€ π)) |
22 | | simpr 486 |
. . . 4
β’ (((π β§ π) β€ π β§ π β€ π) β π β€ π) |
23 | 21, 22 | syl6bir 254 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (((π β§ π) β¨ π) β€ π β π β€ π)) |
24 | 1, 23 | mtod 197 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β Β¬ ((π β§ π) β¨ π) β€ π) |
25 | | simprr 772 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β π β€ π) |
26 | 6, 18, 19, 7, 11 | dihmeetlem5 39821 |
. . . 4
β’ (((πΎ β HL β§ π β π΅ β§ π β π΅) β§ (π β π΄ β§ π β€ π)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ π)) |
27 | 2, 4, 5, 10, 25, 26 | syl32anc 1379 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β (π β§ (π β¨ π)) = ((π β§ π) β¨ π)) |
28 | 27 | breq1d 5119 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β ((π β§ (π β¨ π)) β€ π β ((π β§ π) β¨ π) β€ π)) |
29 | 24, 28 | mtbird 325 |
1
β’ ((((πΎ β HL β§ π β π») β§ π β π΅ β§ π β π΅) β§ ((π β π΄ β§ Β¬ π β€ π) β§ π β€ π)) β Β¬ (π β§ (π β¨ π)) β€ π) |