Step | Hyp | Ref
| Expression |
1 | | dgraaval 41968 |
. . 3
β’ (π΄ β πΈ β
(degAAβπ΄)
= inf({π β β
β£ βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}, β, < )) |
2 | | ssrab2 4077 |
. . . . 5
β’ {π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β β |
3 | | nnuz 12867 |
. . . . 5
β’ β =
(β€β₯β1) |
4 | 2, 3 | sseqtri 4018 |
. . . 4
β’ {π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β
(β€β₯β1) |
5 | | eldifsn 4790 |
. . . . . . . . . . . 12
β’ (π β ((Polyββ)
β {0π}) β (π β (Polyββ) β§ π β
0π)) |
6 | 5 | biimpi 215 |
. . . . . . . . . . 11
β’ (π β ((Polyββ)
β {0π}) β (π β (Polyββ) β§ π β
0π)) |
7 | 6 | ad2antrr 724 |
. . . . . . . . . 10
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β (π β (Polyββ) β§ π β
0π)) |
8 | | simpr 485 |
. . . . . . . . . 10
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β π΄ β β) |
9 | | simplr 767 |
. . . . . . . . . 10
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β (πβπ΄) = 0) |
10 | | dgrnznn 25768 |
. . . . . . . . . 10
β’ (((π β (Polyββ)
β§ π β
0π) β§ (π΄ β β β§ (πβπ΄) = 0)) β (degβπ) β β) |
11 | 7, 8, 9, 10 | syl12anc 835 |
. . . . . . . . 9
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β (degβπ) β
β) |
12 | | simpll 765 |
. . . . . . . . 9
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β π β ((Polyββ) β
{0π})) |
13 | | eqid 2732 |
. . . . . . . . . 10
β’
(degβπ) =
(degβπ) |
14 | 9, 13 | jctil 520 |
. . . . . . . . 9
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β ((degβπ) = (degβπ) β§ (πβπ΄) = 0)) |
15 | | eqeq2 2744 |
. . . . . . . . . . 11
β’ (π = (degβπ) β ((degβπ) = π β (degβπ) = (degβπ))) |
16 | 15 | anbi1d 630 |
. . . . . . . . . 10
β’ (π = (degβπ) β (((degβπ) = π β§ (πβπ΄) = 0) β ((degβπ) = (degβπ) β§ (πβπ΄) = 0))) |
17 | | fveqeq2 6900 |
. . . . . . . . . . 11
β’ (π = π β ((degβπ) = (degβπ) β (degβπ) = (degβπ))) |
18 | | fveq1 6890 |
. . . . . . . . . . . 12
β’ (π = π β (πβπ΄) = (πβπ΄)) |
19 | 18 | eqeq1d 2734 |
. . . . . . . . . . 11
β’ (π = π β ((πβπ΄) = 0 β (πβπ΄) = 0)) |
20 | 17, 19 | anbi12d 631 |
. . . . . . . . . 10
β’ (π = π β (((degβπ) = (degβπ) β§ (πβπ΄) = 0) β ((degβπ) = (degβπ) β§ (πβπ΄) = 0))) |
21 | 16, 20 | rspc2ev 3624 |
. . . . . . . . 9
β’
(((degβπ)
β β β§ π
β ((Polyββ) β {0π}) β§
((degβπ) =
(degβπ) β§ (πβπ΄) = 0)) β βπ β β βπ β ((Polyββ) β
{0π})((degβπ) = π β§ (πβπ΄) = 0)) |
22 | 11, 12, 14, 21 | syl3anc 1371 |
. . . . . . . 8
β’ (((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β§ π΄ β β) β βπ β β βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0)) |
23 | 22 | ex 413 |
. . . . . . 7
β’ ((π β ((Polyββ)
β {0π}) β§ (πβπ΄) = 0) β (π΄ β β β βπ β β βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0))) |
24 | 23 | rexlimiva 3147 |
. . . . . 6
β’
(βπ β
((Polyββ) β {0π})(πβπ΄) = 0 β (π΄ β β β βπ β β βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0))) |
25 | 24 | impcom 408 |
. . . . 5
β’ ((π΄ β β β§
βπ β
((Polyββ) β {0π})(πβπ΄) = 0) β βπ β β βπ β ((Polyββ) β
{0π})((degβπ) = π β§ (πβπ΄) = 0)) |
26 | | elqaa 25842 |
. . . . 5
β’ (π΄ β πΈ β (π΄ β β β§
βπ β
((Polyββ) β {0π})(πβπ΄) = 0)) |
27 | | rabn0 4385 |
. . . . 5
β’ ({π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β β
β βπ β β βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0)) |
28 | 25, 26, 27 | 3imtr4i 291 |
. . . 4
β’ (π΄ β πΈ β {π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β β
) |
29 | | infssuzcl 12918 |
. . . 4
β’ (({π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β
(β€β₯β1) β§ {π β β β£ βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β β
) β inf({π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}, β, < ) β {π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}) |
30 | 4, 28, 29 | sylancr 587 |
. . 3
β’ (π΄ β πΈ β
inf({π β β
β£ βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}, β, < ) β {π β β β£
βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}) |
31 | 1, 30 | eqeltrd 2833 |
. 2
β’ (π΄ β πΈ β
(degAAβπ΄)
β {π β β
β£ βπ β
((Polyββ) β {0π})((degβπ) = π β§ (πβπ΄) = 0)}) |
32 | | eqeq2 2744 |
. . . . 5
β’ (π = (degAAβπ΄) β ((degβπ) = π β (degβπ) = (degAAβπ΄))) |
33 | 32 | anbi1d 630 |
. . . 4
β’ (π = (degAAβπ΄) β (((degβπ) = π β§ (πβπ΄) = 0) β ((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) |
34 | 33 | rexbidv 3178 |
. . 3
β’ (π = (degAAβπ΄) β (βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0) β βπ β ((Polyββ) β
{0π})((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) |
35 | 34 | elrab 3683 |
. 2
β’
((degAAβπ΄) β {π β β β£ βπ β ((Polyββ)
β {0π})((degβπ) = π β§ (πβπ΄) = 0)} β
((degAAβπ΄)
β β β§ βπ β ((Polyββ) β
{0π})((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) |
36 | 31, 35 | sylib 217 |
1
β’ (π΄ β πΈ β
((degAAβπ΄)
β β β§ βπ β ((Polyββ) β
{0π})((degβπ) = (degAAβπ΄) β§ (πβπ΄) = 0))) |