Step | Hyp | Ref
| Expression |
1 | | idd 24 |
. . . 4
β’ (π β ((π βf β π) = 0π β
(π βf
β π) =
0π)) |
2 | | plydiveu.q |
. . . . . . . . . . . . . . . 16
β’ (π β π β (Polyβπ)) |
3 | | plydiv.pl |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ + π¦) β π) |
4 | | plydiv.tm |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π β§ π¦ β π)) β (π₯ Β· π¦) β π) |
5 | | plydiv.rc |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ (π₯ β π β§ π₯ β 0)) β (1 / π₯) β π) |
6 | | plydiv.m1 |
. . . . . . . . . . . . . . . . 17
β’ (π β -1 β π) |
7 | | plydiv.f |
. . . . . . . . . . . . . . . . 17
β’ (π β πΉ β (Polyβπ)) |
8 | | plydiv.g |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ β (Polyβπ)) |
9 | | plydiv.z |
. . . . . . . . . . . . . . . . 17
β’ (π β πΊ β
0π) |
10 | | plydiv.r |
. . . . . . . . . . . . . . . . 17
β’ π
= (πΉ βf β (πΊ βf Β·
π)) |
11 | 3, 4, 5, 6, 7, 8, 9, 10 | plydivlem2 25495 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ)) β π
β (Polyβπ)) |
12 | 2, 11 | mpdan 685 |
. . . . . . . . . . . . . . 15
β’ (π β π
β (Polyβπ)) |
13 | | plydiveu.p |
. . . . . . . . . . . . . . . 16
β’ (π β π β (Polyβπ)) |
14 | | plydiveu.t |
. . . . . . . . . . . . . . . . 17
β’ π = (πΉ βf β (πΊ βf Β·
π)) |
15 | 3, 4, 5, 6, 7, 8, 9, 14 | plydivlem2 25495 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ π β (Polyβπ)) β π β (Polyβπ)) |
16 | 13, 15 | mpdan 685 |
. . . . . . . . . . . . . . 15
β’ (π β π β (Polyβπ)) |
17 | 12, 16, 3, 4, 6 | plysub 25421 |
. . . . . . . . . . . . . 14
β’ (π β (π
βf β π) β (Polyβπ)) |
18 | | dgrcl 25435 |
. . . . . . . . . . . . . 14
β’ ((π
βf β
π) β (Polyβπ) β (degβ(π
βf β
π)) β
β0) |
19 | 17, 18 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (degβ(π
βf β
π)) β
β0) |
20 | 19 | nn0red 12336 |
. . . . . . . . . . . 12
β’ (π β (degβ(π
βf β
π)) β
β) |
21 | | dgrcl 25435 |
. . . . . . . . . . . . . . 15
β’ (π β (Polyβπ) β (degβπ) β
β0) |
22 | 16, 21 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (degβπ) β
β0) |
23 | 22 | nn0red 12336 |
. . . . . . . . . . . . 13
β’ (π β (degβπ) β
β) |
24 | | dgrcl 25435 |
. . . . . . . . . . . . . . 15
β’ (π
β (Polyβπ) β (degβπ
) β
β0) |
25 | 12, 24 | syl 17 |
. . . . . . . . . . . . . 14
β’ (π β (degβπ
) β
β0) |
26 | 25 | nn0red 12336 |
. . . . . . . . . . . . 13
β’ (π β (degβπ
) β
β) |
27 | 23, 26 | ifcld 4511 |
. . . . . . . . . . . 12
β’ (π β if((degβπ
) β€ (degβπ), (degβπ), (degβπ
)) β β) |
28 | | dgrcl 25435 |
. . . . . . . . . . . . . 14
β’ (πΊ β (Polyβπ) β (degβπΊ) β
β0) |
29 | 8, 28 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (degβπΊ) β
β0) |
30 | 29 | nn0red 12336 |
. . . . . . . . . . . 12
β’ (π β (degβπΊ) β
β) |
31 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’
(degβπ
) =
(degβπ
) |
32 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’
(degβπ) =
(degβπ) |
33 | 31, 32 | dgrsub 25474 |
. . . . . . . . . . . . 13
β’ ((π
β (Polyβπ) β§ π β (Polyβπ)) β (degβ(π
βf β π)) β€ if((degβπ
) β€ (degβπ), (degβπ), (degβπ
))) |
34 | 12, 16, 33 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (degβ(π
βf β
π)) β€
if((degβπ
) β€
(degβπ),
(degβπ),
(degβπ
))) |
35 | | plydiveu.pd |
. . . . . . . . . . . . . . 15
β’ (π β (π = 0π β¨
(degβπ) <
(degβπΊ))) |
36 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
β’
(coeffβπ) =
(coeffβπ) |
37 | 32, 36 | dgrlt 25468 |
. . . . . . . . . . . . . . . 16
β’ ((π β (Polyβπ) β§ (degβπΊ) β β0)
β ((π =
0π β¨ (degβπ) < (degβπΊ)) β ((degβπ) β€ (degβπΊ) β§ ((coeffβπ)β(degβπΊ)) = 0))) |
38 | 16, 29, 37 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β ((π = 0π β¨
(degβπ) <
(degβπΊ)) β
((degβπ) β€
(degβπΊ) β§
((coeffβπ)β(degβπΊ)) = 0))) |
39 | 35, 38 | mpbid 232 |
. . . . . . . . . . . . . 14
β’ (π β ((degβπ) β€ (degβπΊ) β§ ((coeffβπ)β(degβπΊ)) = 0)) |
40 | 39 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β (degβπ) β€ (degβπΊ)) |
41 | | plydiveu.qd |
. . . . . . . . . . . . . . 15
β’ (π β (π
= 0π β¨
(degβπ
) <
(degβπΊ))) |
42 | | eqid 2736 |
. . . . . . . . . . . . . . . . 17
β’
(coeffβπ
) =
(coeffβπ
) |
43 | 31, 42 | dgrlt 25468 |
. . . . . . . . . . . . . . . 16
β’ ((π
β (Polyβπ) β§ (degβπΊ) β β0)
β ((π
=
0π β¨ (degβπ
) < (degβπΊ)) β ((degβπ
) β€ (degβπΊ) β§ ((coeffβπ
)β(degβπΊ)) = 0))) |
44 | 12, 29, 43 | syl2anc 585 |
. . . . . . . . . . . . . . 15
β’ (π β ((π
= 0π β¨
(degβπ
) <
(degβπΊ)) β
((degβπ
) β€
(degβπΊ) β§
((coeffβπ
)β(degβπΊ)) = 0))) |
45 | 41, 44 | mpbid 232 |
. . . . . . . . . . . . . 14
β’ (π β ((degβπ
) β€ (degβπΊ) β§ ((coeffβπ
)β(degβπΊ)) = 0)) |
46 | 45 | simpld 496 |
. . . . . . . . . . . . 13
β’ (π β (degβπ
) β€ (degβπΊ)) |
47 | | breq1 5084 |
. . . . . . . . . . . . . 14
β’
((degβπ) =
if((degβπ
) β€
(degβπ),
(degβπ),
(degβπ
)) β
((degβπ) β€
(degβπΊ) β
if((degβπ
) β€
(degβπ),
(degβπ),
(degβπ
)) β€
(degβπΊ))) |
48 | | breq1 5084 |
. . . . . . . . . . . . . 14
β’
((degβπ
) =
if((degβπ
) β€
(degβπ),
(degβπ),
(degβπ
)) β
((degβπ
) β€
(degβπΊ) β
if((degβπ
) β€
(degβπ),
(degβπ),
(degβπ
)) β€
(degβπΊ))) |
49 | 47, 48 | ifboth 4504 |
. . . . . . . . . . . . 13
β’
(((degβπ) β€
(degβπΊ) β§
(degβπ
) β€
(degβπΊ)) β
if((degβπ
) β€
(degβπ),
(degβπ),
(degβπ
)) β€
(degβπΊ)) |
50 | 40, 46, 49 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β if((degβπ
) β€ (degβπ), (degβπ), (degβπ
)) β€ (degβπΊ)) |
51 | 20, 27, 30, 34, 50 | letrd 11174 |
. . . . . . . . . . 11
β’ (π β (degβ(π
βf β
π)) β€ (degβπΊ)) |
52 | 51 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π βf β π) β 0π)
β (degβ(π
βf β π)) β€ (degβπΊ)) |
53 | 13, 2, 3, 4, 6 | plysub 25421 |
. . . . . . . . . . . . . 14
β’ (π β (π βf β π) β (Polyβπ)) |
54 | | dgrcl 25435 |
. . . . . . . . . . . . . 14
β’ ((π βf β
π) β (Polyβπ) β (degβ(π βf β
π)) β
β0) |
55 | 53, 54 | syl 17 |
. . . . . . . . . . . . 13
β’ (π β (degβ(π βf β
π)) β
β0) |
56 | | nn0addge1 12321 |
. . . . . . . . . . . . 13
β’
(((degβπΊ)
β β β§ (degβ(π βf β π)) β β0)
β (degβπΊ) β€
((degβπΊ) +
(degβ(π
βf β π)))) |
57 | 30, 55, 56 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (degβπΊ) β€ ((degβπΊ) + (degβ(π βf β
π)))) |
58 | 57 | adantr 482 |
. . . . . . . . . . 11
β’ ((π β§ (π βf β π) β 0π)
β (degβπΊ) β€
((degβπΊ) +
(degβ(π
βf β π)))) |
59 | | plyf 25400 |
. . . . . . . . . . . . . . . . . . . 20
β’ (πΉ β (Polyβπ) β πΉ:ββΆβ) |
60 | 7, 59 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ:ββΆβ) |
61 | 60 | ffvelcdmda 6989 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β β) β (πΉβπ§) β β) |
62 | 8, 2, 3, 4 | plymul 25420 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΊ βf Β· π) β (Polyβπ)) |
63 | | plyf 25400 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ βf Β·
π) β (Polyβπ) β (πΊ βf Β· π):ββΆβ) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΊ βf Β· π):ββΆβ) |
65 | 64 | ffvelcdmda 6989 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β β) β ((πΊ βf Β· π)βπ§) β β) |
66 | 8, 13, 3, 4 | plymul 25420 |
. . . . . . . . . . . . . . . . . . . 20
β’ (π β (πΊ βf Β· π) β (Polyβπ)) |
67 | | plyf 25400 |
. . . . . . . . . . . . . . . . . . . 20
β’ ((πΊ βf Β·
π) β (Polyβπ) β (πΊ βf Β· π):ββΆβ) |
68 | 66, 67 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΊ βf Β· π):ββΆβ) |
69 | 68 | ffvelcdmda 6989 |
. . . . . . . . . . . . . . . . . 18
β’ ((π β§ π§ β β) β ((πΊ βf Β· π)βπ§) β β) |
70 | 61, 65, 69 | nnncan1d 11408 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β β) β (((πΉβπ§) β ((πΊ βf Β· π)βπ§)) β ((πΉβπ§) β ((πΊ βf Β· π)βπ§))) = (((πΊ βf Β· π)βπ§) β ((πΊ βf Β· π)βπ§))) |
71 | 70 | mpteq2dva 5181 |
. . . . . . . . . . . . . . . 16
β’ (π β (π§ β β β¦ (((πΉβπ§) β ((πΊ βf Β· π)βπ§)) β ((πΉβπ§) β ((πΊ βf Β· π)βπ§)))) = (π§ β β β¦ (((πΊ βf Β· π)βπ§) β ((πΊ βf Β· π)βπ§)))) |
72 | | cnex 10994 |
. . . . . . . . . . . . . . . . . 18
β’ β
β V |
73 | 72 | a1i 11 |
. . . . . . . . . . . . . . . . 17
β’ (π β β β
V) |
74 | 61, 65 | subcld 11374 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β β) β ((πΉβπ§) β ((πΊ βf Β· π)βπ§)) β β) |
75 | 61, 69 | subcld 11374 |
. . . . . . . . . . . . . . . . 17
β’ ((π β§ π§ β β) β ((πΉβπ§) β ((πΊ βf Β· π)βπ§)) β β) |
76 | 60 | feqmptd 6865 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β πΉ = (π§ β β β¦ (πΉβπ§))) |
77 | 64 | feqmptd 6865 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΊ βf Β· π) = (π§ β β β¦ ((πΊ βf Β· π)βπ§))) |
78 | 73, 61, 65, 76, 77 | offval2 7581 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΉ βf β (πΊ βf Β·
π)) = (π§ β β β¦ ((πΉβπ§) β ((πΊ βf Β· π)βπ§)))) |
79 | 10, 78 | eqtrid 2788 |
. . . . . . . . . . . . . . . . 17
β’ (π β π
= (π§ β β β¦ ((πΉβπ§) β ((πΊ βf Β· π)βπ§)))) |
80 | 68 | feqmptd 6865 |
. . . . . . . . . . . . . . . . . . 19
β’ (π β (πΊ βf Β· π) = (π§ β β β¦ ((πΊ βf Β· π)βπ§))) |
81 | 73, 61, 69, 76, 80 | offval2 7581 |
. . . . . . . . . . . . . . . . . 18
β’ (π β (πΉ βf β (πΊ βf Β·
π)) = (π§ β β β¦ ((πΉβπ§) β ((πΊ βf Β· π)βπ§)))) |
82 | 14, 81 | eqtrid 2788 |
. . . . . . . . . . . . . . . . 17
β’ (π β π = (π§ β β β¦ ((πΉβπ§) β ((πΊ βf Β· π)βπ§)))) |
83 | 73, 74, 75, 79, 82 | offval2 7581 |
. . . . . . . . . . . . . . . 16
β’ (π β (π
βf β π) = (π§ β β β¦ (((πΉβπ§) β ((πΊ βf Β· π)βπ§)) β ((πΉβπ§) β ((πΊ βf Β· π)βπ§))))) |
84 | 73, 69, 65, 80, 77 | offval2 7581 |
. . . . . . . . . . . . . . . 16
β’ (π β ((πΊ βf Β· π) βf β
(πΊ βf
Β· π)) = (π§ β β β¦ (((πΊ βf Β·
π)βπ§) β ((πΊ βf Β· π)βπ§)))) |
85 | 71, 83, 84 | 3eqtr4d 2786 |
. . . . . . . . . . . . . . 15
β’ (π β (π
βf β π) = ((πΊ βf Β· π) βf β
(πΊ βf
Β· π))) |
86 | | plyf 25400 |
. . . . . . . . . . . . . . . . 17
β’ (πΊ β (Polyβπ) β πΊ:ββΆβ) |
87 | 8, 86 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β πΊ:ββΆβ) |
88 | | plyf 25400 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Polyβπ) β π:ββΆβ) |
89 | 13, 88 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π:ββΆβ) |
90 | | plyf 25400 |
. . . . . . . . . . . . . . . . 17
β’ (π β (Polyβπ) β π:ββΆβ) |
91 | 2, 90 | syl 17 |
. . . . . . . . . . . . . . . 16
β’ (π β π:ββΆβ) |
92 | | subdi 11450 |
. . . . . . . . . . . . . . . . 17
β’ ((π₯ β β β§ π¦ β β β§ π§ β β) β (π₯ Β· (π¦ β π§)) = ((π₯ Β· π¦) β (π₯ Β· π§))) |
93 | 92 | adantl 483 |
. . . . . . . . . . . . . . . 16
β’ ((π β§ (π₯ β β β§ π¦ β β β§ π§ β β)) β (π₯ Β· (π¦ β π§)) = ((π₯ Β· π¦) β (π₯ Β· π§))) |
94 | 73, 87, 89, 91, 93 | caofdi 7600 |
. . . . . . . . . . . . . . 15
β’ (π β (πΊ βf Β· (π βf β
π)) = ((πΊ βf Β· π) βf β
(πΊ βf
Β· π))) |
95 | 85, 94 | eqtr4d 2779 |
. . . . . . . . . . . . . 14
β’ (π β (π
βf β π) = (πΊ βf Β· (π βf β
π))) |
96 | 95 | fveq2d 6804 |
. . . . . . . . . . . . 13
β’ (π β (degβ(π
βf β
π)) = (degβ(πΊ βf Β·
(π βf
β π)))) |
97 | 96 | adantr 482 |
. . . . . . . . . . . 12
β’ ((π β§ (π βf β π) β 0π)
β (degβ(π
βf β π)) = (degβ(πΊ βf Β· (π βf β
π)))) |
98 | 8 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π βf β π) β 0π)
β πΊ β
(Polyβπ)) |
99 | 9 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π βf β π) β 0π)
β πΊ β
0π) |
100 | 53 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (π βf β π) β 0π)
β (π
βf β π) β (Polyβπ)) |
101 | | simpr 486 |
. . . . . . . . . . . . 13
β’ ((π β§ (π βf β π) β 0π)
β (π
βf β π) β
0π) |
102 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’
(degβπΊ) =
(degβπΊ) |
103 | | eqid 2736 |
. . . . . . . . . . . . . 14
β’
(degβ(π
βf β π)) = (degβ(π βf β π)) |
104 | 102, 103 | dgrmul 25472 |
. . . . . . . . . . . . 13
β’ (((πΊ β (Polyβπ) β§ πΊ β 0π) β§ ((π βf β
π) β (Polyβπ) β§ (π βf β π) β 0π))
β (degβ(πΊ
βf Β· (π βf β π))) = ((degβπΊ) + (degβ(π βf β
π)))) |
105 | 98, 99, 100, 101, 104 | syl22anc 837 |
. . . . . . . . . . . 12
β’ ((π β§ (π βf β π) β 0π)
β (degβ(πΊ
βf Β· (π βf β π))) = ((degβπΊ) + (degβ(π βf β
π)))) |
106 | 97, 105 | eqtrd 2776 |
. . . . . . . . . . 11
β’ ((π β§ (π βf β π) β 0π)
β (degβ(π
βf β π)) = ((degβπΊ) + (degβ(π βf β π)))) |
107 | 58, 106 | breqtrrd 5109 |
. . . . . . . . . 10
β’ ((π β§ (π βf β π) β 0π)
β (degβπΊ) β€
(degβ(π
βf β π))) |
108 | 20, 30 | letri3d 11159 |
. . . . . . . . . . 11
β’ (π β ((degβ(π
βf β
π)) = (degβπΊ) β ((degβ(π
βf β
π)) β€ (degβπΊ) β§ (degβπΊ) β€ (degβ(π
βf β
π))))) |
109 | 108 | adantr 482 |
. . . . . . . . . 10
β’ ((π β§ (π βf β π) β 0π)
β ((degβ(π
βf β π)) = (degβπΊ) β ((degβ(π
βf β π)) β€ (degβπΊ) β§ (degβπΊ) β€ (degβ(π
βf β
π))))) |
110 | 52, 107, 109 | mpbir2and 711 |
. . . . . . . . 9
β’ ((π β§ (π βf β π) β 0π)
β (degβ(π
βf β π)) = (degβπΊ)) |
111 | 110 | fveq2d 6804 |
. . . . . . . 8
β’ ((π β§ (π βf β π) β 0π)
β ((coeffβ(π
βf β π))β(degβ(π
βf β π))) = ((coeffβ(π
βf β
π))β(degβπΊ))) |
112 | 42, 36 | coesub 25459 |
. . . . . . . . . . . . 13
β’ ((π
β (Polyβπ) β§ π β (Polyβπ)) β (coeffβ(π
βf β π)) = ((coeffβπ
) βf β
(coeffβπ))) |
113 | 12, 16, 112 | syl2anc 585 |
. . . . . . . . . . . 12
β’ (π β (coeffβ(π
βf β
π)) = ((coeffβπ
) βf β
(coeffβπ))) |
114 | 113 | fveq1d 6802 |
. . . . . . . . . . 11
β’ (π β ((coeffβ(π
βf β
π))β(degβπΊ)) = (((coeffβπ
) βf β
(coeffβπ))β(degβπΊ))) |
115 | 42 | coef3 25434 |
. . . . . . . . . . . . . 14
β’ (π
β (Polyβπ) β (coeffβπ
):β0βΆβ) |
116 | | ffn 6626 |
. . . . . . . . . . . . . 14
β’
((coeffβπ
):β0βΆβ β
(coeffβπ
) Fn
β0) |
117 | 12, 115, 116 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β (coeffβπ
) Fn
β0) |
118 | 36 | coef3 25434 |
. . . . . . . . . . . . . 14
β’ (π β (Polyβπ) β (coeffβπ):β0βΆβ) |
119 | | ffn 6626 |
. . . . . . . . . . . . . 14
β’
((coeffβπ):β0βΆβ β
(coeffβπ) Fn
β0) |
120 | 16, 118, 119 | 3syl 18 |
. . . . . . . . . . . . 13
β’ (π β (coeffβπ) Fn
β0) |
121 | | nn0ex 12281 |
. . . . . . . . . . . . . 14
β’
β0 β V |
122 | 121 | a1i 11 |
. . . . . . . . . . . . 13
β’ (π β β0 β
V) |
123 | | inidm 4158 |
. . . . . . . . . . . . 13
β’
(β0 β© β0) =
β0 |
124 | 45 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β ((coeffβπ
)β(degβπΊ)) = 0) |
125 | 124 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (degβπΊ) β β0)
β ((coeffβπ
)β(degβπΊ)) = 0) |
126 | 39 | simprd 497 |
. . . . . . . . . . . . . 14
β’ (π β ((coeffβπ)β(degβπΊ)) = 0) |
127 | 126 | adantr 482 |
. . . . . . . . . . . . 13
β’ ((π β§ (degβπΊ) β β0)
β ((coeffβπ)β(degβπΊ)) = 0) |
128 | 117, 120,
122, 122, 123, 125, 127 | ofval 7572 |
. . . . . . . . . . . 12
β’ ((π β§ (degβπΊ) β β0)
β (((coeffβπ
)
βf β (coeffβπ))β(degβπΊ)) = (0 β 0)) |
129 | 29, 128 | mpdan 685 |
. . . . . . . . . . 11
β’ (π β (((coeffβπ
) βf β
(coeffβπ))β(degβπΊ)) = (0 β 0)) |
130 | 114, 129 | eqtrd 2776 |
. . . . . . . . . 10
β’ (π β ((coeffβ(π
βf β
π))β(degβπΊ)) = (0 β
0)) |
131 | | 0m0e0 12135 |
. . . . . . . . . 10
β’ (0
β 0) = 0 |
132 | 130, 131 | eqtrdi 2792 |
. . . . . . . . 9
β’ (π β ((coeffβ(π
βf β
π))β(degβπΊ)) = 0) |
133 | 132 | adantr 482 |
. . . . . . . 8
β’ ((π β§ (π βf β π) β 0π)
β ((coeffβ(π
βf β π))β(degβπΊ)) = 0) |
134 | 111, 133 | eqtrd 2776 |
. . . . . . 7
β’ ((π β§ (π βf β π) β 0π)
β ((coeffβ(π
βf β π))β(degβ(π
βf β π))) = 0) |
135 | | eqid 2736 |
. . . . . . . . . 10
β’
(degβ(π
βf β π)) = (degβ(π
βf β π)) |
136 | | eqid 2736 |
. . . . . . . . . 10
β’
(coeffβ(π
βf β π)) = (coeffβ(π
βf β π)) |
137 | 135, 136 | dgreq0 25467 |
. . . . . . . . 9
β’ ((π
βf β
π) β (Polyβπ) β ((π
βf β π) = 0π β
((coeffβ(π
βf β π))β(degβ(π
βf β π))) = 0)) |
138 | 17, 137 | syl 17 |
. . . . . . . 8
β’ (π β ((π
βf β π) = 0π β
((coeffβ(π
βf β π))β(degβ(π
βf β π))) = 0)) |
139 | 138 | biimpar 479 |
. . . . . . 7
β’ ((π β§ ((coeffβ(π
βf β
π))β(degβ(π
βf β
π))) = 0) β (π
βf β
π) =
0π) |
140 | 134, 139 | syldan 592 |
. . . . . 6
β’ ((π β§ (π βf β π) β 0π)
β (π
βf β π) = 0π) |
141 | 140 | ex 414 |
. . . . 5
β’ (π β ((π βf β π) β 0π
β (π
βf β π) = 0π)) |
142 | | plymul0or 25482 |
. . . . . . 7
β’ ((πΊ β (Polyβπ) β§ (π βf β π) β (Polyβπ)) β ((πΊ βf Β· (π βf β
π)) = 0π
β (πΊ =
0π β¨ (π βf β π) =
0π))) |
143 | 8, 53, 142 | syl2anc 585 |
. . . . . 6
β’ (π β ((πΊ βf Β· (π βf β
π)) = 0π
β (πΊ =
0π β¨ (π βf β π) =
0π))) |
144 | 95 | eqeq1d 2738 |
. . . . . 6
β’ (π β ((π
βf β π) = 0π β
(πΊ βf
Β· (π
βf β π)) = 0π)) |
145 | 9 | neneqd 2946 |
. . . . . . 7
β’ (π β Β¬ πΊ = 0π) |
146 | | biorf 935 |
. . . . . . 7
β’ (Β¬
πΊ = 0π
β ((π
βf β π) = 0π β (πΊ = 0π β¨
(π βf
β π) =
0π))) |
147 | 145, 146 | syl 17 |
. . . . . 6
β’ (π β ((π βf β π) = 0π β
(πΊ = 0π
β¨ (π βf
β π) =
0π))) |
148 | 143, 144,
147 | 3bitr4d 312 |
. . . . 5
β’ (π β ((π
βf β π) = 0π β
(π βf
β π) =
0π)) |
149 | 141, 148 | sylibd 239 |
. . . 4
β’ (π β ((π βf β π) β 0π
β (π
βf β π) = 0π)) |
150 | 1, 149 | pm2.61dne 3029 |
. . 3
β’ (π β (π βf β π) =
0π) |
151 | | df-0p 24875 |
. . 3
β’
0π = (β Γ {0}) |
152 | 150, 151 | eqtrdi 2792 |
. 2
β’ (π β (π βf β π) = (β Γ
{0})) |
153 | | ofsubeq0 12012 |
. . 3
β’ ((β
β V β§ π:ββΆβ β§ π:ββΆβ) β
((π βf
β π) = (β
Γ {0}) β π =
π)) |
154 | 72, 89, 91, 153 | mp3an2i 1466 |
. 2
β’ (π β ((π βf β π) = (β Γ {0}) β
π = π)) |
155 | 152, 154 | mpbid 232 |
1
β’ (π β π = π) |