Step | Hyp | Ref
| Expression |
1 | | incom 4202 |
. 2
β’ (( β₯
βπ) β© π) = (π β© ( β₯ βπ)) |
2 | | osumcllem.u |
. . . . 5
β’ π = ( β₯ β( β₯
β(π + π))) |
3 | | simp1 1137 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β πΎ β HL) |
4 | | simp3 1139 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) |
5 | | osumcllem.a |
. . . . . . . . . . . 12
β’ π΄ = (AtomsβπΎ) |
6 | | osumcllem.c |
. . . . . . . . . . . 12
β’ πΆ = (PSubClβπΎ) |
7 | 5, 6 | psubclssatN 38812 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β πΆ) β π β π΄) |
8 | 7 | 3adant3 1133 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β π΄) |
9 | | osumcllem.o |
. . . . . . . . . . 11
β’ β₯ =
(β₯πβπΎ) |
10 | 5, 9 | polssatN 38779 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
11 | 3, 8, 10 | syl2anc 585 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ βπ) β π΄) |
12 | 4, 11 | sstrd 3993 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β π΄) |
13 | | osumcllem.p |
. . . . . . . . 9
β’ + =
(+πβπΎ) |
14 | 5, 13, 9 | poldmj1N 38799 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) |
15 | 3, 12, 8, 14 | syl3anc 1372 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) |
16 | | incom 4202 |
. . . . . . 7
β’ (( β₯
βπ) β© ( β₯
βπ)) = (( β₯
βπ) β© ( β₯
βπ)) |
17 | 15, 16 | eqtrdi 2789 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) |
18 | 17 | fveq2d 6896 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β( β₯
β(π + π))) = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |
19 | 2, 18 | eqtrid 2785 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |
20 | 19 | ineq1d 4212 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (π β© ( β₯ βπ)) = (( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β© ( β₯
βπ))) |
21 | 5, 9 | polcon2N 38790 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) |
22 | 8, 21 | syld3an2 1412 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) |
23 | 5, 9 | poml5N 38825 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β ( β₯ βπ)) β (( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β© ( β₯
βπ)) = ( β₯
β( β₯ βπ))) |
24 | 3, 12, 22, 23 | syl3anc 1372 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β© ( β₯
βπ)) = ( β₯
β( β₯ βπ))) |
25 | 9, 6 | psubcli2N 38810 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ) β ( β₯ β( β₯
βπ)) = π) |
26 | 25 | 3adant3 1133 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β( β₯
βπ)) = π) |
27 | 20, 24, 26 | 3eqtrd 2777 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (π β© ( β₯ βπ)) = π) |
28 | 1, 27 | eqtrid 2785 |
1
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (( β₯ βπ) β© π) = π) |