Step | Hyp | Ref
| Expression |
1 | | inass 4220 |
. . . . . . 7
β’ ((( β₯
βπ) β© π) β© π) = (( β₯ βπ) β© (π β© π)) |
2 | | simp11 1204 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β πΎ β HL) |
3 | | simp13 1206 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β πΆ) |
4 | | simp21 1207 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β ( β₯ βπ)) |
5 | | osumcllem.l |
. . . . . . . . . 10
β’ β€ =
(leβπΎ) |
6 | | osumcllem.j |
. . . . . . . . . 10
β’ β¨ =
(joinβπΎ) |
7 | | osumcllem.a |
. . . . . . . . . 10
β’ π΄ = (AtomsβπΎ) |
8 | | osumcllem.p |
. . . . . . . . . 10
β’ + =
(+πβπΎ) |
9 | | osumcllem.o |
. . . . . . . . . 10
β’ β₯ =
(β₯πβπΎ) |
10 | | osumcllem.c |
. . . . . . . . . 10
β’ πΆ = (PSubClβπΎ) |
11 | | osumcllem.m |
. . . . . . . . . 10
β’ π = (π + {π}) |
12 | | osumcllem.u |
. . . . . . . . . 10
β’ π = ( β₯ β( β₯
β(π + π))) |
13 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem3N 38829 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (( β₯ βπ) β© π) = π) |
14 | 2, 3, 4, 13 | syl3anc 1372 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (( β₯ βπ) β© π) = π) |
15 | 14 | ineq1d 4212 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ((( β₯ βπ) β© π) β© π) = (π β© π)) |
16 | 1, 15 | eqtr3id 2787 |
. . . . . 6
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (( β₯ βπ) β© (π β© π)) = (π β© π)) |
17 | | simp12 1205 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β πΆ) |
18 | 7, 10 | psubclssatN 38812 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ) β π β π΄) |
19 | 2, 17, 18 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β π΄) |
20 | 7, 10 | psubclssatN 38812 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ) β π β π΄) |
21 | 2, 3, 20 | syl2anc 585 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β π΄) |
22 | | simp22 1208 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β β
) |
23 | 7, 8 | paddssat 38685 |
. . . . . . . . . . . 12
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β (π + π) β π΄) |
24 | 2, 19, 21, 23 | syl3anc 1372 |
. . . . . . . . . . 11
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π + π) β π΄) |
25 | 7, 9 | polssatN 38779 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ (π + π) β π΄) β ( β₯ β(π + π)) β π΄) |
26 | 2, 24, 25 | syl2anc 585 |
. . . . . . . . . 10
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ( β₯ β(π + π)) β π΄) |
27 | 7, 9 | polssatN 38779 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ ( β₯
β(π + π)) β π΄) β ( β₯ β( β₯
β(π + π))) β π΄) |
28 | 2, 26, 27 | syl2anc 585 |
. . . . . . . . 9
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ( β₯ β( β₯
β(π + π))) β π΄) |
29 | 12, 28 | eqsstrid 4031 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β π΄) |
30 | | simp23 1209 |
. . . . . . . 8
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β π) |
31 | 29, 30 | sseldd 3984 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β π΄) |
32 | | simp3 1139 |
. . . . . . 7
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β Β¬ π β (π + π)) |
33 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem8N 38834 |
. . . . . . 7
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π΄) β§ Β¬ π β (π + π)) β (π β© π) = β
) |
34 | 2, 19, 21, 4, 22, 31, 32, 33 | syl331anc 1396 |
. . . . . 6
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π β© π) = β
) |
35 | 16, 34 | eqtrd 2773 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (( β₯ βπ) β© (π β© π)) = β
) |
36 | 35 | fveq2d 6896 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ( β₯ β(( β₯
βπ) β© (π β© π))) = ( β₯
ββ
)) |
37 | 7, 9 | pol0N 38780 |
. . . . 5
β’ (πΎ β HL β ( β₯
ββ
) = π΄) |
38 | 2, 37 | syl 17 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ( β₯ ββ
) =
π΄) |
39 | 36, 38 | eqtrd 2773 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ( β₯ β(( β₯
βπ) β© (π β© π))) = π΄) |
40 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem1N 38827 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β (π β© π) = π) |
41 | 2, 19, 21, 30, 40 | syl31anc 1374 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π β© π) = π) |
42 | 39, 41 | ineq12d 4214 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (( β₯ β(( β₯
βπ) β© (π β© π))) β© (π β© π)) = (π΄ β© π)) |
43 | 7, 9, 10 | polsubclN 38823 |
. . . . . 6
β’ ((πΎ β HL β§ ( β₯
β(π + π)) β π΄) β ( β₯ β( β₯
β(π + π))) β πΆ) |
44 | 2, 26, 43 | syl2anc 585 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β ( β₯ β( β₯
β(π + π))) β πΆ) |
45 | 12, 44 | eqeltrid 2838 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β πΆ) |
46 | 7, 8, 10 | paddatclN 38820 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ β§ π β π΄) β (π + {π}) β πΆ) |
47 | 2, 17, 31, 46 | syl3anc 1372 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π + {π}) β πΆ) |
48 | 11, 47 | eqeltrid 2838 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β πΆ) |
49 | 10 | psubclinN 38819 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β πΆ) β (π β© π) β πΆ) |
50 | 2, 45, 48, 49 | syl3anc 1372 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π β© π) β πΆ) |
51 | 5, 6, 7, 8, 9, 10,
11, 12 | osumcllem2N 38828 |
. . . 4
β’ (((πΎ β HL β§ π β π΄ β§ π β π΄) β§ π β π) β π β (π β© π)) |
52 | 2, 19, 21, 30, 51 | syl31anc 1374 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β (π β© π)) |
53 | 10, 9 | poml6N 38826 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ (π β© π) β πΆ) β§ π β (π β© π)) β (( β₯ β(( β₯
βπ) β© (π β© π))) β© (π β© π)) = π) |
54 | 2, 17, 50, 52, 53 | syl31anc 1374 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (( β₯ β(( β₯
βπ) β© (π β© π))) β© (π β© π)) = π) |
55 | 31 | snssd 4813 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β {π} β π΄) |
56 | 7, 8 | paddssat 38685 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ {π} β π΄) β (π + {π}) β π΄) |
57 | 2, 19, 55, 56 | syl3anc 1372 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π + {π}) β π΄) |
58 | 11, 57 | eqsstrid 4031 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π β π΄) |
59 | | sseqin2 4216 |
. . 3
β’ (π β π΄ β (π΄ β© π) = π) |
60 | 58, 59 | sylib 217 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β (π΄ β© π) = π) |
61 | 42, 54, 60 | 3eqtr3rd 2782 |
1
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
β§ π β π) β§ Β¬ π β (π + π)) β π = π) |