Step | Hyp | Ref
| Expression |
1 | | simpll 765 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β πΎ β HL) |
2 | | simplr 767 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β π β π΄) |
3 | | pexmid.a |
. . . . . . 7
β’ π΄ = (AtomsβπΎ) |
4 | | pexmid.o |
. . . . . . 7
β’ β₯ =
(β₯πβπΎ) |
5 | 3, 4 | polssatN 38774 |
. . . . . 6
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β π΄) |
6 | 5 | adantr 481 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ βπ) β π΄) |
7 | | pexmid.p |
. . . . . 6
β’ + =
(+πβπΎ) |
8 | 3, 7, 4 | poldmj1N 38794 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄ β§ ( β₯ βπ) β π΄) β ( β₯ β(π + ( β₯ βπ))) = (( β₯ βπ) β© ( β₯ β( β₯
βπ)))) |
9 | 1, 2, 6, 8 | syl3anc 1371 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ β(π + ( β₯ βπ))) = (( β₯ βπ) β© ( β₯ β( β₯
βπ)))) |
10 | 3, 4 | pnonsingN 38799 |
. . . . 5
β’ ((πΎ β HL β§ ( β₯
βπ) β π΄) β (( β₯ βπ) β© ( β₯ β( β₯
βπ))) =
β
) |
11 | 1, 6, 10 | syl2anc 584 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β (( β₯ βπ) β© ( β₯ β( β₯
βπ))) =
β
) |
12 | 9, 11 | eqtrd 2772 |
. . 3
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ β(π + ( β₯ βπ))) = β
) |
13 | 12 | fveq2d 6895 |
. 2
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ β( β₯
β(π + ( β₯
βπ)))) = ( β₯
ββ
)) |
14 | | simpr 485 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ β( β₯
βπ)) = π) |
15 | | eqid 2732 |
. . . . . . 7
β’
(PSubClβπΎ) =
(PSubClβπΎ) |
16 | 3, 4, 15 | ispsubclN 38803 |
. . . . . 6
β’ (πΎ β HL β (π β (PSubClβπΎ) β (π β π΄ β§ ( β₯ β( β₯
βπ)) = π))) |
17 | 16 | ad2antrr 724 |
. . . . 5
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β (π β (PSubClβπΎ) β (π β π΄ β§ ( β₯ β( β₯
βπ)) = π))) |
18 | 2, 14, 17 | mpbir2and 711 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β π β (PSubClβπΎ)) |
19 | 3, 4, 15 | polsubclN 38818 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β ( β₯ βπ) β (PSubClβπΎ)) |
20 | 19 | adantr 481 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ βπ) β (PSubClβπΎ)) |
21 | 3, 4 | 2polssN 38781 |
. . . . 5
β’ ((πΎ β HL β§ π β π΄) β π β ( β₯ β( β₯
βπ))) |
22 | 21 | adantr 481 |
. . . 4
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β π β ( β₯ β( β₯
βπ))) |
23 | 7, 4, 15 | osumclN 38833 |
. . . 4
β’ (((πΎ β HL β§ π β (PSubClβπΎ) β§ ( β₯ βπ) β (PSubClβπΎ)) β§ π β ( β₯ β( β₯
βπ))) β (π + ( β₯ βπ)) β (PSubClβπΎ)) |
24 | 1, 18, 20, 22, 23 | syl31anc 1373 |
. . 3
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β (π + ( β₯ βπ)) β (PSubClβπΎ)) |
25 | 4, 15 | psubcli2N 38805 |
. . 3
β’ ((πΎ β HL β§ (π + ( β₯ βπ)) β (PSubClβπΎ)) β ( β₯ β( β₯
β(π + ( β₯
βπ)))) = (π + ( β₯ βπ))) |
26 | 1, 24, 25 | syl2anc 584 |
. 2
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ β( β₯
β(π + ( β₯
βπ)))) = (π + ( β₯ βπ))) |
27 | 3, 4 | pol0N 38775 |
. . 3
β’ (πΎ β HL β ( β₯
ββ
) = π΄) |
28 | 27 | ad2antrr 724 |
. 2
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β ( β₯ ββ
) =
π΄) |
29 | 13, 26, 28 | 3eqtr3d 2780 |
1
β’ (((πΎ β HL β§ π β π΄) β§ ( β₯ β( β₯
βπ)) = π) β (π + ( β₯ βπ)) = π΄) |