Step | Hyp | Ref
| Expression |
1 | | dia2dimlem2.k |
. . . . . . . . 9
β’ (π β (πΎ β HL β§ π β π»)) |
2 | 1 | simpld 496 |
. . . . . . . 8
β’ (π β πΎ β HL) |
3 | 2 | hllatd 37829 |
. . . . . . 7
β’ (π β πΎ β Lat) |
4 | | dia2dimlem2.p |
. . . . . . . . 9
β’ (π β (π β π΄ β§ Β¬ π β€ π)) |
5 | 4 | simpld 496 |
. . . . . . . 8
β’ (π β π β π΄) |
6 | | eqid 2737 |
. . . . . . . . 9
β’
(BaseβπΎ) =
(BaseβπΎ) |
7 | | dia2dimlem2.a |
. . . . . . . . 9
β’ π΄ = (AtomsβπΎ) |
8 | 6, 7 | atbase 37754 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
9 | 5, 8 | syl 17 |
. . . . . . 7
β’ (π β π β (BaseβπΎ)) |
10 | | dia2dimlem2.u |
. . . . . . . . 9
β’ (π β (π β π΄ β§ π β€ π)) |
11 | 10 | simpld 496 |
. . . . . . . 8
β’ (π β π β π΄) |
12 | 6, 7 | atbase 37754 |
. . . . . . . 8
β’ (π β π΄ β π β (BaseβπΎ)) |
13 | 11, 12 | syl 17 |
. . . . . . 7
β’ (π β π β (BaseβπΎ)) |
14 | | dia2dimlem2.l |
. . . . . . . 8
β’ β€ =
(leβπΎ) |
15 | | dia2dimlem2.j |
. . . . . . . 8
β’ β¨ =
(joinβπΎ) |
16 | 6, 14, 15 | latlej2 18339 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ π β (BaseβπΎ)) β π β€ (π β¨ π)) |
17 | 3, 9, 13, 16 | syl3anc 1372 |
. . . . . 6
β’ (π β π β€ (π β¨ π)) |
18 | 6, 15, 7 | hlatjcl 37832 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π β¨ π) β (BaseβπΎ)) |
19 | 2, 5, 11, 18 | syl3anc 1372 |
. . . . . . 7
β’ (π β (π β¨ π) β (BaseβπΎ)) |
20 | | dia2dimlem2.m |
. . . . . . . 8
β’ β§ =
(meetβπΎ) |
21 | 6, 14, 20 | latleeqm2 18358 |
. . . . . . 7
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ)) β (π β€ (π β¨ π) β ((π β¨ π) β§ π) = π)) |
22 | 3, 13, 19, 21 | syl3anc 1372 |
. . . . . 6
β’ (π β (π β€ (π β¨ π) β ((π β¨ π) β§ π) = π)) |
23 | 17, 22 | mpbid 231 |
. . . . 5
β’ (π β ((π β¨ π) β§ π) = π) |
24 | | dia2dimlem2.rf |
. . . . . . . 8
β’ (π β (π
βπΉ) β€ (π β¨ π)) |
25 | | dia2dimlem2.f |
. . . . . . . . . 10
β’ (π β (πΉ β π β§ (πΉβπ) β π)) |
26 | | dia2dimlem2.h |
. . . . . . . . . . 11
β’ π» = (LHypβπΎ) |
27 | | dia2dimlem2.t |
. . . . . . . . . . 11
β’ π = ((LTrnβπΎ)βπ) |
28 | | dia2dimlem2.r |
. . . . . . . . . . 11
β’ π
= ((trLβπΎ)βπ) |
29 | 14, 7, 26, 27, 28 | trlat 38635 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ (π β π΄ β§ Β¬ π β€ π) β§ (πΉ β π β§ (πΉβπ) β π)) β (π
βπΉ) β π΄) |
30 | 1, 4, 25, 29 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π
βπΉ) β π΄) |
31 | | dia2dimlem2.v |
. . . . . . . . . 10
β’ (π β (π β π΄ β§ π β€ π)) |
32 | 31 | simpld 496 |
. . . . . . . . 9
β’ (π β π β π΄) |
33 | | dia2dimlem2.rv |
. . . . . . . . 9
β’ (π β (π
βπΉ) β π) |
34 | 14, 15, 7 | hlatexch2 37862 |
. . . . . . . . 9
β’ ((πΎ β HL β§ ((π
βπΉ) β π΄ β§ π β π΄ β§ π β π΄) β§ (π
βπΉ) β π) β ((π
βπΉ) β€ (π β¨ π) β π β€ ((π
βπΉ) β¨ π))) |
35 | 2, 30, 11, 32, 33, 34 | syl131anc 1384 |
. . . . . . . 8
β’ (π β ((π
βπΉ) β€ (π β¨ π) β π β€ ((π
βπΉ) β¨ π))) |
36 | 24, 35 | mpd 15 |
. . . . . . 7
β’ (π β π β€ ((π
βπΉ) β¨ π)) |
37 | 25 | simpld 496 |
. . . . . . . . . 10
β’ (π β πΉ β π) |
38 | 14, 15, 20, 7, 26, 27, 28 | trlval2 38629 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
39 | 1, 37, 4, 38 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β (π
βπΉ) = ((π β¨ (πΉβπ)) β§ π)) |
40 | 39 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π
βπΉ) β¨ π) = (((π β¨ (πΉβπ)) β§ π) β¨ π)) |
41 | 14, 7, 26, 27 | ltrnel 38605 |
. . . . . . . . . . . . 13
β’ (((πΎ β HL β§ π β π») β§ πΉ β π β§ (π β π΄ β§ Β¬ π β€ π)) β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
42 | 1, 37, 4, 41 | syl3anc 1372 |
. . . . . . . . . . . 12
β’ (π β ((πΉβπ) β π΄ β§ Β¬ (πΉβπ) β€ π)) |
43 | 42 | simpld 496 |
. . . . . . . . . . 11
β’ (π β (πΉβπ) β π΄) |
44 | 6, 15, 7 | hlatjcl 37832 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΄ β§ (πΉβπ) β π΄) β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
45 | 2, 5, 43, 44 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β (π β¨ (πΉβπ)) β (BaseβπΎ)) |
46 | 1 | simprd 497 |
. . . . . . . . . . 11
β’ (π β π β π») |
47 | 6, 26 | lhpbase 38464 |
. . . . . . . . . . 11
β’ (π β π» β π β (BaseβπΎ)) |
48 | 46, 47 | syl 17 |
. . . . . . . . . 10
β’ (π β π β (BaseβπΎ)) |
49 | 31 | simprd 497 |
. . . . . . . . . 10
β’ (π β π β€ π) |
50 | 6, 14, 15, 20, 7 | atmod4i1 38332 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ (πΉβπ)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β§ π β€ π) β (((π β¨ (πΉβπ)) β§ π) β¨ π) = (((π β¨ (πΉβπ)) β¨ π) β§ π)) |
51 | 2, 32, 45, 48, 49, 50 | syl131anc 1384 |
. . . . . . . . 9
β’ (π β (((π β¨ (πΉβπ)) β§ π) β¨ π) = (((π β¨ (πΉβπ)) β¨ π) β§ π)) |
52 | 15, 7 | hlatjass 37835 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π β π΄ β§ (πΉβπ) β π΄ β§ π β π΄)) β ((π β¨ (πΉβπ)) β¨ π) = (π β¨ ((πΉβπ) β¨ π))) |
53 | 2, 5, 43, 32, 52 | syl13anc 1373 |
. . . . . . . . . 10
β’ (π β ((π β¨ (πΉβπ)) β¨ π) = (π β¨ ((πΉβπ) β¨ π))) |
54 | 53 | oveq1d 7373 |
. . . . . . . . 9
β’ (π β (((π β¨ (πΉβπ)) β¨ π) β§ π) = ((π β¨ ((πΉβπ) β¨ π)) β§ π)) |
55 | 51, 54 | eqtrd 2777 |
. . . . . . . 8
β’ (π β (((π β¨ (πΉβπ)) β§ π) β¨ π) = ((π β¨ ((πΉβπ) β¨ π)) β§ π)) |
56 | 40, 55 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((π
βπΉ) β¨ π) = ((π β¨ ((πΉβπ) β¨ π)) β§ π)) |
57 | 36, 56 | breqtrd 5132 |
. . . . . 6
β’ (π β π β€ ((π β¨ ((πΉβπ) β¨ π)) β§ π)) |
58 | 6, 15, 7 | hlatjcl 37832 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (πΉβπ) β π΄ β§ π β π΄) β ((πΉβπ) β¨ π) β (BaseβπΎ)) |
59 | 2, 43, 32, 58 | syl3anc 1372 |
. . . . . . . . 9
β’ (π β ((πΉβπ) β¨ π) β (BaseβπΎ)) |
60 | 6, 15 | latjcl 18329 |
. . . . . . . . 9
β’ ((πΎ β Lat β§ π β (BaseβπΎ) β§ ((πΉβπ) β¨ π) β (BaseβπΎ)) β (π β¨ ((πΉβπ) β¨ π)) β (BaseβπΎ)) |
61 | 3, 9, 59, 60 | syl3anc 1372 |
. . . . . . . 8
β’ (π β (π β¨ ((πΉβπ) β¨ π)) β (BaseβπΎ)) |
62 | 6, 20 | latmcl 18330 |
. . . . . . . 8
β’ ((πΎ β Lat β§ (π β¨ ((πΉβπ) β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ)) β ((π β¨ ((πΉβπ) β¨ π)) β§ π) β (BaseβπΎ)) |
63 | 3, 61, 48, 62 | syl3anc 1372 |
. . . . . . 7
β’ (π β ((π β¨ ((πΉβπ) β¨ π)) β§ π) β (BaseβπΎ)) |
64 | 6, 14, 20 | latmlem2 18360 |
. . . . . . 7
β’ ((πΎ β Lat β§ (π β (BaseβπΎ) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π) β (BaseβπΎ) β§ (π β¨ π) β (BaseβπΎ))) β (π β€ ((π β¨ ((πΉβπ) β¨ π)) β§ π) β ((π β¨ π) β§ π) β€ ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π)))) |
65 | 3, 13, 63, 19, 64 | syl13anc 1373 |
. . . . . 6
β’ (π β (π β€ ((π β¨ ((πΉβπ) β¨ π)) β§ π) β ((π β¨ π) β§ π) β€ ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π)))) |
66 | 57, 65 | mpd 15 |
. . . . 5
β’ (π β ((π β¨ π) β§ π) β€ ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
67 | 23, 66 | eqbrtrrd 5130 |
. . . 4
β’ (π β π β€ ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
68 | | dia2dimlem2.g |
. . . . . . 7
β’ (π β πΊ β π) |
69 | 14, 15, 20, 7, 26, 27, 28 | trlval2 38629 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π») β§ πΊ β π β§ (π β π΄ β§ Β¬ π β€ π)) β (π
βπΊ) = ((π β¨ (πΊβπ)) β§ π)) |
70 | 1, 68, 4, 69 | syl3anc 1372 |
. . . . . 6
β’ (π β (π
βπΊ) = ((π β¨ (πΊβπ)) β§ π)) |
71 | | dia2dimlem2.gv |
. . . . . . . . . 10
β’ (π β (πΊβπ) = π) |
72 | | dia2dimlem2.q |
. . . . . . . . . 10
β’ π = ((π β¨ π) β§ ((πΉβπ) β¨ π)) |
73 | 71, 72 | eqtrdi 2793 |
. . . . . . . . 9
β’ (π β (πΊβπ) = ((π β¨ π) β§ ((πΉβπ) β¨ π))) |
74 | 73 | oveq2d 7374 |
. . . . . . . 8
β’ (π β (π β¨ (πΊβπ)) = (π β¨ ((π β¨ π) β§ ((πΉβπ) β¨ π)))) |
75 | 74 | oveq1d 7373 |
. . . . . . 7
β’ (π β ((π β¨ (πΊβπ)) β§ π) = ((π β¨ ((π β¨ π) β§ ((πΉβπ) β¨ π))) β§ π)) |
76 | 14, 15, 7 | hlatlej1 37840 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β π β€ (π β¨ π)) |
77 | 2, 5, 11, 76 | syl3anc 1372 |
. . . . . . . . . 10
β’ (π β π β€ (π β¨ π)) |
78 | 6, 14, 15, 20, 7 | atmod3i1 38330 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ (π β π΄ β§ (π β¨ π) β (BaseβπΎ) β§ ((πΉβπ) β¨ π) β (BaseβπΎ)) β§ π β€ (π β¨ π)) β (π β¨ ((π β¨ π) β§ ((πΉβπ) β¨ π))) = ((π β¨ π) β§ (π β¨ ((πΉβπ) β¨ π)))) |
79 | 2, 5, 19, 59, 77, 78 | syl131anc 1384 |
. . . . . . . . 9
β’ (π β (π β¨ ((π β¨ π) β§ ((πΉβπ) β¨ π))) = ((π β¨ π) β§ (π β¨ ((πΉβπ) β¨ π)))) |
80 | 79 | oveq1d 7373 |
. . . . . . . 8
β’ (π β ((π β¨ ((π β¨ π) β§ ((πΉβπ) β¨ π))) β§ π) = (((π β¨ π) β§ (π β¨ ((πΉβπ) β¨ π))) β§ π)) |
81 | | hlol 37826 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OL) |
82 | 2, 81 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ β OL) |
83 | 6, 20 | latmassOLD 37694 |
. . . . . . . . 9
β’ ((πΎ β OL β§ ((π β¨ π) β (BaseβπΎ) β§ (π β¨ ((πΉβπ) β¨ π)) β (BaseβπΎ) β§ π β (BaseβπΎ))) β (((π β¨ π) β§ (π β¨ ((πΉβπ) β¨ π))) β§ π) = ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
84 | 82, 19, 61, 48, 83 | syl13anc 1373 |
. . . . . . . 8
β’ (π β (((π β¨ π) β§ (π β¨ ((πΉβπ) β¨ π))) β§ π) = ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
85 | 80, 84 | eqtrd 2777 |
. . . . . . 7
β’ (π β ((π β¨ ((π β¨ π) β§ ((πΉβπ) β¨ π))) β§ π) = ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
86 | 75, 85 | eqtrd 2777 |
. . . . . 6
β’ (π β ((π β¨ (πΊβπ)) β§ π) = ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
87 | 70, 86 | eqtrd 2777 |
. . . . 5
β’ (π β (π
βπΊ) = ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π))) |
88 | 87 | eqcomd 2743 |
. . . 4
β’ (π β ((π β¨ π) β§ ((π β¨ ((πΉβπ) β¨ π)) β§ π)) = (π
βπΊ)) |
89 | 67, 88 | breqtrd 5132 |
. . 3
β’ (π β π β€ (π
βπΊ)) |
90 | | hlatl 37825 |
. . . . 5
β’ (πΎ β HL β πΎ β AtLat) |
91 | 2, 90 | syl 17 |
. . . 4
β’ (π β πΎ β AtLat) |
92 | | hlop 37827 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β OP) |
93 | 2, 92 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ β OP) |
94 | | eqid 2737 |
. . . . . . . . . 10
β’
(0.βπΎ) =
(0.βπΎ) |
95 | | eqid 2737 |
. . . . . . . . . 10
β’
(ltβπΎ) =
(ltβπΎ) |
96 | 94, 95, 7 | 0ltat 37756 |
. . . . . . . . 9
β’ ((πΎ β OP β§ π β π΄) β (0.βπΎ)(ltβπΎ)π) |
97 | 93, 11, 96 | syl2anc 585 |
. . . . . . . 8
β’ (π β (0.βπΎ)(ltβπΎ)π) |
98 | | hlpos 37831 |
. . . . . . . . . 10
β’ (πΎ β HL β πΎ β Poset) |
99 | 2, 98 | syl 17 |
. . . . . . . . 9
β’ (π β πΎ β Poset) |
100 | 6, 94 | op0cl 37649 |
. . . . . . . . . 10
β’ (πΎ β OP β
(0.βπΎ) β
(BaseβπΎ)) |
101 | 93, 100 | syl 17 |
. . . . . . . . 9
β’ (π β (0.βπΎ) β (BaseβπΎ)) |
102 | 6, 26, 27, 28 | trlcl 38630 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β (π
βπΊ) β (BaseβπΎ)) |
103 | 1, 68, 102 | syl2anc 585 |
. . . . . . . . 9
β’ (π β (π
βπΊ) β (BaseβπΎ)) |
104 | 6, 14, 95 | pltletr 18233 |
. . . . . . . . 9
β’ ((πΎ β Poset β§
((0.βπΎ) β
(BaseβπΎ) β§ π β (BaseβπΎ) β§ (π
βπΊ) β (BaseβπΎ))) β (((0.βπΎ)(ltβπΎ)π β§ π β€ (π
βπΊ)) β (0.βπΎ)(ltβπΎ)(π
βπΊ))) |
105 | 99, 101, 13, 103, 104 | syl13anc 1373 |
. . . . . . . 8
β’ (π β (((0.βπΎ)(ltβπΎ)π β§ π β€ (π
βπΊ)) β (0.βπΎ)(ltβπΎ)(π
βπΊ))) |
106 | 97, 89, 105 | mp2and 698 |
. . . . . . 7
β’ (π β (0.βπΎ)(ltβπΎ)(π
βπΊ)) |
107 | 6, 95, 94 | opltn0 37655 |
. . . . . . . 8
β’ ((πΎ β OP β§ (π
βπΊ) β (BaseβπΎ)) β ((0.βπΎ)(ltβπΎ)(π
βπΊ) β (π
βπΊ) β (0.βπΎ))) |
108 | 93, 103, 107 | syl2anc 585 |
. . . . . . 7
β’ (π β ((0.βπΎ)(ltβπΎ)(π
βπΊ) β (π
βπΊ) β (0.βπΎ))) |
109 | 106, 108 | mpbid 231 |
. . . . . 6
β’ (π β (π
βπΊ) β (0.βπΎ)) |
110 | 109 | neneqd 2949 |
. . . . 5
β’ (π β Β¬ (π
βπΊ) = (0.βπΎ)) |
111 | 94, 7, 26, 27, 28 | trlator0 38637 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β π») β§ πΊ β π) β ((π
βπΊ) β π΄ β¨ (π
βπΊ) = (0.βπΎ))) |
112 | 1, 68, 111 | syl2anc 585 |
. . . . . . 7
β’ (π β ((π
βπΊ) β π΄ β¨ (π
βπΊ) = (0.βπΎ))) |
113 | 112 | orcomd 870 |
. . . . . 6
β’ (π β ((π
βπΊ) = (0.βπΎ) β¨ (π
βπΊ) β π΄)) |
114 | 113 | ord 863 |
. . . . 5
β’ (π β (Β¬ (π
βπΊ) = (0.βπΎ) β (π
βπΊ) β π΄)) |
115 | 110, 114 | mpd 15 |
. . . 4
β’ (π β (π
βπΊ) β π΄) |
116 | 14, 7 | atcmp 37776 |
. . . 4
β’ ((πΎ β AtLat β§ π β π΄ β§ (π
βπΊ) β π΄) β (π β€ (π
βπΊ) β π = (π
βπΊ))) |
117 | 91, 11, 115, 116 | syl3anc 1372 |
. . 3
β’ (π β (π β€ (π
βπΊ) β π = (π
βπΊ))) |
118 | 89, 117 | mpbid 231 |
. 2
β’ (π β π = (π
βπΊ)) |
119 | 118 | eqcomd 2743 |
1
β’ (π β (π
βπΊ) = π) |