Step | Hyp | Ref
| Expression |
1 | | plydiv.f |
. . 3
β’ (π β πΉ β (Polyβπ)) |
2 | | plybss 25943 |
. . 3
β’ (πΉ β (Polyβπ) β π β β) |
3 | | ply0 25957 |
. . 3
β’ (π β β β
0π β (Polyβπ)) |
4 | 1, 2, 3 | 3syl 18 |
. 2
β’ (π β 0π
β (Polyβπ)) |
5 | | plydiv.0 |
. . 3
β’ (π β (πΉ = 0π β¨
((degβπΉ) β
(degβπΊ)) <
0)) |
6 | | cnex 11193 |
. . . . . . 7
β’ β
β V |
7 | 6 | a1i 11 |
. . . . . 6
β’ (π β β β
V) |
8 | | plyf 25947 |
. . . . . . 7
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
9 | | ffn 6716 |
. . . . . . 7
β’ (πΉ:ββΆβ β
πΉ Fn
β) |
10 | 1, 8, 9 | 3syl 18 |
. . . . . 6
β’ (π β πΉ Fn β) |
11 | | plydiv.g |
. . . . . . . 8
β’ (π β πΊ β (Polyβπ)) |
12 | | plyf 25947 |
. . . . . . . 8
β’ (πΊ β (Polyβπ) β πΊ:ββΆβ) |
13 | | ffn 6716 |
. . . . . . . 8
β’ (πΊ:ββΆβ β
πΊ Fn
β) |
14 | 11, 12, 13 | 3syl 18 |
. . . . . . 7
β’ (π β πΊ Fn β) |
15 | | plyf 25947 |
. . . . . . . 8
β’
(0π β (Polyβπ) β
0π:ββΆβ) |
16 | | ffn 6716 |
. . . . . . . 8
β’
(0π:ββΆβ β
0π Fn β) |
17 | 4, 15, 16 | 3syl 18 |
. . . . . . 7
β’ (π β 0π Fn
β) |
18 | | inidm 4217 |
. . . . . . 7
β’ (β
β© β) = β |
19 | 14, 17, 7, 7, 18 | offn 7685 |
. . . . . 6
β’ (π β (πΊ βf Β·
0π) Fn β) |
20 | | eqidd 2731 |
. . . . . 6
β’ ((π β§ π§ β β) β (πΉβπ§) = (πΉβπ§)) |
21 | | eqidd 2731 |
. . . . . . . 8
β’ ((π β§ π§ β β) β (πΊβπ§) = (πΊβπ§)) |
22 | | 0pval 25420 |
. . . . . . . . 9
β’ (π§ β β β
(0πβπ§) = 0) |
23 | 22 | adantl 480 |
. . . . . . . 8
β’ ((π β§ π§ β β) β
(0πβπ§) = 0) |
24 | 14, 17, 7, 7, 18, 21, 23 | ofval 7683 |
. . . . . . 7
β’ ((π β§ π§ β β) β ((πΊ βf Β·
0π)βπ§) = ((πΊβπ§) Β· 0)) |
25 | 11, 12 | syl 17 |
. . . . . . . . 9
β’ (π β πΊ:ββΆβ) |
26 | 25 | ffvelcdmda 7085 |
. . . . . . . 8
β’ ((π β§ π§ β β) β (πΊβπ§) β β) |
27 | 26 | mul01d 11417 |
. . . . . . 7
β’ ((π β§ π§ β β) β ((πΊβπ§) Β· 0) = 0) |
28 | 24, 27 | eqtrd 2770 |
. . . . . 6
β’ ((π β§ π§ β β) β ((πΊ βf Β·
0π)βπ§) = 0) |
29 | 1, 8 | syl 17 |
. . . . . . . 8
β’ (π β πΉ:ββΆβ) |
30 | 29 | ffvelcdmda 7085 |
. . . . . . 7
β’ ((π β§ π§ β β) β (πΉβπ§) β β) |
31 | 30 | subid1d 11564 |
. . . . . 6
β’ ((π β§ π§ β β) β ((πΉβπ§) β 0) = (πΉβπ§)) |
32 | 7, 10, 19, 10, 20, 28, 31 | offveq 7696 |
. . . . 5
β’ (π β (πΉ βf β (πΊ βf Β·
0π)) = πΉ) |
33 | 32 | eqeq1d 2732 |
. . . 4
β’ (π β ((πΉ βf β (πΊ βf Β·
0π)) = 0π β πΉ = 0π)) |
34 | 32 | fveq2d 6894 |
. . . . . 6
β’ (π β (degβ(πΉ βf β
(πΊ βf
Β· 0π))) = (degβπΉ)) |
35 | | dgrcl 25982 |
. . . . . . . . . . 11
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
36 | 11, 35 | syl 17 |
. . . . . . . . . 10
β’ (π β (degβπΊ) β
β0) |
37 | 36 | nn0red 12537 |
. . . . . . . . 9
β’ (π β (degβπΊ) β
β) |
38 | 37 | recnd 11246 |
. . . . . . . 8
β’ (π β (degβπΊ) β
β) |
39 | 38 | addlidd 11419 |
. . . . . . 7
β’ (π β (0 + (degβπΊ)) = (degβπΊ)) |
40 | 39 | eqcomd 2736 |
. . . . . 6
β’ (π β (degβπΊ) = (0 + (degβπΊ))) |
41 | 34, 40 | breq12d 5160 |
. . . . 5
β’ (π β ((degβ(πΉ βf β
(πΊ βf
Β· 0π))) < (degβπΊ) β (degβπΉ) < (0 + (degβπΊ)))) |
42 | | dgrcl 25982 |
. . . . . . . 8
β’ (πΉ β (Polyβπ) β (degβπΉ) β
β0) |
43 | 1, 42 | syl 17 |
. . . . . . 7
β’ (π β (degβπΉ) β
β0) |
44 | 43 | nn0red 12537 |
. . . . . 6
β’ (π β (degβπΉ) β
β) |
45 | | 0red 11221 |
. . . . . 6
β’ (π β 0 β
β) |
46 | 44, 37, 45 | ltsubaddd 11814 |
. . . . 5
β’ (π β (((degβπΉ) β (degβπΊ)) < 0 β
(degβπΉ) < (0 +
(degβπΊ)))) |
47 | 41, 46 | bitr4d 281 |
. . . 4
β’ (π β ((degβ(πΉ βf β
(πΊ βf
Β· 0π))) < (degβπΊ) β ((degβπΉ) β (degβπΊ)) < 0)) |
48 | 33, 47 | orbi12d 915 |
. . 3
β’ (π β (((πΉ βf β (πΊ βf Β·
0π)) = 0π β¨ (degβ(πΉ βf β
(πΊ βf
Β· 0π))) < (degβπΊ)) β (πΉ = 0π β¨
((degβπΉ) β
(degβπΊ)) <
0))) |
49 | 5, 48 | mpbird 256 |
. 2
β’ (π β ((πΉ βf β (πΊ βf Β·
0π)) = 0π β¨ (degβ(πΉ βf β
(πΊ βf
Β· 0π))) < (degβπΊ))) |
50 | | plydiv.r |
. . . . . 6
β’ π
= (πΉ βf β (πΊ βf Β·
π)) |
51 | | oveq2 7419 |
. . . . . . 7
β’ (π = 0π β
(πΊ βf
Β· π) = (πΊ βf Β·
0π)) |
52 | 51 | oveq2d 7427 |
. . . . . 6
β’ (π = 0π β
(πΉ βf
β (πΊ
βf Β· π)) = (πΉ βf β (πΊ βf Β·
0π))) |
53 | 50, 52 | eqtrid 2782 |
. . . . 5
β’ (π = 0π β
π
= (πΉ βf β (πΊ βf Β·
0π))) |
54 | 53 | eqeq1d 2732 |
. . . 4
β’ (π = 0π β
(π
= 0π
β (πΉ
βf β (πΊ βf Β·
0π)) = 0π)) |
55 | 53 | fveq2d 6894 |
. . . . 5
β’ (π = 0π β
(degβπ
) =
(degβ(πΉ
βf β (πΊ βf Β·
0π)))) |
56 | 55 | breq1d 5157 |
. . . 4
β’ (π = 0π β
((degβπ
) <
(degβπΊ) β
(degβ(πΉ
βf β (πΊ βf Β·
0π))) < (degβπΊ))) |
57 | 54, 56 | orbi12d 915 |
. . 3
β’ (π = 0π β
((π
= 0π
β¨ (degβπ
) <
(degβπΊ)) β
((πΉ βf
β (πΊ
βf Β· 0π)) = 0π
β¨ (degβ(πΉ
βf β (πΊ βf Β·
0π))) < (degβπΊ)))) |
58 | 57 | rspcev 3611 |
. 2
β’
((0π β (Polyβπ) β§ ((πΉ βf β (πΊ βf Β·
0π)) = 0π β¨ (degβ(πΉ βf β
(πΊ βf
Β· 0π))) < (degβπΊ))) β βπ β (Polyβπ)(π
= 0π β¨
(degβπ
) <
(degβπΊ))) |
59 | 4, 49, 58 | syl2anc 582 |
1
β’ (π β βπ β (Polyβπ)(π
= 0π β¨
(degβπ
) <
(degβπΊ))) |