Step | Hyp | Ref
| Expression |
1 | | simpl1 1191 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β πΎ β HL) |
2 | | simpl2 1192 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β π β πΆ) |
3 | | eqid 2732 |
. . . . 5
β’
(AtomsβπΎ) =
(AtomsβπΎ) |
4 | | osumcl.c |
. . . . 5
β’ πΆ = (PSubClβπΎ) |
5 | 3, 4 | psubclssatN 39115 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ) β π β (AtomsβπΎ)) |
6 | 1, 2, 5 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β π β (AtomsβπΎ)) |
7 | | simpl3 1193 |
. . . 4
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β π β πΆ) |
8 | 3, 4 | psubclssatN 39115 |
. . . 4
β’ ((πΎ β HL β§ π β πΆ) β π β (AtomsβπΎ)) |
9 | 1, 7, 8 | syl2anc 584 |
. . 3
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β π β (AtomsβπΎ)) |
10 | | osumcl.p |
. . . 4
β’ + =
(+πβπΎ) |
11 | 3, 10 | paddssat 38988 |
. . 3
β’ ((πΎ β HL β§ π β (AtomsβπΎ) β§ π β (AtomsβπΎ)) β (π + π) β (AtomsβπΎ)) |
12 | 1, 6, 9, 11 | syl3anc 1371 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β (π + π) β (AtomsβπΎ)) |
13 | | simpll1 1212 |
. . . 4
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π = β
) β πΎ β HL) |
14 | | oveq1 7418 |
. . . . . 6
β’ (π = β
β (π + π) = (β
+ π)) |
15 | 3, 10 | padd02 38986 |
. . . . . . 7
β’ ((πΎ β HL β§ π β (AtomsβπΎ)) β (β
+ π) = π) |
16 | 1, 9, 15 | syl2anc 584 |
. . . . . 6
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β (β
+ π) = π) |
17 | 14, 16 | sylan9eqr 2794 |
. . . . 5
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π = β
) β (π + π) = π) |
18 | | simpll3 1214 |
. . . . 5
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π = β
) β π β πΆ) |
19 | 17, 18 | eqeltrd 2833 |
. . . 4
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π = β
) β (π + π) β πΆ) |
20 | | osumcl.o |
. . . . 5
β’ β₯ =
(β₯πβπΎ) |
21 | 20, 4 | psubcli2N 39113 |
. . . 4
β’ ((πΎ β HL β§ (π + π) β πΆ) β ( β₯ β( β₯
β(π + π))) = (π + π)) |
22 | 13, 19, 21 | syl2anc 584 |
. . 3
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π = β
) β ( β₯ β( β₯
β(π + π))) = (π + π)) |
23 | 10, 20, 4 | osumcllem11N 39140 |
. . . . 5
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ (π β ( β₯ βπ) β§ π β β
)) β (π + π) = ( β₯ β( β₯
β(π + π)))) |
24 | 23 | anassrs 468 |
. . . 4
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π β β
) β (π + π) = ( β₯ β( β₯
β(π + π)))) |
25 | 24 | eqcomd 2738 |
. . 3
β’ ((((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β§ π β β
) β ( β₯ β( β₯
β(π + π))) = (π + π)) |
26 | 22, 25 | pm2.61dane 3029 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β ( β₯ β( β₯
β(π + π))) = (π + π)) |
27 | 3, 20, 4 | ispsubclN 39111 |
. . 3
β’ (πΎ β HL β ((π + π) β πΆ β ((π + π) β (AtomsβπΎ) β§ ( β₯ β( β₯
β(π + π))) = (π + π)))) |
28 | 1, 27 | syl 17 |
. 2
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β ((π + π) β πΆ β ((π + π) β (AtomsβπΎ) β§ ( β₯ β( β₯
β(π + π))) = (π + π)))) |
29 | 12, 26, 28 | mpbir2and 711 |
1
β’ (((πΎ β HL β§ π β πΆ β§ π β πΆ) β§ π β ( β₯ βπ)) β (π + π) β πΆ) |