Step | Hyp | Ref
| Expression |
1 | | simp2lr 1241 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β Β¬ π β€ π) |
2 | | oveq1 7412 |
. . . . . . 7
β’ (π = π
β (π β¨ (π β§ π)) = (π
β¨ (π β§ π))) |
3 | | simpr 485 |
. . . . . . 7
β’ (((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π) β (π
β¨ (π β§ π)) = π) |
4 | 2, 3 | sylan9eqr 2794 |
. . . . . 6
β’ ((((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π) β§ π = π
) β (π β¨ (π β§ π)) = π) |
5 | | dihmeetlem3.b |
. . . . . . . 8
β’ π΅ = (BaseβπΎ) |
6 | | dihmeetlem3.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
7 | | simp11l 1284 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β πΎ β HL) |
8 | 7 | hllatd 38222 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β πΎ β Lat) |
9 | | simp2ll 1240 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β π΄) |
10 | | dihmeetlem3.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
11 | 5, 10 | atbase 38147 |
. . . . . . . . 9
β’ (π β π΄ β π β π΅) |
12 | 9, 11 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β π΅) |
13 | | simp12l 1286 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β π΅) |
14 | | simp12r 1287 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β π΅) |
15 | | dihmeetlem3.m |
. . . . . . . . . 10
β’ β§ =
(meetβπΎ) |
16 | 5, 15 | latmcl 18389 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
17 | 8, 13, 14, 16 | syl3anc 1371 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β (π β§ π) β π΅) |
18 | | simp11r 1285 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β π») |
19 | | dihmeetlem3.h |
. . . . . . . . . 10
β’ π» = (LHypβπΎ) |
20 | 5, 19 | lhpbase 38857 |
. . . . . . . . 9
β’ (π β π» β π β π΅) |
21 | 18, 20 | syl 17 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β π΅) |
22 | 5, 15 | latmcl 18389 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
23 | 8, 13, 21, 22 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β (π β§ π) β π΅) |
24 | | dihmeetlem3.j |
. . . . . . . . . . . 12
β’ β¨ =
(joinβπΎ) |
25 | 5, 6, 24 | latlej1 18397 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π β π΅ β§ (π β§ π) β π΅) β π β€ (π β¨ (π β§ π))) |
26 | 8, 12, 23, 25 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β€ (π β¨ (π β§ π))) |
27 | | simp2r 1200 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β (π β¨ (π β§ π)) = π) |
28 | 26, 27 | breqtrd 5173 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β€ π) |
29 | 5, 15 | latmcl 18389 |
. . . . . . . . . . . 12
β’ ((πΎ β Lat β§ π β π΅ β§ π β π΅) β (π β§ π) β π΅) |
30 | 8, 14, 21, 29 | syl3anc 1371 |
. . . . . . . . . . 11
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β (π β§ π) β π΅) |
31 | 5, 6, 24 | latlej1 18397 |
. . . . . . . . . . 11
β’ ((πΎ β Lat β§ π β π΅ β§ (π β§ π) β π΅) β π β€ (π β¨ (π β§ π))) |
32 | 8, 12, 30, 31 | syl3anc 1371 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β€ (π β¨ (π β§ π))) |
33 | | simp3 1138 |
. . . . . . . . . 10
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β (π β¨ (π β§ π)) = π) |
34 | 32, 33 | breqtrd 5173 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β€ π) |
35 | 5, 6, 15 | latlem12 18415 |
. . . . . . . . . 10
β’ ((πΎ β Lat β§ (π β π΅ β§ π β π΅ β§ π β π΅)) β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) |
36 | 8, 12, 13, 14, 35 | syl13anc 1372 |
. . . . . . . . 9
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β ((π β€ π β§ π β€ π) β π β€ (π β§ π))) |
37 | 28, 34, 36 | mpbi2and 710 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β€ (π β§ π)) |
38 | | simp13 1205 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β (π β§ π) β€ π) |
39 | 5, 6, 8, 12, 17, 21, 37, 38 | lattrd 18395 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ (π β¨ (π β§ π)) = π) β π β€ π) |
40 | 39 | 3exp 1119 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β (((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β ((π β¨ (π β§ π)) = π β π β€ π))) |
41 | 4, 40 | syl7 74 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β (((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β ((((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π) β§ π = π
) β π β€ π))) |
42 | 41 | exp4a 432 |
. . . 4
β’ (((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β (((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β (((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π) β (π = π
β π β€ π)))) |
43 | 42 | 3imp 1111 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (π = π
β π β€ π)) |
44 | 43 | necon3bd 2954 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β (Β¬ π β€ π β π β π
)) |
45 | 1, 44 | mpd 15 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΅ β§ π β π΅) β§ (π β§ π) β€ π) β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β¨ (π β§ π)) = π) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π
β¨ (π β§ π)) = π)) β π β π
) |