Step | Hyp | Ref
| Expression |
1 | | cdleme4.g |
. 2
β’ πΊ = ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π) β§ π))) |
2 | | simp11l 1285 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΎ β HL) |
3 | | simp12l 1287 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
4 | | simp13l 1289 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
5 | | eqid 2737 |
. . . . 5
β’
(BaseβπΎ) =
(BaseβπΎ) |
6 | | cdleme4.j |
. . . . 5
β’ β¨ =
(joinβπΎ) |
7 | | cdleme4.a |
. . . . 5
β’ π΄ = (AtomsβπΎ) |
8 | 5, 6, 7 | hlatjcl 37832 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
9 | 2, 3, 4, 8 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β (BaseβπΎ)) |
10 | | simp11 1204 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΎ β HL β§ π β π»)) |
11 | | simp12 1205 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
12 | | simp13 1206 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
13 | | simp2r 1201 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β π΄ β§ Β¬ π β€ π)) |
14 | | simp31 1210 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π) |
15 | | simp33 1212 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ π β€ (π β¨ π)) |
16 | | cdleme4.l |
. . . . . 6
β’ β€ =
(leβπΎ) |
17 | | cdleme4.m |
. . . . . 6
β’ β§ =
(meetβπΎ) |
18 | | cdleme4.h |
. . . . . 6
β’ π» = (LHypβπΎ) |
19 | | cdleme4.u |
. . . . . 6
β’ π = ((π β¨ π) β§ π) |
20 | | cdleme4.f |
. . . . . 6
β’ πΉ = ((π β¨ π) β§ (π β¨ ((π β¨ π) β§ π))) |
21 | 16, 6, 17, 7, 18, 19, 20 | cdleme3fa 38702 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) |
22 | 10, 11, 12, 13, 14, 15, 21 | syl132anc 1389 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΉ β π΄) |
23 | | simp2l 1200 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π
β π΄ β§ Β¬ π
β€ π)) |
24 | | simp2rl 1243 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
25 | | simp32 1211 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π
β€ (π β¨ π)) |
26 | | eqid 2737 |
. . . . . 6
β’ ((π
β¨ π) β§ π) = ((π
β¨ π) β§ π) |
27 | 16, 6, 17, 7, 18, 19, 20, 1, 26 | cdleme7b 38710 |
. . . . 5
β’ (((πΎ β HL β§ π β π») β§ (π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ (π β¨ π) β§ π
β€ (π β¨ π))) β ((π
β¨ π) β§ π) β π΄) |
28 | 10, 23, 24, 15, 25, 27 | syl113anc 1383 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π
β¨ π) β§ π) β π΄) |
29 | 5, 6, 7 | hlatjcl 37832 |
. . . 4
β’ ((πΎ β HL β§ πΉ β π΄ β§ ((π
β¨ π) β§ π) β π΄) β (πΉ β¨ ((π
β¨ π) β§ π)) β (BaseβπΎ)) |
30 | 2, 22, 28, 29 | syl3anc 1372 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (πΉ β¨ ((π
β¨ π) β§ π)) β (BaseβπΎ)) |
31 | 2 | hllatd 37829 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΎ β Lat) |
32 | | eqid 2737 |
. . . . 5
β’
(LinesβπΎ) =
(LinesβπΎ) |
33 | | eqid 2737 |
. . . . 5
β’
(pmapβπΎ) =
(pmapβπΎ) |
34 | 6, 7, 32, 33 | linepmap 38241 |
. . . 4
β’ (((πΎ β Lat β§ π β π΄ β§ π β π΄) β§ π β π) β ((pmapβπΎ)β(π β¨ π)) β (LinesβπΎ)) |
35 | 31, 3, 4, 14, 34 | syl31anc 1374 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((pmapβπΎ)β(π β¨ π)) β (LinesβπΎ)) |
36 | | simp2ll 1241 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π
β π΄) |
37 | 5, 6, 7 | hlatjcl 37832 |
. . . . . . 7
β’ ((πΎ β HL β§ π
β π΄ β§ π β π΄) β (π
β¨ π) β (BaseβπΎ)) |
38 | 2, 36, 24, 37 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π
β¨ π) β (BaseβπΎ)) |
39 | | simp11r 1286 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π») |
40 | 5, 18 | lhpbase 38464 |
. . . . . . 7
β’ (π β π» β π β (BaseβπΎ)) |
41 | 39, 40 | syl 17 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β (BaseβπΎ)) |
42 | 5, 16, 17 | latmle2 18355 |
. . . . . 6
β’ ((πΎ β Lat β§ (π
β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π
β¨ π) β§ π) β€ π) |
43 | 31, 38, 41, 42 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π
β¨ π) β§ π) β€ π) |
44 | 16, 6, 17, 7, 18, 19, 20 | cdleme3 38703 |
. . . . . 6
β’ (((πΎ β HL β§ π β π») β§ ((π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ Β¬ π β€ (π β¨ π))) β Β¬ πΉ β€ π) |
45 | 10, 11, 12, 13, 14, 15, 44 | syl132anc 1389 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ πΉ β€ π) |
46 | | nbrne2 5126 |
. . . . . 6
β’ ((((π
β¨ π) β§ π) β€ π β§ Β¬ πΉ β€ π) β ((π
β¨ π) β§ π) β πΉ) |
47 | 46 | necomd 3000 |
. . . . 5
β’ ((((π
β¨ π) β§ π) β€ π β§ Β¬ πΉ β€ π) β πΉ β ((π
β¨ π) β§ π)) |
48 | 43, 45, 47 | syl2anc 585 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΉ β ((π
β¨ π) β§ π)) |
49 | 6, 7, 32, 33 | linepmap 38241 |
. . . 4
β’ (((πΎ β Lat β§ πΉ β π΄ β§ ((π
β¨ π) β§ π) β π΄) β§ πΉ β ((π
β¨ π) β§ π)) β ((pmapβπΎ)β(πΉ β¨ ((π
β¨ π) β§ π))) β (LinesβπΎ)) |
50 | 31, 22, 28, 48, 49 | syl31anc 1374 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((pmapβπΎ)β(πΉ β¨ ((π
β¨ π) β§ π))) β (LinesβπΎ)) |
51 | 5, 7 | atbase 37754 |
. . . . . 6
β’ (πΉ β π΄ β πΉ β (BaseβπΎ)) |
52 | 22, 51 | syl 17 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΉ β (BaseβπΎ)) |
53 | 5, 17 | latmcl 18330 |
. . . . . 6
β’ ((πΎ β Lat β§ (π
β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π
β¨ π) β§ π) β (BaseβπΎ)) |
54 | 31, 38, 41, 53 | syl3anc 1372 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π
β¨ π) β§ π) β (BaseβπΎ)) |
55 | 5, 16, 6 | latlej2 18339 |
. . . . 5
β’ ((πΎ β Lat β§ πΉ β (BaseβπΎ) β§ ((π
β¨ π) β§ π) β (BaseβπΎ)) β ((π
β¨ π) β§ π) β€ (πΉ β¨ ((π
β¨ π) β§ π))) |
56 | 31, 52, 54, 55 | syl3anc 1372 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π
β¨ π) β§ π) β€ (πΉ β¨ ((π
β¨ π) β§ π))) |
57 | 16, 6, 17, 7, 18, 19, 20, 1, 26 | cdleme7c 38711 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ π β π΄) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β ((π
β¨ π) β§ π)) |
58 | 10, 11, 4, 23, 13, 14, 25, 15, 57 | syl323anc 1401 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β ((π
β¨ π) β§ π)) |
59 | 58 | necomd 3000 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π
β¨ π) β§ π) β π) |
60 | | hlatl 37825 |
. . . . . . . 8
β’ (πΎ β HL β πΎ β AtLat) |
61 | 2, 60 | syl 17 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΎ β AtLat) |
62 | 16, 6, 17, 7, 18, 19 | lhpat2 38511 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ π β π)) β π β π΄) |
63 | 10, 11, 4, 14, 62 | syl112anc 1375 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β π β π΄) |
64 | 16, 7 | atncmp 37777 |
. . . . . . 7
β’ ((πΎ β AtLat β§ ((π
β¨ π) β§ π) β π΄ β§ π β π΄) β (Β¬ ((π
β¨ π) β§ π) β€ π β ((π
β¨ π) β§ π) β π)) |
65 | 61, 28, 63, 64 | syl3anc 1372 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (Β¬ ((π
β¨ π) β§ π) β€ π β ((π
β¨ π) β§ π) β π)) |
66 | 59, 65 | mpbird 257 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ ((π
β¨ π) β§ π) β€ π) |
67 | 5, 16, 17 | latlem12 18356 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ (((π
β¨ π) β§ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((((π
β¨ π) β§ π) β€ (π β¨ π) β§ ((π
β¨ π) β§ π) β€ π) β ((π
β¨ π) β§ π) β€ ((π β¨ π) β§ π))) |
68 | 31, 54, 9, 41, 67 | syl13anc 1373 |
. . . . . . . 8
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((((π
β¨ π) β§ π) β€ (π β¨ π) β§ ((π
β¨ π) β§ π) β€ π) β ((π
β¨ π) β§ π) β€ ((π β¨ π) β§ π))) |
69 | 68 | biimpd 228 |
. . . . . . 7
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((((π
β¨ π) β§ π) β€ (π β¨ π) β§ ((π
β¨ π) β§ π) β€ π) β ((π
β¨ π) β§ π) β€ ((π β¨ π) β§ π))) |
70 | 43, 69 | mpan2d 693 |
. . . . . 6
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (((π
β¨ π) β§ π) β€ (π β¨ π) β ((π
β¨ π) β§ π) β€ ((π β¨ π) β§ π))) |
71 | 19 | breq2i 5114 |
. . . . . 6
β’ (((π
β¨ π) β§ π) β€ π β ((π
β¨ π) β§ π) β€ ((π β¨ π) β§ π)) |
72 | 70, 71 | syl6ibr 252 |
. . . . 5
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (((π
β¨ π) β§ π) β€ (π β¨ π) β ((π
β¨ π) β§ π) β€ π)) |
73 | 66, 72 | mtod 197 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β Β¬ ((π
β¨ π) β§ π) β€ (π β¨ π)) |
74 | | nbrne1 5125 |
. . . . 5
β’ ((((π
β¨ π) β§ π) β€ (πΉ β¨ ((π
β¨ π) β§ π)) β§ Β¬ ((π
β¨ π) β§ π) β€ (π β¨ π)) β (πΉ β¨ ((π
β¨ π) β§ π)) β (π β¨ π)) |
75 | 74 | necomd 3000 |
. . . 4
β’ ((((π
β¨ π) β§ π) β€ (πΉ β¨ ((π
β¨ π) β§ π)) β§ Β¬ ((π
β¨ π) β§ π) β€ (π β¨ π)) β (π β¨ π) β (πΉ β¨ ((π
β¨ π) β§ π))) |
76 | 56, 73, 75 | syl2anc 585 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β (π β¨ π) β (πΉ β¨ ((π
β¨ π) β§ π))) |
77 | 16, 6, 17, 7, 18, 19, 20, 1, 26 | cdleme7e 38713 |
. . . 4
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β (0.βπΎ)) |
78 | 1, 77 | eqnetrrid 3020 |
. . 3
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π) β§ π))) β (0.βπΎ)) |
79 | | eqid 2737 |
. . . 4
β’
(0.βπΎ) =
(0.βπΎ) |
80 | 5, 17, 79, 7, 32, 33 | 2lnat 38250 |
. . 3
β’ (((πΎ β HL β§ (π β¨ π) β (BaseβπΎ) β§ (πΉ β¨ ((π
β¨ π) β§ π)) β (BaseβπΎ)) β§ (((pmapβπΎ)β(π β¨ π)) β (LinesβπΎ) β§ ((pmapβπΎ)β(πΉ β¨ ((π
β¨ π) β§ π))) β (LinesβπΎ)) β§ ((π β¨ π) β (πΉ β¨ ((π
β¨ π) β§ π)) β§ ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π) β§ π))) β (0.βπΎ))) β ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π) β§ π))) β π΄) |
81 | 2, 9, 30, 35, 50, 76, 78, 80 | syl322anc 1399 |
. 2
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β ((π β¨ π) β§ (πΉ β¨ ((π
β¨ π) β§ π))) β π΄) |
82 | 1, 81 | eqeltrid 2842 |
1
β’ ((((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ ((π
β π΄ β§ Β¬ π
β€ π) β§ (π β π΄ β§ Β¬ π β€ π)) β§ (π β π β§ π
β€ (π β¨ π) β§ Β¬ π β€ (π β¨ π))) β πΊ β π΄) |