Step | Hyp | Ref
| Expression |
1 | | incom 4200 |
. 2
β’ (( β₯
βπ) β© π) = (π β© ( β₯ βπ)) |
2 | | osumcllem.u |
. . . . 5
β’ π = ( β₯ β( β₯
β(π + π))) |
3 | | simp1 1134 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β πΎ β HL) |
4 | | simp3 1136 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) |
5 | | osumcllem.a |
. . . . . . . . . . . 12
β’ π΄ = (AtomsβπΎ) |
6 | | osumcllem.c |
. . . . . . . . . . . 12
β’ πΆ = (PSubClβπΎ) |
7 | 5, 6 | psubclssatN 39115 |
. . . . . . . . . . 11
β’ ((πΎ β HL β§ π β πΆ) β π β π΄) |
8 | 7 | 3adant3 1130 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β π΄) |
9 | | osumcllem.o |
. . . . . . . . . . 11
β’ β₯ =
(β₯πβπΎ) |
10 | 5, 9 | polssatN 39082 |
. . . . . . . . . 10
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
11 | 3, 8, 10 | syl2anc 582 |
. . . . . . . . 9
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ βπ) β π΄) |
12 | 4, 11 | sstrd 3991 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β π΄) |
13 | | osumcllem.p |
. . . . . . . . 9
β’ + =
(+πβπΎ) |
14 | 5, 13, 9 | poldmj1N 39102 |
. . . . . . . 8
β’ ((πΎ β HL β§ π β π΄ β§ π β π΄) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) |
15 | 3, 12, 8, 14 | syl3anc 1369 |
. . . . . . 7
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) |
16 | | incom 4200 |
. . . . . . 7
β’ (( β₯
βπ) β© ( β₯
βπ)) = (( β₯
βπ) β© ( β₯
βπ)) |
17 | 15, 16 | eqtrdi 2786 |
. . . . . 6
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β(π + π)) = (( β₯ βπ) β© ( β₯ βπ))) |
18 | 17 | fveq2d 6894 |
. . . . 5
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β( β₯
β(π + π))) = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |
19 | 2, 18 | eqtrid 2782 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π = ( β₯ β(( β₯
βπ) β© ( β₯
βπ)))) |
20 | 19 | ineq1d 4210 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (π β© ( β₯ βπ)) = (( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β© ( β₯
βπ))) |
21 | 5, 9 | polcon2N 39093 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) |
22 | 8, 21 | syld3an2 1409 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β π β ( β₯ βπ)) |
23 | 5, 9 | poml5N 39128 |
. . . 4
β’ ((πΎ β HL β§ π β π΄ β§ π β ( β₯ βπ)) β (( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β© ( β₯
βπ)) = ( β₯
β( β₯ βπ))) |
24 | 3, 12, 22, 23 | syl3anc 1369 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (( β₯ β(( β₯
βπ) β© ( β₯
βπ))) β© ( β₯
βπ)) = ( β₯
β( β₯ βπ))) |
25 | 9, 6 | psubcli2N 39113 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ) β ( β₯ β( β₯
βπ)) = π) |
26 | 25 | 3adant3 1130 |
. . 3
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β ( β₯ β( β₯
βπ)) = π) |
27 | 20, 24, 26 | 3eqtrd 2774 |
. 2
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (π β© ( β₯ βπ)) = π) |
28 | 1, 27 | eqtrid 2782 |
1
β’ ((πΎ β HL β§ π β πΆ β§ π β ( β₯ βπ)) β (( β₯ βπ) β© π) = π) |