Step | Hyp | Ref
| Expression |
1 | | dalem38.y |
. 2
β’ π = ((π β¨ π) β¨ π
) |
2 | | dalem.ph |
. . . . . . 7
β’ (π β (((πΎ β HL β§ πΆ β (BaseβπΎ)) β§ (π β π΄ β§ π β π΄ β§ π
β π΄) β§ (π β π΄ β§ π β π΄ β§ π β π΄)) β§ (π β π β§ π β π) β§ ((Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π
) β§ Β¬ πΆ β€ (π
β¨ π)) β§ (Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π) β§ Β¬ πΆ β€ (π β¨ π)) β§ (πΆ β€ (π β¨ π) β§ πΆ β€ (π β¨ π) β§ πΆ β€ (π
β¨ π))))) |
3 | | dalem.l |
. . . . . . 7
β’ β€ =
(leβπΎ) |
4 | | dalem.j |
. . . . . . 7
β’ β¨ =
(joinβπΎ) |
5 | | dalem.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
6 | | dalem.ps |
. . . . . . 7
β’ (π β ((π β π΄ β§ π β π΄) β§ Β¬ π β€ π β§ (π β π β§ Β¬ π β€ π β§ πΆ β€ (π β¨ π)))) |
7 | | dalem38.m |
. . . . . . 7
β’ β§ =
(meetβπΎ) |
8 | | dalem38.o |
. . . . . . 7
β’ π = (LPlanesβπΎ) |
9 | | dalem38.z |
. . . . . . 7
β’ π = ((π β¨ π) β¨ π) |
10 | | dalem38.g |
. . . . . . 7
β’ πΊ = ((π β¨ π) β§ (π β¨ π)) |
11 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 10 | dalem28 39083 |
. . . . . 6
β’ ((π β§ π = π β§ π) β π β€ (πΊ β¨ π)) |
12 | | dalem38.h |
. . . . . . 7
β’ π» = ((π β¨ π) β§ (π β¨ π)) |
13 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 12 | dalem33 39088 |
. . . . . 6
β’ ((π β§ π = π β§ π) β π β€ (π» β¨ π)) |
14 | 2 | dalemkelat 39007 |
. . . . . . . 8
β’ (π β πΎ β Lat) |
15 | 14 | 3ad2ant1 1130 |
. . . . . . 7
β’ ((π β§ π = π β§ π) β πΎ β Lat) |
16 | 2, 5 | dalempeb 39022 |
. . . . . . . 8
β’ (π β π β (BaseβπΎ)) |
17 | 16 | 3ad2ant1 1130 |
. . . . . . 7
β’ ((π β§ π = π β§ π) β π β (BaseβπΎ)) |
18 | 2 | dalemkehl 39006 |
. . . . . . . . 9
β’ (π β πΎ β HL) |
19 | 18 | 3ad2ant1 1130 |
. . . . . . . 8
β’ ((π β§ π = π β§ π) β πΎ β HL) |
20 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 10 | dalem23 39079 |
. . . . . . . 8
β’ ((π β§ π = π β§ π) β πΊ β π΄) |
21 | 6 | dalemccea 39066 |
. . . . . . . . 9
β’ (π β π β π΄) |
22 | 21 | 3ad2ant3 1132 |
. . . . . . . 8
β’ ((π β§ π = π β§ π) β π β π΄) |
23 | | eqid 2726 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
24 | 23, 4, 5 | hlatjcl 38749 |
. . . . . . . 8
β’ ((πΎ β HL β§ πΊ β π΄ β§ π β π΄) β (πΊ β¨ π) β (BaseβπΎ)) |
25 | 19, 20, 22, 24 | syl3anc 1368 |
. . . . . . 7
β’ ((π β§ π = π β§ π) β (πΊ β¨ π) β (BaseβπΎ)) |
26 | 2, 5 | dalemqeb 39023 |
. . . . . . . 8
β’ (π β π β (BaseβπΎ)) |
27 | 26 | 3ad2ant1 1130 |
. . . . . . 7
β’ ((π β§ π = π β§ π) β π β (BaseβπΎ)) |
28 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 12 | dalem29 39084 |
. . . . . . . 8
β’ ((π β§ π = π β§ π) β π» β π΄) |
29 | 23, 4, 5 | hlatjcl 38749 |
. . . . . . . 8
β’ ((πΎ β HL β§ π» β π΄ β§ π β π΄) β (π» β¨ π) β (BaseβπΎ)) |
30 | 19, 28, 22, 29 | syl3anc 1368 |
. . . . . . 7
β’ ((π β§ π = π β§ π) β (π» β¨ π) β (BaseβπΎ)) |
31 | 23, 3, 4 | latjlej12 18417 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ (πΊ β¨ π) β (BaseβπΎ)) β§ (π β (BaseβπΎ) β§ (π» β¨ π) β (BaseβπΎ))) β ((π β€ (πΊ β¨ π) β§ π β€ (π» β¨ π)) β (π β¨ π) β€ ((πΊ β¨ π) β¨ (π» β¨ π)))) |
32 | 15, 17, 25, 27, 30, 31 | syl122anc 1376 |
. . . . . 6
β’ ((π β§ π = π β§ π) β ((π β€ (πΊ β¨ π) β§ π β€ (π» β¨ π)) β (π β¨ π) β€ ((πΊ β¨ π) β¨ (π» β¨ π)))) |
33 | 11, 13, 32 | mp2and 696 |
. . . . 5
β’ ((π β§ π = π β§ π) β (π β¨ π) β€ ((πΊ β¨ π) β¨ (π» β¨ π))) |
34 | 23, 5 | atbase 38671 |
. . . . . . 7
β’ (πΊ β π΄ β πΊ β (BaseβπΎ)) |
35 | 20, 34 | syl 17 |
. . . . . 6
β’ ((π β§ π = π β§ π) β πΊ β (BaseβπΎ)) |
36 | 23, 5 | atbase 38671 |
. . . . . . 7
β’ (π» β π΄ β π» β (BaseβπΎ)) |
37 | 28, 36 | syl 17 |
. . . . . 6
β’ ((π β§ π = π β§ π) β π» β (BaseβπΎ)) |
38 | 6, 5 | dalemcceb 39072 |
. . . . . . 7
β’ (π β π β (BaseβπΎ)) |
39 | 38 | 3ad2ant3 1132 |
. . . . . 6
β’ ((π β§ π = π β§ π) β π β (BaseβπΎ)) |
40 | 23, 4 | latjjdir 18454 |
. . . . . 6
β’ ((πΎ β Lat β§ (πΊ β (BaseβπΎ) β§ π» β (BaseβπΎ) β§ π β (BaseβπΎ))) β ((πΊ β¨ π») β¨ π) = ((πΊ β¨ π) β¨ (π» β¨ π))) |
41 | 15, 35, 37, 39, 40 | syl13anc 1369 |
. . . . 5
β’ ((π β§ π = π β§ π) β ((πΊ β¨ π») β¨ π) = ((πΊ β¨ π) β¨ (π» β¨ π))) |
42 | 33, 41 | breqtrrd 5169 |
. . . 4
β’ ((π β§ π = π β§ π) β (π β¨ π) β€ ((πΊ β¨ π») β¨ π)) |
43 | | dalem38.i |
. . . . 5
β’ πΌ = ((π β¨ π
) β§ (π β¨ π)) |
44 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 43 | dalem37 39092 |
. . . 4
β’ ((π β§ π = π β§ π) β π
β€ (πΌ β¨ π)) |
45 | 2, 4, 5 | dalempjqeb 39028 |
. . . . . 6
β’ (π β (π β¨ π) β (BaseβπΎ)) |
46 | 45 | 3ad2ant1 1130 |
. . . . 5
β’ ((π β§ π = π β§ π) β (π β¨ π) β (BaseβπΎ)) |
47 | 23, 4, 5 | hlatjcl 38749 |
. . . . . . 7
β’ ((πΎ β HL β§ πΊ β π΄ β§ π» β π΄) β (πΊ β¨ π») β (BaseβπΎ)) |
48 | 19, 20, 28, 47 | syl3anc 1368 |
. . . . . 6
β’ ((π β§ π = π β§ π) β (πΊ β¨ π») β (BaseβπΎ)) |
49 | 23, 4 | latjcl 18401 |
. . . . . 6
β’ ((πΎ β Lat β§ (πΊ β¨ π») β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((πΊ β¨ π») β¨ π) β (BaseβπΎ)) |
50 | 15, 48, 39, 49 | syl3anc 1368 |
. . . . 5
β’ ((π β§ π = π β§ π) β ((πΊ β¨ π») β¨ π) β (BaseβπΎ)) |
51 | 2, 5 | dalemreb 39024 |
. . . . . 6
β’ (π β π
β (BaseβπΎ)) |
52 | 51 | 3ad2ant1 1130 |
. . . . 5
β’ ((π β§ π = π β§ π) β π
β (BaseβπΎ)) |
53 | 2, 3, 4, 5, 6, 7, 8, 1, 9, 43 | dalem34 39089 |
. . . . . 6
β’ ((π β§ π = π β§ π) β πΌ β π΄) |
54 | 23, 4, 5 | hlatjcl 38749 |
. . . . . 6
β’ ((πΎ β HL β§ πΌ β π΄ β§ π β π΄) β (πΌ β¨ π) β (BaseβπΎ)) |
55 | 19, 53, 22, 54 | syl3anc 1368 |
. . . . 5
β’ ((π β§ π = π β§ π) β (πΌ β¨ π) β (BaseβπΎ)) |
56 | 23, 3, 4 | latjlej12 18417 |
. . . . 5
β’ ((πΎ β Lat β§ ((π β¨ π) β (BaseβπΎ) β§ ((πΊ β¨ π») β¨ π) β (BaseβπΎ)) β§ (π
β (BaseβπΎ) β§ (πΌ β¨ π) β (BaseβπΎ))) β (((π β¨ π) β€ ((πΊ β¨ π») β¨ π) β§ π
β€ (πΌ β¨ π)) β ((π β¨ π) β¨ π
) β€ (((πΊ β¨ π») β¨ π) β¨ (πΌ β¨ π)))) |
57 | 15, 46, 50, 52, 55, 56 | syl122anc 1376 |
. . . 4
β’ ((π β§ π = π β§ π) β (((π β¨ π) β€ ((πΊ β¨ π») β¨ π) β§ π
β€ (πΌ β¨ π)) β ((π β¨ π) β¨ π
) β€ (((πΊ β¨ π») β¨ π) β¨ (πΌ β¨ π)))) |
58 | 42, 44, 57 | mp2and 696 |
. . 3
β’ ((π β§ π = π β§ π) β ((π β¨ π) β¨ π
) β€ (((πΊ β¨ π») β¨ π) β¨ (πΌ β¨ π))) |
59 | 23, 5 | atbase 38671 |
. . . . 5
β’ (πΌ β π΄ β πΌ β (BaseβπΎ)) |
60 | 53, 59 | syl 17 |
. . . 4
β’ ((π β§ π = π β§ π) β πΌ β (BaseβπΎ)) |
61 | 23, 4 | latjjdir 18454 |
. . . 4
β’ ((πΎ β Lat β§ ((πΊ β¨ π») β (BaseβπΎ) β§ πΌ β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((πΊ β¨ π») β¨ πΌ) β¨ π) = (((πΊ β¨ π») β¨ π) β¨ (πΌ β¨ π))) |
62 | 15, 48, 60, 39, 61 | syl13anc 1369 |
. . 3
β’ ((π β§ π = π β§ π) β (((πΊ β¨ π») β¨ πΌ) β¨ π) = (((πΊ β¨ π») β¨ π) β¨ (πΌ β¨ π))) |
63 | 58, 62 | breqtrrd 5169 |
. 2
β’ ((π β§ π = π β§ π) β ((π β¨ π) β¨ π
) β€ (((πΊ β¨ π») β¨ πΌ) β¨ π)) |
64 | 1, 63 | eqbrtrid 5176 |
1
β’ ((π β§ π = π β§ π) β π β€ (((πΊ β¨ π») β¨ πΌ) β¨ π)) |