Step | Hyp | Ref
| Expression |
1 | | elaa 25758 |
. . 3
β’ (π΄ β πΈ β (π΄ β β β§
βπ β
((Polyββ€) β {0π})(πβπ΄) = 0)) |
2 | | zssq 12922 |
. . . . . 6
β’ β€
β β |
3 | | qsscn 12926 |
. . . . . 6
β’ β
β β |
4 | | plyss 25642 |
. . . . . 6
β’ ((β€
β β β§ β β β) β (Polyββ€)
β (Polyββ)) |
5 | 2, 3, 4 | mp2an 690 |
. . . . 5
β’
(Polyββ€) β (Polyββ) |
6 | | ssdif 4135 |
. . . . 5
β’
((Polyββ€) β (Polyββ) β
((Polyββ€) β {0π}) β
((Polyββ) β {0π})) |
7 | | ssrexv 4047 |
. . . . 5
β’
(((Polyββ€) β {0π}) β
((Polyββ) β {0π}) β (βπ β ((Polyββ€)
β {0π})(πβπ΄) = 0 β βπ β ((Polyββ) β
{0π})(πβπ΄) = 0)) |
8 | 5, 6, 7 | mp2b 10 |
. . . 4
β’
(βπ β
((Polyββ€) β {0π})(πβπ΄) = 0 β βπ β ((Polyββ) β
{0π})(πβπ΄) = 0) |
9 | 8 | anim2i 617 |
. . 3
β’ ((π΄ β β β§
βπ β
((Polyββ€) β {0π})(πβπ΄) = 0) β (π΄ β β β§ βπ β ((Polyββ)
β {0π})(πβπ΄) = 0)) |
10 | 1, 9 | sylbi 216 |
. 2
β’ (π΄ β πΈ β (π΄ β β β§
βπ β
((Polyββ) β {0π})(πβπ΄) = 0)) |
11 | | simpll 765 |
. . . 4
β’ (((π΄ β β β§ π β ((Polyββ)
β {0π})) β§ (πβπ΄) = 0) β π΄ β β) |
12 | | simplr 767 |
. . . 4
β’ (((π΄ β β β§ π β ((Polyββ)
β {0π})) β§ (πβπ΄) = 0) β π β ((Polyββ) β
{0π})) |
13 | | simpr 485 |
. . . 4
β’ (((π΄ β β β§ π β ((Polyββ)
β {0π})) β§ (πβπ΄) = 0) β (πβπ΄) = 0) |
14 | | eqid 2731 |
. . . 4
β’
(coeffβπ) =
(coeffβπ) |
15 | | fveq2 6878 |
. . . . . . . . . 10
β’ (π = π β ((coeffβπ)βπ) = ((coeffβπ)βπ)) |
16 | 15 | oveq1d 7408 |
. . . . . . . . 9
β’ (π = π β (((coeffβπ)βπ) Β· π) = (((coeffβπ)βπ) Β· π)) |
17 | 16 | eleq1d 2817 |
. . . . . . . 8
β’ (π = π β ((((coeffβπ)βπ) Β· π) β β€ β (((coeffβπ)βπ) Β· π) β β€)) |
18 | 17 | rabbidv 3439 |
. . . . . . 7
β’ (π = π β {π β β β£ (((coeffβπ)βπ) Β· π) β β€} = {π β β β£ (((coeffβπ)βπ) Β· π) β β€}) |
19 | | oveq2 7401 |
. . . . . . . . 9
β’ (π = π β (((coeffβπ)βπ) Β· π) = (((coeffβπ)βπ) Β· π)) |
20 | 19 | eleq1d 2817 |
. . . . . . . 8
β’ (π = π β ((((coeffβπ)βπ) Β· π) β β€ β (((coeffβπ)βπ) Β· π) β β€)) |
21 | 20 | cbvrabv 3441 |
. . . . . . 7
β’ {π β β β£
(((coeffβπ)βπ) Β· π) β β€} = {π β β β£ (((coeffβπ)βπ) Β· π) β β€} |
22 | 18, 21 | eqtrdi 2787 |
. . . . . 6
β’ (π = π β {π β β β£ (((coeffβπ)βπ) Β· π) β β€} = {π β β β£ (((coeffβπ)βπ) Β· π) β β€}) |
23 | 22 | infeq1d 9454 |
. . . . 5
β’ (π = π β inf({π β β β£ (((coeffβπ)βπ) Β· π) β β€}, β, < ) =
inf({π β β
β£ (((coeffβπ)βπ) Β· π) β β€}, β, <
)) |
24 | 23 | cbvmptv 5254 |
. . . 4
β’ (π β β0
β¦ inf({π β
β β£ (((coeffβπ)βπ) Β· π) β β€}, β, < )) = (π β β0
β¦ inf({π β
β β£ (((coeffβπ)βπ) Β· π) β β€}, β, <
)) |
25 | | eqid 2731 |
. . . 4
β’ (seq0(
Β· , (π β
β0 β¦ inf({π β β β£ (((coeffβπ)βπ) Β· π) β β€}, β, <
)))β(degβπ)) =
(seq0( Β· , (π β
β0 β¦ inf({π β β β£ (((coeffβπ)βπ) Β· π) β β€}, β, <
)))β(degβπ)) |
26 | 11, 12, 13, 14, 24, 25 | elqaalem3 25763 |
. . 3
β’ (((π΄ β β β§ π β ((Polyββ)
β {0π})) β§ (πβπ΄) = 0) β π΄ β πΈ) |
27 | 26 | r19.29an 3157 |
. 2
β’ ((π΄ β β β§
βπ β
((Polyββ) β {0π})(πβπ΄) = 0) β π΄ β πΈ) |
28 | 10, 27 | impbii 208 |
1
β’ (π΄ β πΈ β (π΄ β β β§
βπ β
((Polyββ) β {0π})(πβπ΄) = 0)) |